Lean 3's obsolete mathematical components library: please use mathlib4

十分钟魔法练习

formally verified category theory library

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Formalizing "Proofs from THE BOOK"

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).

The Principia Rewrite

Formalized quantum computing in Lean theorem prover

A Coq library providing tactics to deal with hypothesis

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

🧪 | Rinha de Backend Lean4

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.

Web-based natural deduction proof assistant

Experiments with interactive theorem provers, LLMs and formal systems

Aris: a logic engine/formal proof interface; 2nd generation, successor to the C version of Aris.

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.