Conjectures.io bounty platform pays out for Lean proofs of Erdős #859, #18(b), #1062(ii) and Ben Green's problems 24, 39, 40 within ten days, mostly to Purdue's 'JenW1N'

2026-09-25★★★after cutoffscienceConjectures.ioOpenAIconfidence: medium

Between Sept 15 and Sept 25, 2026, Conjectures.io paid bounties for machine-checked Lean proofs of seven formalised open problems. The platform runs on Bittensor subnet 66, publishes open problems as pinned Lean statements and pays in its alpha token after a kernel check and human review. Six of the seven went to "JenW1N" (Purdue students Jensen Kohlmeyer and Liam Kruer): Erdős #108 (see its own entry), #18(b), #859, #1062(ii), and Green's open problems 24 and 40. Green's problem 39 went to "Jordan". Proofs run to 14k–74k lines of Lean, and the JenW1N submissions credit OpenAI ChatGPT/Codex. By Oct 5 the platform listed 26 problems solved and about $128–130k paid. erdosproblems.com still marked #18, #859 and #1062 as open, with pending proof claims, so expert acceptance is not yet established.

Key facts

Results page (Oct 5, 2026): 26 problems solved, 33 verified proofs, $129,963 (127,226.57 α) paid, 257 live bounties; two submissions rejected (Erdős #70, #252) as already solved/formalised; Erdős #579 (by 'Jordan', Oct 3) pending review. (The lead recorded $127,713 earlier the same day; the total moves with the token price)
Erdős #18(b), JenW1N, Sept 16, $3,232: proves h(n!) < n^ε for every ε > 0 and large n (h(m) = number of divisors needed to represent every 1 ≤ k < m as a sum of distinct divisors of a practical m); Lean file 14,043 lines. Erdős had shown h(n!) < n
Erdős #859, JenW1N, Sept 18, $3,820: the density d_t of n for which t is a sum of distinct divisors of n satisfies d_t ~ c₁/(log t)^c₂ (Erdős 1970 had only bounds of this shape); Lean file 36,197 lines
Erdős #1062(ii), JenW1N, Sept 21, $4,007: on fork-free subsets of {1,…,n} (no a | b and a | c), whether lim f(n)/n is irrational (Guy's problem B24); Lean file 74,209 lines; the page itself notes that 'a complete ordinary-kernel check and target axiom audit are still required'
Green's open problem 24, JenW1N, Sept 25, $4,247: a (1/3 + o(1))n² asymptotic from Ben Green's list of 100 open problems; 52,946 lines of Lean; disclosure: 'OpenAI ChatGPT/Codex assisted with the mathematics, certificate generation, Lean formalization, verification, and presentation'
Green's open problem 40, JenW1N, Sept 15, $4,436; Green's open problem 39, 'Jordan', Sept 19, $2,793
Platform model: 'checking a proof takes seconds where finding one can take months'; accepts proofs made with 'any AI, tool, or method'; payment only after Lean kernel check against the pinned statement plus human review for gaming or plagiarism
erdosproblems.com on Oct 5, 2026: #18 OPEN with 3 proof claims, #859 OPEN with 1 proof claim, #1062 OPEN with 1 proof claim, #579 OPEN with none

Science result

Field: mathematics / number theory (divisors, practical numbers) / combinatorics
Problem: Erdős problems #18(b), #859, #1062(ii) and Ben Green's open problems 24, 39, 40, as formalised on Conjectures.io
Result: Lean 4 proofs accepted and paid by Conjectures.io; see key facts for each statement
AI system: ChatGPT, Codex
Human role: AI-assisted: student solvers using ChatGPT/Codex for mathematics, certificates and Lean (disclosed for #108 and Green 24; not stated on every solution page)
Verification: Lean kernel check against pinned bounty statements plus platform human review; no peer review; erdosproblems.com has not yet marked them solved
Status: pending
Why surprising: Decades-old Erdős questions settled as tens of thousands of lines of AI-assisted Lean, paid by a crypto bounty before any mathematician wrote them up.

What happened

After the Erdős #108 disproof (Sept 15), the same two-person Purdue team kept claiming Conjectures.io bounties. They took several number-theory problems on divisors and practical numbers that Erdős posed in the 1970s, plus three problems from Ben Green's list. Each solution is a single Lean file checked against the platform's pinned formal statement, and the platform describes it in a write-up. Rewards were paid in Bittensor alpha, worth about $2.8k–4.4k per problem.

We read the solution pages through a summarising fetcher. Exact statements, especially the precise formal form of #1062(ii) and Green 24, should be checked against the pinned Lean targets.

Why it matters

A crypto-funded bounty market is now paying for formal proofs of open problems, and AI-assisted solvers are collecting the payouts in days. The Lean check guarantees that the pinned statement was proved. It does not guarantee that the statement matches what Erdős or Green meant, or that mathematicians find the proof illuminating. Graph theorists raised the same complaint about the #108 write-up. Watch whether erdosproblems.com accepts the claims.

Changelog

2026-10-05: created (leads run; lead from conjectures.io/results). Confidence medium: statements summarised from platform pages, no expert confirmation yet

People

Jensen Huang

Related events

Sources (8)

id: 2026-09-25-conjectures-io-erdos-green-bounty-solves · updated 2026-10-05 · open in the interactive timeline