Theorem Proving
(Up) | See also: Formal Specification, Coq
Works regarding the formal proving of theorems, and the mechanical implementation of such, especially (but not exclusively) as computer software.
Web resources
General
The Incredible Proof Machine ★★★
The de Bruijn criterion vs the LCF architecture ★
John Harrison: Slides from recent talks ★
Satisfiability modulo theories - Wikipedia
Do theorems provers demonstrate their own correctness? ★★★
What is a deep embedding vs a shallow embedding? With examples? ★
HOL (and HOL Light)
HOL Interactive Theorem Prover ★
HOL88/src/ml/hol-rule.ml at master · theoremprover-museum/HOL88 ★
Lean
notes-fplean/notes at cron - notes-fplean - Codeberg.org ★
F*
F*: A Higher-Order Effectful Language Designed for Program Verification ★
Calculational proofs · FStarLang/FStar Wiki ★
Executing F* code · FStarLang/FStar Wiki ★
Proof-oriented Programming in F* ★ 💭
F* - An introduction to the F* programming language ★
Program verification with F* ★ 💭
Other
Ulrich Berger, Minlog (wayback) ★
(in Equational Logic) Formal verification of simple equational proofs (as in Universal Algebra...)? ★
Repositories
stepchowfun/proofs: My personal repository of formally verified mathematics. ★★
thautwarm/Sequent.jl: formally and easily, describe the semantics. ★★ 💭
(in Name Binding) bacam/sato-maps-agda ★ 💭
Papers
Robbins Algebras are Boolean (online @ www.cs.unm.edu) ★ 💭
How to believe a machine-checked proof (online @ tidsskrift.dk) ★ 💭
Automated Reasoning and its Applications (online @ www.cl.cam.ac.uk) 💭
The LCF Approach to Theorem Proving (online @ www.cl.cam.ac.uk) ★ 💭
From LCF to HOL (online @ www.cl.cam.ac.uk)
Automated Reasoning for the Working Mathematician (online @ www.contrib.andrew.cmu.edu) ★ 💭
The Future of Mathematics? (online @ www.andrew.cmu.edu) ★★★ 💭
HOL Light - tutorial.pdf (online @ www.cl.cam.ac.uk) ★
Theorem proving support in programming language semantics (online @ arxiv.org) ★ 💭
Towards self-verification of HOL Light (online @ www.cl.cam.ac.uk)
A Self-Verifying Theorem Prover (online @ www.kookamara.com)
Hyperproof: Logical Reasoning with Diagrams (online @ aaai.org) ★★
Books
The Seventeen Provers of the World (borrow with print disabilities @ archive.org) ★ 💭
Theorem Proving in Lean 4 (online @ archive.org) ★ 💭
Handbook of Automated Reasoning, Vol. 1 (borrow with print disabilities @ archive.org) ★★
Handbook of Automated Reasoning, Vol. 2 (borrow with print disabilities @ archive.org) ★★
Hyperproof (borrow @ archive.org)