The formal verification of computer systems has become practical. It has an essential role in tech firms such as Amazon, AMD, Intel, Microsoft and Nvidia. In recent years, researchers have started asking whether verification technology could also benefit research mathematicians. Here, we explore every aspect of doing logic on the computer: its foundations, its applications and the issues involved with formalising mathematics.


general examples Isabelle logic Isar Kurt_Gödel set_theory David_Hilbert Archive_of_Formal_Proofs philosophy newbies NG_de_Bruijn Martin-Löf_type_theory verification MJC_Gordon HOL_system type_theory sledgehammer recursion memories constructive_logic Stanford LCF HOL_Light Ackermann's_function type_classes incompleteness Robin_Milner AUTOMATH ALEXANDRIA nominal_package intuitionism axiom_of_choice automation analysis Mizar Hao_Wang Fibonacci Ernst_Zermelo Coq recruitment locales jEdit inductive_definitions gcd descriptions ZFC_in_HOL Russell Ramsey's_theorem Proofs_from_THE_BOOK PVS Imre_Lakatos Erdős Dana_Scott resolution quotients quaternions proof_documents ordinal_partitions nonstandard_analysis law_of_excluded_middle formal_mathematics Szemerédi’s_regularity_lemma Standard_ML QED_project MetiTarski Leonhard_Euler John_Littlewood Jacques_Fleuriot BDDs Alan_Turing