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