-
hex Public
Verified computational algebra in Lean 4 — polynomial factoring, LLL, and friends
-
lean4 Public
Forked from leanprover/lean4Lean 4 programming language and theorem prover
Lean Apache License 2.0 UpdatedJun 15, 2026 -
-
Independent comparator verification: the uniform-constant Erdős unit-distance conjecture is false (Alpöge 2026, formalized)
-
jacobian-claude Public
Forked from rkirov/jacobian-claudeClaude code trying to formalize Jacobians. I don't understand the math, and haven't reviewed any of this.
-
erdos-unit-distance Public
Formalization of Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture (companion to mathlib4 branch kim/erdos-unit-distance)
-
mathlib4 Public
Forked from leanprover-community/mathlib4The math library of Lean 4
-
fplll-ffi Public
Lean 4 FFI bindings for the fplll lattice-reduction library, with the unimodular transform for downstream result verification
Lean Apache License 2.0 UpdatedJun 8, 2026 -
bubble Public
Containerized Lean 4 development environments
-
lean-v431-link-repro Public
Minimal reproducer: Lean v4.31.0-rc1 static FFI link fails on Linux with undefined libc++ symbols
UpdatedJun 3, 2026 -
LeanTriathlon Public
Forked from project-numina/LeanTriathlonLean Apache License 2.0 UpdatedJun 3, 2026 -
-
lean-bench-samply Public
Samply-specific orchestrator + postprocessor on top of lean-bench's timed-regions sidecar.
Python UpdatedMay 30, 2026 -
codewars Public
Lean 4 support for codewars.com (proposal & runner image)
-
mathlib-ci Public
Forked from leanprover-community/mathlib-ciScripts and utilities to support the mathlib repository's CI/CD operations
-
presentations Public
Forked from leanprover/presentationslean-related presentations
-
-
hex-lp Public
Sketch: a fast, fully verified Lean-native LP library. SKETCH.md outlines phases 0-13 from textbook simplex through verified MILP.
UpdatedMay 12, 2026 -
lean-qsopt Public
Stub: planned Lean 4 FFI bindings for QSopt-Exact (exact-rational LP solver). PLAN.md only.
UpdatedMay 12, 2026 -
cslib Public
Forked from leanprover/cslibA Lean library for Computer Science
-
lint-style-action Public
Forked from leanprover-community/lint-style-actionMathlib style linter
UpdatedMay 12, 2026 -
VCV-io Public
Forked from Verified-zkEVM/VCV-ioFormalized Cryptography Proofs in Lean 4
Lean Apache License 2.0 UpdatedMay 12, 2026 -
ceili Public
Android app for Irish set dancing — Matt Cunningham's Dance Music of Ireland series with calling instructions and pitch-preserving tempo control
Kotlin UpdatedMay 10, 2026 -
CompPoly Public
Forked from Verified-zkEVM/CompPolyComputable Polynomials in Lean.
Lean Apache License 2.0 UpdatedMay 10, 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 -
-
pod-1 Public
Forked from FormalFrontier/podMulti-agent manager for Claude Code
-
reference-manual Public
Forked from leanprover/reference-manualThe Lean reference manual
-
aesop Public
Forked from leanprover-community/aesopWhite-box automation for Lean 4
-
lean-action Public
Forked from leanprover/lean-actionGitHub action for standard CI in Lean projects
{{ message }}