Lean 3's obsolete mathematical components library: please use mathlib4
-
Updated
Jun 28, 2024 - Lean
#
formal-mathematics
Here are 91 public repositories matching this topic...
A collection of formalized statements of conjectures in Lean.
-
Updated
Oct 30, 2026 - Lean
LLMs as Copilots for Theorem Proving in Lean
-
Updated
Oct 13, 2026 - C++
The Principia Rewrite
latex coq logic latex-packages formal-mathematics coq-ecosystem formal-proofs formal-logic history-of-philosophy
-
Updated
Jul 19, 2026 - TeX
[ICML2026] The first, fully verified, sorry-free, large-scale Lean 4 library for statistical learning theory, covering infrastructures for mordern statistics and learning theory.
formalization formal-mathematics machine-learning-theory learning-theory lean4 high-dimensional-statistics high-dimensional-probability autoformalization statistical-learning-theory icml2026
-
Updated
Jul 15, 2026 - Lean
The matrix cookbook, proved in the Lean theorem prover
-
Updated
Oct 26, 2026 - Lean
A template for blueprint-driven formalization projects in Lean.
theorem-proving mathematics proof-assistant formal-mathematics mathematical-programming lean-theorem-prover lean4 formalisation-mathematics lean-blueprint formalised-mathematics leanblueprint
-
Updated
Oct 19, 2026 - Python
Lean formalizations of IMO problem statements
-
Updated
Apr 23, 2026 - Lean
Repository hosting the resources for the conference "ItaLean 2025", held in Bologna, Italy, December 9–12, 2025.
machine-learning ai conference artificial-intelligence formal-methods formal-mathematics lean4 ai4math
-
Updated
Jul 27, 2026 - HTML
Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.
lean natural-numbers formal-mathematics peano theorem-prover microsoft-research lean-theorem-prover imperial-college-london gamified-learning
-
Updated
Dec 12, 2021
The Slate Interactive Theorem Prover
web-app collaboration proof-assistant mathematical-expressions mathematical-logic formal-mathematics interactive-theorem-proving
-
Updated
Jan 9, 2023 - TypeScript
A curated list of awesome interactive theorem prover frameworks
math mathematics formalization formal-verification formal-mathematics interactive-theorem-proving interactive-theorem-prover
-
Updated
Oct 22, 2026
TreeThink: Mathematical Reasoning of LLMs with Tree Search Methods | EMNLP 2026 System Demonstrations
-
Updated
Oct 24, 2026 - Python
A style guide for Coq
c haskell dependent-types style-guide ocaml coq proof formal-semantics verification proof-assistant software-engineering formal-methods formal-verification formal-mathematics formal-specification formal-proofs appliedfm
-
Updated
Nov 30, 2021
AI-powered IDE for Lean 4 theorem proving. Integrates Claude as a proof assistant with full tool use, live tactic state, inline diagnostics, Unicode input, and Lake build support. Built with Flutter.
-
Updated
Mar 14, 2026 - Dart
A fork of openai/miniF2F adapted to Lean 4, with corrections to formalizations and informal descriptions. for human readers.
-
Updated
Apr 23, 2026 - Lean
rubikcubegroup魔方定理证明+视频分享。discuss here: https://lean4daydayup.zulipchat.com/join/45reytdk5yv7t7sheywhulw3/
-
Updated
Apr 16, 2024 - Lean
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
tutorial research logic mathematics proof-assistant lean formal-methods formal-mathematics interactive-theorem-proving tu-wien formal-proofs formalisation leanprover lean4 formalized-mathematics formalisation-mathematics
-
Updated
Jan 14, 2025 - Lean
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
algebra mathematics proof-assistant lean formal-methods formalization number-theory formal-mathematics interactive-theorem-proving theorem-prover formal-proofs mathematical-programming lean4
-
Updated
Aug 21, 2024 - TeX
A kernel-minimal LCF-style HOL theorem prover in the Wolfram Language
-
Updated
Jun 21, 2026 - Wolfram Language
Add this topic to your repo
To associate your repository with the formal-mathematics topic, visit your repo's landing page and select "manage topics."