Proof Verification

Lean Theorem Prover

• Lean Zulip — Community chat for Lean users.
• Loogle! — Search Mathlib by name, subexpression, or type shape.
• Lean 4 Web — Run Lean with Mathlib in the browser, no install needed.
• Mathlib Docs — API documentation for Mathlib 4.
• The Lean Prover Community — Community resources for Lean theorem prover.
• Lean 4 Documentation — Official documentation for Lean 4.
• Theorem Proving in Lean — A textbook on theorem proving using Lean.
• Mathematics in Lean — A tutorial on formalizing mathematics with Mathlib.
• Functional Programming in Lean — A book on writing programs in Lean 4.
• Glimpse of Lean — A short introductory course for mathematicians new to Lean.

The Rocq Prover (Coq Proof Assistant)

• Rocq — Interactive theorem prover for formalizing mathematics.
• UniMath — Univalent mathematics library for Rocq.

Agda

• Agda — Dependently typed functional language and proof assistant.
• Agda Docs — Reference manual and user guide for Agda.
• Cubical Agda — Standard library for cubical type theory in Agda.
• agda-unimath — Library of univalent mathematics formalized in Agda.

Isabelle

• Isabelle — Generic proof assistant, best known for Isabelle/HOL.
• Isabelle Docs — Manuals, tutorials, and the Archive of Formal Proofs.

← Back to Home