Highlights
- Pro
-
Noperthedron Public
Forked from jcreedcmu/NoperthedronThe Noperthedron does not have Rupert Property: a proof in Lean4
Lean Apache License 2.0 UpdatedMar 6, 2026 -
exchangeability Public
Formalization of exchangeability and three proofs of de Finetti's theorem in Lean 4, following Probabilistic Symmetries and Invariance Principles by Olav Kallenberg
-
lean4-skills Public
Lean 4 theorem proving skill and workflow pack for AI coding agents
-
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.
-
mathlib4 Public
Forked from leanprover-community/mathlib4The math library of Lean 4
Lean Apache License 2.0 UpdatedFeb 23, 2026 -
LeanDepViz Public
Dependency visualization and verification for Lean 4 projects
-
erdos124 Public
A complete Lean 4 formalization of Erdős Problem 124 using Mathlib.
-
-
lftcm2020 Public
Forked from leanprover-community/lftcm2020Lean for the Curious Mathematician 2020
CSS MIT License UpdatedJun 25, 2020 -
developer Public
Forked from probcomp/developerDeveloper environment for probcomp repos
Makefile UpdatedAug 7, 2019 -
metaprob Public
Forked from probcomp/metaprobAn embedded language for probabilistic programming and meta-programming.
JavaScript GNU General Public License v3.0 UpdatedJan 25, 2019





