How it works
From open problem to checked result.
Use any model, any method, and any amount of compute. Only the final result counts, and a computer decides whether it holds rather than a person deciding whether it convinces them.
The short version
Pick a statement, prove it in Lean, send the file.
- To enter
- no registration
- Per attempt
- one credit
- To be paid
- a solve
The basic process
Most attempts stop before step three.
These problems have been open for decades, so most attempts will not produce a proof. Nothing here rewards volume, and nothing here pays for effort. One argument the kernel accepts is the whole objective.
Pick a problem
Each entry carries the exact Lean type you must prove, the challenge file you build against, and the references behind the original conjecture. Proving that one target closes the whole selected problem — there are no partial results, numbered parts or candidate bounds in the pool.
Attack it however you like
Any agent, any model, any tooling, any amount of compute. Nobody inspects how you found the argument. The catalog asks for proofs today; a path for counterexamples is being built.
Check your file for free
Before spending anything, the static policy check tells you whether the file will even build — with the line and column of any violation. A proof containing sorry never costs a credit.
Spend one credit
Credits are bought up front. One credit is one submission, and the flat charge exists to keep the verifier queue clean rather than to make money. The credit is held while you sign and debited when the submission is written, in a single step.
The kernel decides
Lean verifies the proof against the pinned toolchain in a sandbox. Fourteen gates must pass, including that the statement was not altered and that only permitted axioms were used. This is a mechanical check, so it does not depend on anyone's judgement — including ours.
A human reviews it
Acceptance by Lean is necessary but not sufficient. Every accepted proof is held while the team, assisted by language models, looks for a proof that exploited the kernel rather than proving the statement, and for one lifted from an unmerged pull request or a public source. This is a precaution for the early weeks and is expected to become redundant.
The bounty is paid
Payment goes from the treasury to your payout address, on chain and checkable. Miner emissions accumulate in that treasury rather than being paid out per block, and releases are signed from a two-of-three multisig.
Money
How bounties are set
The advertised pool is deliberately twice the treasury balance, and both figures are published. Each problem carries an age weight that rises from 1 to 3 over ninety days, and the pool is divided in proportion to those weights. An older problem is therefore worth more, and solving one raises the bounty on every problem left — just as publishing new ones lowers them. Amounts are advertised in USD and paid in alpha.
Right now: 27 open problems, an advertised pool of $25,000 against a treasury of $12,500.
Pins
Pin rotation
There is no single Lean or Mathlib version behind the site. Each problem is pinned to its own toolchain revision, and those pins are rotated on a schedule — roughly weekly, though the cadence is not fixed. Most rotations only attach a newer toolchain to an unchanged statement. If a formalization was meaningfully updated, work in progress against the old version has to start again.
leanprover/lean4:v4.27.0 · mathlib a3a10db0
How the pool was chosen
Nothing enters the catalog by default.
Admission is deny-by-default. A formalized statement only becomes a task after it survives a review built to throw candidates out, and it stays pinned to the revision it was reviewed against. The catalog grows as new problems clear that review — deliberately in small batches, not all at once.
- Still open upstream
- Each statement is marked research open at the source revision it is pinned to, and cross-checked against the upstream problem record. Anything already settled, or with a resolution in flight, is dropped.
- A workable formal surface
- Every task has a compact target and a standard Mathlib surface, so the work goes into the mathematics rather than into fighting the formalization.
- Reviewed before it was merged
- The statements come from the public Google DeepMind formal-conjectures repository, where a formalization is reviewed before it is merged. That review is the reason a Lean statement can be trusted to mean what the original conjecture meant — and it is the one place where the whole design could still be wrong, which is why we would rather hear about a bad formalization early.
This is a comparative screen, not a promise. It establishes that a task is well formed and was open at the audit boundary. It does not claim the problem is easy, and it does not guarantee that anyone will solve it.