-
compfiles Public
Catalog Of Math Problems Formalized In Lean
-
tryAtEachStep Public
Try a tactic at each step in a Lean proof.
-
-
Rupert.lean Public
Formalization of the Rupert Problem for convex polyhedra.
-
Example Sandstorm app using only the raw Cap'n Proto API, written in Rust.
-
sandstorm-rust Public
Sandstorm Cap'n Proto interfaces, packaged for Rust
-
-
acronymy.net Public
collaborative website asking: can we define every word as an acronym?
-
matroid-generator Public
Forked from gmou3/matroid-generatorGenerate all non-isomorphic matroids
-
formal-conjectures Public
Forked from google-deepmind/formal-conjecturesA collection of formalized statements of conjectures in Lean.
Lean Apache License 2.0 UpdatedMay 9, 2026 -
FLT Public
Forked from ImperialCollegeLondon/FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
Lean Apache License 2.0 UpdatedMay 7, 2026 -
docgen-action Public
Forked from leanprover-community/docgen-actionAction to generate Lean documentation pages
JavaScript UpdatedMay 7, 2026 -
Sphere-Packing-Lean Public
Forked from thefundamentaltheor3m/Sphere-Packing-LeanA Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
Lean Apache License 2.0 UpdatedApr 21, 2026 -
lean4lean Public
Forked from digama0/lean4leanLean 4 kernel / 'external checker' written in Lean 4
Lean UpdatedMar 21, 2026 -
mathlib4 Public
Forked from leanprover-community/mathlib4Work in progress mathlib port for lean 4
Lean Apache License 2.0 UpdatedMar 18, 2026 -
OSforGFF Public
Forked from mrdouglasny/OSforGFFA Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms
-
-
-
PrimeNumberTheoremAnd Public
Forked from AlexKontorovich/PrimeNumberTheoremAndblueprint for prime number theorem and more
Lean Apache License 2.0 UpdatedJan 18, 2026 -
plastexdepgraph Public
Forked from PatrickMassot/plastexdepgraphDependency graph plugin for plasTeX
Python Apache License 2.0 UpdatedJan 14, 2026 -
animate-lean-proofs Public
tool for turning Lean proofs into Blender animations
-
infinity-cosmos Public
Forked from emilyriehl/infinity-cosmosA blueprint for a formalization of infinity-cosmos theory in Lean.
TeX Apache License 2.0 UpdatedNov 19, 2025 -
equational_theories Public
Forked from teorth/equational_theoriesA project to map out the relations between different equational theories of Magmas.
TeX Apache License 2.0 UpdatedOct 29, 2025 -
-
doc-gen4 Public
Forked from leanprover/doc-gen4Document Generator for Lean 4
Lean Apache License 2.0 UpdatedSep 13, 2025 -
lean-interval Public
Forked from girving/intervalConservative floating point interval arithmetic in Lean
-
lean4-maze Public
maze game encoded in Lean 4 syntax
-
rust Public
Forked from rust-lang/rusta safe, concurrent, practical language
-
-
acronymy-assistant Public
interactive backronym composition tool
{{ message }}