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.

Isabelle

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

← Back to Home