Conjectures, Bittensor’s subnet 66, has published a paper, Lean proof and review record for a claimed negative answer to Erdos problem 96. The team announced the result on September 14, attributing the construction to its miners.
The paper names Liam Kruer and Jensen Kohlmeyer as authors. Its accompanying Lean source credits OpenAI Codex with substantial assistance in the mathematical work and preparation, while assigning responsibility to the authors.
The question behind the proof
Imagine points arranged as the corners of a convex polygon. How many pairs of those points can sit exactly one unit apart as the polygon grows?
The proposed linear bound would keep that count proportional to the number of vertices. Kruer and Kohlmeyer’s working paper describes a family of strictly convex configurations whose ratio of unit-distance pairs to vertices grows without bound. That is the basis of their negative answer. The paper leaves the optimal growth rate open.
For Bittensor, the concrete output is unusually inspectable: a mathematical argument, its formal source and a record of the checks applied to it. Readers can examine what the subnet says it produced beyond a performance score.
Three dates in the record
Conjectures records verification on September 10, an approval decision on September 11 and certification on September 14. The announcement therefore marks the public result package after those earlier checks.
Its result page describes a replay against a pinned task and Lean toolchain. The published record lets readers separate the mathematical claim, the accepted artifact and the project’s review decision. Each answers a different question about the work.
Limits and verification
Verification and certification are reported by Conjectures. Tao Outsider has read the public material and has not independently replayed the proof. The project records no second-kernel check, limited provenance-search coverage and no guarantee of originality. Its reward-paid label also remains a project report. A TaoSwap snapshot on September 15 listed one active miner on SN66.
Sources
Conjectures announcement, September 14
Result and verification record
Kruer and Kohlmeyer’s working paper
Published Lean source and authorship disclosure
Was this article useful?
One tap feedback helps us improve each post.
