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.


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