Stars
MCP Server for AI agents to interact with our Lean infrastructure
Research code base for Automatic Textbook Formalization
Lean theorem proving interface which feels like pen-and-paper proofs.
Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked
Lean formalizations for the paper "On the paucity of lattice triangles"
LeanInteract: A Python Interface for Lean 4
Lean evaluation and metaprogramming utilities for provers.
Lean formalizations for the paper "Almost all primes are partially regular"
Lean formalizations for the paper "Parity of k-differentials in genus zero and one"
Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"
A collection of optimization problems in mathematics
The Noperthedron does not have Rupert Property: a proof in Lean4
Blueprint for the PNT+ Project
SorryDB indexes sorries in public lean repositories
A formal proof of the Riemann Hypothesis for curves