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.

Archive

general examples Isabelle logic Isar philosophy formalised_mathematics newbies Kurt_Gödel verification set_theory NG_de_Bruijn David_Hilbert Archive_of_Formal_Proofs Principia_Mathematica Martin-Löf_type_theory MJC_Gordon HOL_system type_theory sledgehammer recursion AUTOMATH type_classes memories inductive_definitions constructive_logic analysis Stanford LCF HOL_Light Fibonacci Ackermann's_function lambda_calculus incompleteness Robin_Milner Hao_Wang Bertrand_Russell ALEXANDRIA nominal_package intuitionism axiom_of_choice automation Paul_Erdős Mizar Imre_Lakatos Ernst_Zermelo Coq Alan_Turing recruitment locales jEdit gcd descriptions ZFC_in_HOL Ramsey's_theorem Proofs_from_THE_BOOK PVS Dana_Scott 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

Posts