How it works
From an open problem to a paid proof.
Everything happens on this site. You need an account to submit, and a Bittensor wallet only when it is time to be paid.
The short version
Prove it in Lean, upload the chat, get paid.
- To enter
- an account
- Per attempt
- one credit, 0.25 τ
- To be paid
- an accepted proof and its chat logs
Step by step
Seven steps, each on its own page.
Most attempts end at step six. These problems have stood for years and nothing here pays for effort: one proof that Lean accepts is the whole objective.
Create an account
Sign up with a password, Google, an email link, or a Bittensor wallet in Talisman or TAO.com. Nothing else is needed until you are paid.
Sign upPick a problem
Each problem is an exact Lean statement. Prove it or refute it: both count, and the first accepted answer takes the bounty.
Browse problemsWork on it, and keep the chat
Use any model, agent or tool. Every open problem needs the original AI chat logs that produced the proof, so keep them. Your agent can package them for you.
What we check in chat logsGet credits
One credit buys one verification attempt. Pay with TAO from a linked wallet or with other crypto through TMC Pay, or claim an invitation if someone sent you one.
Top upCheck, then submit
Add your Lean file and the page checks it for free. Then upload the chat logs and submit, which spends one credit. You can attach PDFs that explain the argument.
Submit a proofLean, then a reviewer
The proof is compiled and checked by the Lean kernel in a sandbox, usually within minutes. A reviewer then reads the chat logs and checks the grounds in the submission terms. Both decisions are published.
Submission termsGet paid
The bounty is paid in alpha to the wallet you choose for rewards in your account settings.
Account settings
Money
How much a problem pays.
A new problem opens at 2.5% of the available reward pool and rises to 12.5% over 15 days while it stays open. The amount is fixed when you submit, so it does not move during verification or review. Bounties are paid in alpha; dollar figures are estimates at the current rate.
Right now: 254 open problems, drawing on a pool of $51,435.
Your payout wallet
A wallet only for getting paid.
Install the Talisman or TAO.com browser extension and create a Bittensor account in it. Then connect it in your account settings and choose it for rewards. You can do this after your proof is accepted, but no reward is paid until a wallet is set.
Account settingsWhere the problems come from
Every problem was open when it entered.
Statements come from Formal Conjectures, a public repository maintained by Google DeepMind, where a formalization is reviewed before it is merged. A problem enters the catalog only after an audit confirms it is still open, and it stays pinned to the revision that was audited.
- Still open
- Marked research open at its pinned revision and checked against the original problem record. Anything already settled is left out.
- Pinned
- The statement, the toolchain and every definition it uses are fixed. When a problem gets a new version, a proof already submitted is still checked against the version it was written for.
- Reported, not assumed
- If a formal statement does not match the original conjecture, tell us on Discord. A proof of a faulty statement can earn a capped defect award instead of the bounty.
leanprover/lean4:v4.35.0-rc2 · formal-conjectures 1ccfff4d
Optimisation
The same rule, for code.
The optimisation competitions apply the same check to software: faster code plus a Lean proof that it behaves exactly like the original. Each one has its own rules on its page.
Ready?
Pick a problem.
Already mining on Bittensor? The command-line client does all of this from a terminal. Miner guide