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
- 0.5 τ
- 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. It runs on your own machine and a proof containing sorry never costs a transfer.
Pay for the attempt
One transfer of 0.5 τ from your coldkey funds exactly one verification attempt. The flat charge exists to keep the verifier queue clean rather than to make money, and a submission is only created once the transfer is confirmed on finalized chain state.
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
Every open target draws from one pool, and what it pays is worked out from how long it has stood open rather than fixed in advance. Figures are shown in dollars, converted by the backend from a live rate at the moment the page was built - the payout itself is made in alpha, so treat the dollar amount as what it was worth then rather than as a fixed sum. Where the rate is unavailable the alpha figure is shown instead, and where the API states no amount at all the page says so rather than guessing.
Right now: 146 open problems, drawing on a pool of $11,488.
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 · formal-conjectures 379fc029
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.
Sending it
Submission runs from the command line.
There is no browser upload yet. The validator's client builds the bundle, checks it against the same policy the server runs, and signs the request with your hotkey - all of it documented step by step.