Thue–Morse: all three Joshi–Rust first-occurrence formulas
Let t(j) be the parity of the binary digit sum of j, with indexing from zero. Let A(d) be the greatest length of a monochromatic arithmetic progression of positive difference d in t, and let i(d) be the least starting index attaining A(d). Joshi–Rust Conjecture 3.8 asks for the three first-occurrence identities: i(2^n+1)=3·2^(2n)−2^n−1 for n≥2; i(2^(2n)−1)=3·2^(4n)−2^(2n)+1 for n≥1; and i(2^(2n+1)−1)=2^(2n+1)−1 for n≥0. The ranges are explicit: the first formula excludes n=1, where the previously recorded value is i(3)=45.
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Combinatorics on words; automatic sequences and arithmetic progressions
- Posed by
- Gandhar Joshi and Dan Rust, Monochromatic arithmetic progressions in the Fibonacci, Thue–Morse, and Rudin–Shapiro words (2025), Conjecture 3.8; arXiv:2501.05830v2, DOI 10.1016/j.tcs.2025.115391.
- Year posed
- 2025
- Years open
- 1y
- Solved
- 2026-10-04
- Model
- OpenAI Codex
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 6 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
All three displayed first-occurrence families are proved in the stated ranges. The proof also gives exact all-start classifications for the plus and even-minus families, and rederives their established maximal-length values without assuming those values as hypotheses. For q=2^m, m≥2, every length-(q+2) progression at difference q+1 starts at lq²−q−1 with l≥1 and t(l−1)=t(l+1)=1−t(l). For even m≥2, every length-(q+4) progression at difference q−1 starts at lq²−q+1 with the same condition. Its least l is 3. For odd m, the earliest length-q progression at difference q−1 starts at q−1. Global maximality and exclusion of every earlier start are included. The prior length results and block-recognition methods of Parshina and Aedo–Grimm–Nagai–Staynova are explicitly credited. This is the first-occurrence conjecture, distinct from the existing avoiding-population matching-height entry. Broader all-difference classifications are not claimed. Worldwide novelty remains unassessed.
What the AI did
dot (OpenAI) developed the uniform all-start carry/desubstitution argument, translated the complete proof into Lean, and prepared the exact source/build/axiom certificates. Separate AI checks examined the hand proof, formal statement semantics, and final imported artifacts. This disclosure concerns substantive proof discovery and formalization; it does not claim human expert endorsement.
Verification
Read by this site on 4 October 2026, not rebuilt. Seven modules, mathlib, Lean 4.33.1. No sorry, admit, axiom declarations, native_decide, opaque or unsafe in the source modules. Definitions checked by hand: t is the recursive digit-sum parity, A(d) and i(d) are global sSup and sInf with attained maxima and exclusion of every earlier start proved, and the three headline theorems state Conjecture 3.8 as printed, with the submitter's ranges (the first formula fails at n = 1). The package's axiom log lists only propext, Classical.choice and Quot.sound. The repository has no CI; the build receipt is the author's own log. The three formulas were also checked numerically here for d = 1, 3, 5, 7, 9, 15, 17, 31, 63. The informal-to-formal review in the package is by the same AI agent.
Sources
Submitted by ZestyDingo473 on