// leak
Leak is the proving engine behind CompeteMath. When a problem here is marked verified, a Leak prover wrote a proof in Lean 4 and the Lean kernel checked it — the claim is machine-checked, not eyeballed. See About for the wider project.
Leak is not one program. It is four families of prover, each attacking a proof a different way, plus a small set of services they all share.
They differ in how much compute they are willing to spend and in how they break a hard theorem into pieces it can actually close.
The lightweight member of the family. River goes at a problem directly and cheaply, which makes it the right first attempt on anything that is not deeply hard — and a fast baseline to measure the heavier provers against.
View repositoryA heavy recursive decomposer. Stronghold splits a theorem into sub-goals, then splits the sub-goals that resist, recursing until the pieces are small enough to close outright and reassembling the proof on the way back up.
View repositoryA heavy DAG-refinement loop. Ultra lays the argument out as a dependency graph of lemmas and repeatedly refines that graph in light of what the last pass proved and what it got stuck on, rather than committing to one decomposition up front.
View repositoryOur most advanced prover, and a hybrid of the two above. Finality takes Stronghold’s decomposition and Ultra’s refinement loop and runs them together, so it can keep breaking a goal down and redesign the whole plan when the evidence says the plan is wrong. The result adapts to a problem far better than either parent does alone.
View repositoryStronghold, Ultra and Finality drive Anthropic’s Claude models as their reasoning core. Everything we write — the orchestration, the decomposition, the refinement, the verification gates — is open, but the model at the centre is not ours to open. So those three are open source in the parts we own and closed in the part we do not, and we would rather say that plainly than call them something they are not.
The provers do not talk to Lean directly. They talk to MCP services that search the library, hold a live proof state, and compile. The deployments are private — they are ours, and they cost real compute to run — but the source is open, so you can read exactly what a prover is allowed to ask for and what it gets back.
There are two of these groups, on two different versions of Lean, and a proof is certified by whichever group its prover runs on. That is not an accident of history we are hiding: a proof that compiles on one Lean does not automatically compile on the other, so we keep the groups separate and record which one signed off.
Lean 4.29.1 — Stronghold & Finality
Lemma search over Mathlib. A prover describes the shape of the result it needs and Leak I finds what already exists, so it builds on the library instead of reinventing it.
View repositoryAn interactive Lean proof-state daemon. A prover can open a goal, apply one tactic, and look at what it did — the difference between reasoning about a proof and actually stepping through it.
View repositoryNo longer in service. It is listed here for provenance: the repository stays public so the history of how the stack got to its current shape is not quietly erased.
View repositoryThe gate for this group. Leak IV compiles a complete proof script and reports exactly what the kernel says. A proof only counts as proved once this service accepts it — and it rejects on warnings too, so an unfinished proof can never pass as a finished one.
View repositoryLean 4.32.0 — River & Ultra
Library search for the newer toolchain — the counterpart of Leak I, against the Mathlib these two provers actually build on.
View repositoryThe working compiler. River and Ultra design a proof as a dependency graph, and Leak XII both compiles that graph and checks it is a valid one — no cycles, no dead nodes, and an assembly that really does derive the target from its parts. It also elaborates individual declarations, so a prover can ask what a name actually means instead of guessing.
View repositoryThe gate for this group — the same role Leak IV plays for the other one. Nothing from River or Ultra counts as proved until Leak XIV has certified the assembled proof.
View repository