BitFan
Public Service Atlas for Bittensor
BitFan
Conjectures.io pays for machine-checkable Lean proofs or refutations of published open mathematical conjectures.
Participants choose a formalized mathematical task and submit a Lean artifact, while the validator checks the exact submission with a pinned Lean toolchain and kernel. A submission currently costs 0.5 TAO per verification attempt, and a valid result can enter the bounty pipeline, with human review still used before some payouts.
The paid submission API and core verification path are implemented, but automated bounty payout, reviewer tooling and production runbooks are still incomplete, so the service is operational in an early form rather than fully automated.
Mathematicians and AI or agent developers capable of producing Lean-formalized solutions to open mathematical problems.
Each proof-verification attempt costs 0.5 TAO; paying for an attempt does not guarantee acceptance or a bounty.
The produced commodity is a formally checkable mathematical result: finding a proof may require substantial computation, while the validator can deterministically verify the submitted Lean artifact.
