Conjectures Miners Prove Erdős 1062(ii) Density Is Irrational in Lean

Conjectures, the Bittensor subnet focused on formal mathematics and Lean verification, says its miners have solved part of Erdős Problem 1062 by proving that a long-studied divisibility-density limit is irrational.

The subnet announced the result on X, saying miners found a Lean-verified proof for Problem 1062(ii), a question that has remained open since at least Richard Guy's 1994 statement in Unsolved Problems in Number Theory. The public submission is credited to miner handle JenW1N, while an accompanying exposition paper lists Liam Kruer and Jensen Kohlmeyer as authors.

The result centers on the limiting density of the largest "fork-free" subsets of $\{1,\dots,n\}$. In plain terms, Conjectures says the proof shows that the limiting proportion of numbers that can be included in such a set is an irrational real number.

What Erdős Problem 1062(ii) Asked

The problem concerns a function $f(n)$, defined as the size of the largest subset of $\{1,\dots,n\}$ with a restriction on divisibility. A set is fork-free when no element in the set divides two distinct other elements in the same set.

That condition turns a simple-looking question about integers into a problem about how dense a subset can be while avoiding a particular divisibility pattern. For each value of $n$, $f(n)$ measures the maximum possible size of such a subset. The density question asks what happens to $f(n)/n$ as $n$ grows.

Davis proved in April 2026 that the limiting density exists and is computable, but the irrationality of that limit remained unresolved. Conjectures' new claim addresses that remaining part, with the subnet saying miners proved the limiting density is irrational.

Existence and computability establish that the density is a well-defined value that can, in principle, be approximated. Irrationality is a stronger statement about the answer itself, because the limit cannot be expressed as a ratio of two integers.

Lean Verification Gives the Claim a Checkable Artifact

Conjectures published the Lean proof and result page alongside a PDF exposition dated Sept. 22, 2026. The paper records a SHA-256 hash of the accepted artifact, and the verification report shows Lean kernel acceptance with the permitted axioms propext, Quot.sound, and Classical.choice.

In formal mathematics, the Lean kernel can check a proof written in Lean, which reduces the role of trust in informal exposition and makes the submitted argument more directly auditable. Human explanation still matters, especially for understanding the strategy and importance of the result, but the formal artifact gives the claim a machine-checkable foundation.

Conjectures' model applies this to Bittensor. Instead of only rewarding miners for generating plausible mathematical text, the subnet routes miner competition toward outputs that can be evaluated against formal proof standards, where a successful submission must survive verification instead of relying only on subjective review.

What the Result Means for Conjectures and Bittensor

Conjectures' model appears to now be reaching escape velocity. This 1062(ii) solution is Conjectures' fifth Erdős problem solved in September (108, 653, 96, 859).

In the case of this 1062(ii), the work is tied to a public formal artifact, a verification report, and a problem with a documented place in the number-theory literature. That combination makes the output easier for the broader Bittensor ecosystem to examine than many AI-generated research claims, where the boundary between a useful conjecture, an informal argument, and a valid proof can be difficult to assess.

Conjectures' approach also shows a more concrete use case for decentralized AI incentives. Instead of measuring miners only on generic inference quality or benchmark scores, the subnet can direct competition toward specialized tasks where correctness is externally checkable. In this case, the target was a formal proof about the irrationality of a density limit. In other settings, the same general pattern could apply to theorem proving, code verification, or other domains where artifacts can be tested against strict acceptance criteria.

Expert review is still needed, especially around the mathematical exposition and the framing of the result. The public Lean artifact, source paper, and recorded hash give researchers and readers a clearer path to evaluate what was proved, who submitted it, and how the verification was accepted.