Stars
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"
A computable model of Polynomials in Lean.
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
Tool for animating the history of a Lean Blueprint dependency graph
A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions