The Erdos-Borwein Constant is 2-Dense
Is the Erdos-Borwein Constant 2-Dense?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Analytic number theory; digit distribution of constants
- Posed by
- Richard E. Crandall
- Year posed
- 2002
- Years open
- 24y
- Solved
- 2026-09-07
- Model
- ChatGPT-6 Astra
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 25 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
This work proves that the Erdős–Borwein constant's binary expansion contains every finite binary sequence as a consecutive block, each occurring infinitely often. This implies that the Erdős–Borwein constant is 2-dense.
Verification
The Lean development proves disjunctivity of the binary expansion conditional on two hypotheses supplied as theorem arguments, not as axioms: AGP, the Alford-Granville-Pomerance estimate in the form of Vandehey's Proposition 2.1, and PrimeIntervalSupply, a standard prime number theorem consequence bounding the primes in (L, 2L) below by L/(3 log L). Both are published theorems rather than conjectures, so the mathematics is conditional only on known results; neither is formalized here. Read directly from lean/ErdosBorwein/PrimeInputs.lean on 8 September 2026. The audited endpoints depend on propext, Classical.choice and Quot.sound only. Because the statement is the author's own rather than anchored to a canonical tracker, and because what the kernel certifies is the implication, this takes the statement-unaudited tier. No specialist in analytic number theory has read the argument.
Sources
Submitted by nufrogcaca on