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 ★★★

LCF architecture | PLS Lab ★

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 ★

HOL Light ★

HOL Light - Wikipedia

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 ★

F* Tutorial ★

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

Metamath Home Page ★

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) ★ 💭

Logic Machines and Diagrams (online @ archive.org) (borrow @ archive.org) ★★ 💭