Table of Contents
Conjectures, a Bittensor subnet focused on Lean-verified mathematics, has announced miner-submitted solutions to two more Erdős problems, adding to a fast run of formal proof results from the project.
The team said on X that its miners solved Erdős Problem 108, a 55-year-old graph theory question, and Erdős Problem 653, a 29-year-old problem in discrete geometry. Both results were verified in Lean through Conjectures.
The update comes only days after Conjectures said its miners had found a Lean-verified counterexample to Erdős Problem 96, a long-standing question about unit distances in convex polygons.
Bart Hillerich
Conjectures Says Miners Settled Two Erdős Problems
The first new result concerns Erdős Problem 108, which asks whether graphs with sufficiently large chromatic number must contain high-girth subgraphs that also have large chromatic number.
In simpler terms, the problem asks whether enough global coloring complexity in a graph forces the existence of a similarly complex substructure after short cycles are ruled out.
Conjectures said the new result disproves the conjecture.
According to the team’s announcement, the construction produces graphs with arbitrarily high chromatic number whose subgraphs without four-cycles require at most six colors.
The result separates two kinds of graph complexity. A graph can be difficult to color overall, while the parts that avoid a particular short-cycle pattern remain bounded in coloring difficulty.
Conjectures published both the Lean proof for Erdős Problem 108 and an accompanying PDF paper.
The second result concerns Erdős Problem 653, a problem about distances determined by points in the plane. The question involves, for each point in a finite planar set, counting how many distinct distances that point sees to the other points.
More simply, the problem asks whether a large collection of points can be arranged so that nearly every point “sees” a different number of unique distances to the other points.
Conjectures said the new result proves that, as the number of points grows, n points in the plane can have almost n different counts of distinct distances from individual points.
The team also published the Lean proof for Erdős Problem 653 and a separate PDF paper.
Why Lean Verification Matters
Conjectures is built around a specific premise: open mathematical problems can be turned into exact Lean statements, and independent participants can compete to submit proofs or counterexamples that a machine can check.
Lean is a proof assistant. Instead of relying only on prose arguments, a mathematical claim is formalized so that software can verify whether a submitted proof establishes the target statement. The hard part remains finding the proof, construction, or counterexample. The checking step, once the work is formalized correctly, can be comparatively fast and reproducible.
That structure is central to Conjectures’ role as a Bittensor subnet. The project publishes conjectures as fixed Lean targets, allows miners to use any model, agent, search strategy, or compute setup, and rewards submissions that pass validation. Conjectures, in this regard, is essentially a system where “the Lean kernel rather than a committee” settles whether a submitted proof holds.
The model does not make every mathematical result instantly self-explanatory. Human review is still important for understanding significance, presentation, authorship, and whether a result has been scoped correctly. Lean verification changes the baseline. A successful submission is an artifact that can be rerun against a formal statement rather than a persuasive sketch or a claimed proof.
Large models and automated agents can generate plausible but incorrect arguments. A proof assistant gives the workflow a stricter endpoint, because the result has to satisfy the formal checker rather than just read convincingly.
A Breakthrough Run for Bittensor-Based Proof Search
Many AI tasks are difficult to evaluate cleanly. Creative writing, research summaries, coding agents, and forecasting systems often require subjective grading or complex benchmarks. Mathematical proof has a different shape. Finding a proof may require creativity, domain knowledge, search, and compute, but a formalized proof can be checked against a precise target.
That makes the task heavily compatible with Bittensor’s subnet model, where independent operators compete to produce useful work. In Conjectures’ case, miners are rewarded for producing a valid formal artifact, regardless of effort, model choice, or process.
Tristan Hillerich
Conjectures’ latest two results follow its recent Erdős Problem 96 announcement, where miners found a Lean-verified construction showing superlinearly many unit distances in strictly convex position. That earlier result addressed a 66-year-old discrete geometry problem and came with both a formal proof and an explanatory paper.
In our coverage of the Problem 96 solution, we had written that the achievement was decentralized AI's swing back at OpenAI's solving of the Navier-Stokes Millennium Prize problem.
Now, with Conjectures pointing to two additional Erdős problems across graph theory and planar distance geometry, we're seeing Bittensor pull into the lead. In doing so, the commonly held belief that, on a long enough time horizon, centralized systems cannot compete with open-source, appears to be playing out now.
It's still early innings, but the results, at the very least, should convince you of this takeaway:
Bittensor, and perhaps even more broadly, open-source & decentralized AI, has found its mathematics champion.
