Table of Contents
Conjectures says its miners have found a solution to Erdős Problem 96, a discrete geometry problem that had remained open for more than 66 years.
The team announced the result on X, saying the solve disproves the conjectured linear bound for unit-distance pairs in convex polygons. The construction, according to Conjectures, produces strictly convex polygons with superlinearly many pairs of vertices at distance one from each other.
Conjectures also published the full Lean-verified proof and an accompanying paper by Liam Kruer and Jensen Kohlmeyer.
The paper states that for every integer d ≥ 2, the authors construct a finite set in the Euclidean plane, in strictly convex position, with enough unit-distance pairs to show that the maximum number of such pairs in a convex n-gon is not O(n).
Just a week ago, the world marveled at OpenAI’s solving of the Navier-Stokes Millennium Prize problem. Today, we have a similar feat coming out of the Bittensor ecosystem representing decentralized AI's swing back. Truly remarkable.
What Is Conjectures?
Conjectures is a Bittensor subnet focused on formal mathematics. The subnet publishes unsolved mathematical conjectures as exact Lean statements, lets independent participants use any model, tool, or compute strategy they want, and rewards successful submissions that pass verification.
Lean is a proof assistant that lets mathematical claims be written in a form that software can check. In open mathematics, the difficulty lies both in finding a convincing argument and in establishing that the argument proves the exact statement in question.
Conjectures is built around that asymmetry. Finding a proof or counterexample can require significant creativity, search, and compute, while checking a properly formalized proof can be comparatively fast. The subnet uses that structure to turn proof discovery into a competitive task. Miners search for solutions, validators check submitted Lean files against a pinned toolchain, and accepted work can be reviewed before rewards are released.
The project’s goal is settling decades-old open questions through public, rerunnable proofs, which sets Conjectures apart from many AI benchmarks. A successful result like we have today becomes part of the mathematical record.
Why Erdős Problem 96 Matters
Erdős Problem 96 asks whether n points in the plane that form a convex polygon can determine only O(n) pairs of points at distance one from each other. The problem concerns how many equal-length edges can be packed among the vertices of a convex polygon as the number of vertices grows.
The problem sits in discrete geometry, a field concerned with configurations of points, lines, distances, and other finite geometric structures. Paul Erdős and collaborators studied many such extremal questions, often asking whether a simple-looking geometric restriction forces a strong upper bound.
The hoped-for answer was linear. A linear bound would mean that even as the polygon gained more vertices, the number of unit-distance pairs could grow only proportionally with the number of points. The new Conjectures result claims the opposite. There are strictly convex configurations where the number of unit-distance pairs grows superlinearly along an infinite family of examples.
The paper is careful about the scope of the result. It does not claim to determine the optimal growth rate for the problem. Instead, it gives a construction that is enough to rule out any eventual linear upper bound.
The result would not close every question about unit distances in convex position, but it would settle the specific Erdős Problem 96 formulation in the negative.
How the Construction Works
The proof builds convex point sets with many controlled unit distances by starting from a finite incidence pattern and amplifying it.
The paper describes a coordinate-incidence graph with two families of seed points and a set of edges between them. Each edge corresponds to a pair of points that can be made exactly distance one apart. The construction then uses rotations and subset products to create many copies of the seed configuration while preserving those unit-distance relationships.
Two geometric problems have to be solved for that amplification to count. First, the copied vertices must remain distinct. Second, all of the resulting points must stay in strictly convex position, meaning every point remains an extreme point of the convex hull rather than falling inside the polygon.
Kruer and Kohlmeyer's construction addresses those constraints through carefully separated seed radii, radial support margins, and small rotations that correct distance errors without breaking convexity. The proof then shows that the amplified configuration contains at least a fixed multiple of d times its number of vertices in unit-distance pairs, which is enough to defeat a universal linear bound.
The construction produces a family of strictly convex point sets whose unit-distance count grows too quickly for the original conjecture to survive.
A Bittensor Proof Search Result Arrives After OpenAI's Navier-Stokes Claim
Earlier this month, OpenAI said its AI agents solved the Navier-Stokes Millennium Prize problem, releasing a written proof and Lean formalization for one of the best-known open problems in mathematical physics. That claim drew major attention because of both the significance of the problem and the role OpenAI attributed to large-scale agent orchestration.
It also drew a dispute over research priority and attribution. NYU mathematician Tristan Buckmaster alleged that OpenAI pursued a similar approach after learning about work he had conducted with Levent Alpöge, an Anthropic researcher, and questioned whether the company’s systems had accessed transcripts of their work with OpenAI models. OpenAI denied using their prompts, proofs, or private transcripts, and said its models reached the result independently. The competing accounts remain unresolved, but the episode has raised broader questions about how AI labs protect confidential research and assign credit when models contribute to mathematical discoveries.
Conjectures is a very different system. Its submission process is designed to create a clearer record of priority. A miner first publishes a cryptographic fingerprint of the Lean file and reveals the file afterward, preventing another participant from seeing the submitted proof and claiming it first. The validator then checks the unchanged artifact against a pinned statement and toolchain, while accepted work is screened for material copied from the internet or an unmerged pull request before rewards are released.
That mechanism cannot eliminate every dispute over intellectual influence or underlying ideas, but it makes the submitted artifact, its timing, and its verification far more transparent.
In a field confronting difficult questions about AI-assisted research credit, Conjectures offers a model in which priority is recorded, the proof is publicly rerunnable, and rewards flow to the participant who submitted the verified result.
