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