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

• UpdatedJun 28, 2024
• Lean

十分钟魔法练习

• UpdatedSep 2, 2023
• HTML

formally verified category theory library

• UpdatedJun 23, 2020
• Idris

The Principia Rewrite

• UpdatedJan 30, 2025
• TeX

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

• UpdatedJan 22, 2025
• Coq

• UpdatedMar 7, 2025
• Isabelle

🧪 | Rinha de Backend Lean4

• UpdatedSep 12, 2023
• Lean

Formalizing "Proofs from THE BOOK"

• UpdatedDec 11, 2024
• TeX

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

• UpdatedJul 13, 2023
• OCaml

Formalized quantum computing in Lean theorem prover

• UpdatedMar 6, 2021
• Lean

A Coq library providing tactics to deal with hypothesis

• UpdatedDec 20, 2024
• Coq

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

• UpdatedMar 13, 2025
• C++

Experiments with interactive theorem provers, LLMs and formal systems

• UpdatedJul 10, 2023
• Coq

A style guide for Coq

• UpdatedNov 30, 2021

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

• UpdatedMar 17, 2025
• Isabelle

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).

• UpdatedFeb 22, 2025
• ReScript

A toy formally-specified Computer Algebra library written in Rust and formalized in Lean 4

• UpdatedJan 15, 2025
• Rust

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

• UpdatedJan 14, 2025
• Lean

A library of formalized automaton algorithms

• UpdatedAug 3, 2022
• Coq

• UpdatedJan 10, 2019
• Lean