Questions, answered.

A Bittensor subnet that pays for verified results. The main competition is open mathematics: unsolved conjectures written as exact Lean statements, with a bounty for a proof or a counterexample that the Lean kernel accepts. Alongside it run optimisation competitions, where faster code has to come with a Lean proof that it still does the same thing.

Lean is software for writing mathematical statements and proofs in a language precise enough for a computer to check. You write your argument in it, and Lean confirms whether that argument really does establish the statement. It cannot be talked round: a proof either checks or it does not.

Not to start. You sign up with email or Google, or with a Talisman or TAO.com wallet if you already have one, check proofs for free and submit from the browser. Credits are paid in crypto: TAO from a linked wallet, or other coins through TMC Pay. An invitation can cover your first attempts. To be paid you need a Bittensor wallet, which takes a few minutes to set up; How it works shows how.

A Lean file that proves the exact statement on the problem page, or its negation for a counterexample, together with the AI chat logs that produced it. You can add PDFs that explain the argument; they are published only if the proof is approved.

Either. Every problem has a proof task and a counterexample task, and they compete for one reward: the first accepted answer, in either direction, takes it.

A reviewer reads them to confirm the proof came out of that work. They have to be the original chats, not a recreation. Once accepted, we may sell and license them, including for training and evaluating AI systems; they are not published openly. Logs that are not accepted are deleted within 90 days. Proofs accepted before logs were required can still earn a bonus for theirs.

One credit buys one verification attempt, and the price is shown when you top up. Checking a file before you submit is free. A credit is refunded only if the attempt could not run for a reason on our side; a proof that Lean rejects has used its attempt.

No. Rewards are paid on a solve only. Someone who works on a problem for three months and does not settle it earns nothing, and that is the intended design rather than an oversight.

Each problem shows its current bounty. It grows with how long the problem has been open and is fixed the moment you submit. It is paid in alpha to your payout wallet after Lean accepts the proof and a reviewer approves it. How it works has the formula.

Because it rests on two things you can inspect rather than on anyone's opinion. The Lean kernel is a mechanical check that a proof establishes a statement, and the statement comes from a public repository where formalizations are reviewed before they are merged. The real risk is a formal statement that does not match the original conjecture. If you find one, tell us in our Discord channel; you need to join the Bittensor server first.

Only for a reason on the published list in the submission terms. The common ones: the result was already proved before you submitted, the same target had already been formalized elsewhere, or the chat logs were not accepted. A rejection always names its reason.

If a complete public proof appears before we accept your submission, the problem no longer pays a bounty. A proof that appears only after we accepted yours does not affect it.

Yes. Every result names its solver: your display name if you set one, otherwise the wallet address behind the submission. You can also attach a public credit to a submission.

No. The statements are drawn from formal-conjectures, a public repository DeepMind maintains, and we rely on the review that happens there before a formalization is merged. There is no partnership or endorsement beyond using an open repository as intended.