AI provers on a Bittensor subnet close six decades-old Erdős problems in ten days

markjeffrey · x · 2026-09-19

conjecture.io announced that SN66, a Bittensor subnet that pays bounties for solving open math problems, has had its miners resolve six long-standing open problems in ten days — roughly 249 combined years unsolved:

Every result is machine-checked in Lean — formal proofs published with code that anyone can rerun, not just "we believe." Problems Erdős posed that top mathematicians couldn't close in half a century were picked off one by one by a swarm of miners running AI provers, in public.

Original post →

More from Research

Research channel →