What this is, and what it is not.

A Bittensor subnet aimed at open mathematical conjectures. The site publishes them as exact Lean statements that anyone can attack, and the network around it pays for results that survive formal checking. The goal is to settle problems that have been open for decades, add those proofs to the mathematical record, and show what a Bittensor subnet can produce.

In July 2026 the Jacobian Conjecture in dimension three, open for 87 years, and the Dinitz–Garg–Goemans conjecture, open for roughly 30, both fell to model-assisted searches days apart. Both are linked from the home page. Whatever that capability turns out to be worth, very little of it is pointed at open problems, and there is no standing place to bring a result if you find one.

A conjecture is a mathematical statement that looks true — often with a great deal of evidence behind it — but that nobody has managed to prove. The ones here are open questions that working mathematicians have tried and failed to settle, some for decades. Proving one is a genuine contribution, not an exercise with a known answer.

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.

Both Bittensor miners and mathematicians. Today taking part requires a wallet, which is a barrier we know about — card and USDC payment for the submission fee, and USDC payouts, are planned so that someone outside crypto can take part.

A Lean proof of the exact statement shown on the problem page. Not a sketch, not an argument in prose — a file the kernel can check. Nobody inspects how you found it.

No. There is no registration and no UID to compete for. You pay a flat fee per submission, which keeps spam out of the verifier queue, and that is the only gate.

One credit per submission, currently priced at 0.5 TAO. Credits are bought up front and do not expire. The rate is a configuration value and can change. It should not worry anyone doing real work: the file is checked against the static policy for free before any credit is spent.

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.

It depends on the problem and on when you solve it. The advertised pool is twice the treasury balance and is divided between the open problems in proportion to an age weight that rises from 1 to 3 over ninety days. So an older problem pays more, solving one raises the bounty on everything left, and publishing new problems lowers them. Each problem page shows its current amount and when that snapshot was taken.

Miner emissions accumulate in a treasury rather than being paid out per block. When a proof is verified and clears review, the bounty is transferred to your payout address. Bounties are advertised in USD and paid in alpha, and releases are signed from a two-of-three multisig — manually at first.

Thinner roles than the words suggest. A miner carries the submitted Lean file and signs its commitment; the reference miner does not even ship a proof generator. The validator runs the file through the pinned toolchain and publishes the verdict. Neither role says anything about how the mathematics has to be found.

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 itself comes from a public repository where formalizations are reviewed before they are merged. The real risk in this design is not that Lean accepts a bad proof — it is that a formalized statement does not faithfully capture the original conjecture, which is exactly why we ask people to report one that looks wrong.

Copying a proof from an unmerged pull request or from anywhere on the internet is disqualifying, as is exploiting a weakness in the kernel rather than proving the statement. The full list is shown before you spend a credit, and the reason is shown to you if a submission is rejected. This step is a precaution for the early weeks: it is likely redundant and we do not expect to need it in the long run.

Proofs. Every task in the pool asks for a proof of the published statement, and a counterexample needs its own formal statement and verification path. That path is not much harder to build and is expected at launch or shortly after — but until it lands, a disproof has nowhere to go here.

Lean itself is quick, and the queue is often empty. What follows is not: an accepted proof is held for manual review before any reward is issued, and that is measured in hours rather than minutes. We do not publish a target time, because we would rather not commit to one we have not tested.

A problem resolved outside the subnet is retired from the pool and no bounty is payable on it. We check for this by hand today and intend to have an agent watching for published solutions; until that is running, the gap between a result appearing elsewhere and the problem being retired is real and is on us.

Most rotations attach a newer toolchain to an unchanged statement and nothing about your work changes. If a formalization was meaningfully updated — usually because part of it was wrong — then work against the old version has to start again. Submissions pause while a rotation runs.

There is an optional credit field on a submission, and you may leave it blank. Results are contributed upstream under the Conjectures account rather than an individual one, so that the repository gets a single recognisable contributor. Publicly we show the on-chain identity that submitted the proof, not a personal name.

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.

That is the one real risk in the whole system, so we would rather hear about it early — before someone spends weeks on it. Reach us on Discord.

Yes, and more are ready than are published. The pool is being kept small on purpose until there is a real sense of how often solves happen, since the advertised pool is a public promise made against a treasury we would rather not overrun. Every candidate clears the same admission review before it becomes a task.

The catalog, the submission flow and the isolated verifier work. Payouts are signed manually, counterexample handling is not built, and payment without a Bittensor wallet is planned rather than available. Where a page can tell you which of these applies, it does.