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