AI Proof WatchKeep up with AI contributions

GPT-5.5 Pro construction answers Erdős #38

A sparse set B that is not an asymptotic additive basis gives, for every A of Schnirelmann density 0<α<1 and every cutoff N, a shift b∈B for which A∪(A+b) covers at least (α+f(α))N of [1,N], with f(α)>0.

Sources for this record

What was already known

Erdős proved a gain when B is a finite-order additive basis and asked whether a non-basis can provide it at every cutoff.

AI involvement AI-autonomous

The forum announcement credits GPT-5.5 Pro with the construction after the problem was supplied; Liam Price cleaned the final manuscript.

The announcing primary forum post assigns the solution to GPT-5.5 Pro and only final PDF cleanup to Liam Price; no human mathematical input beyond posing the task is documented.

Importance Notable

Answers the single-shift non-basis question in the manuscript’s stated form.

Limitations

A community Lean formalization is reported, and Nat Sothanaphan checked its statement against the paper. His standard GPT screening is not a whole-proof human check. The stronger quantitative bound shown on the problem page is not established by the linked manuscript.

Technical verification Formal (Lean 4 (Aristotle community formalization))

The forum reports Aristotle's autoformalization and links a community Lean proof of the same density-increment construction; Nat Sothanaphan checked statement correspondence. The FormalConjectures file alone is a sorry placeholder and is not treated as the proof. This review did not build the community file.

Formal checking

Positive Erdős 38 single-shift construction using an asymptotic additive-basis definition and explicit positive f(alpha); Source-reported Lean 4 autoformalization in Erdos38.lean, with Nat Sothanaphan's later statement-match review

Checker
Aristotle (Harmonic), formalization shared by Matteo Del Vecchio
Scope
Positive Erdős 38 single-shift construction using an asymptotic additive-basis definition and explicit positive f(alpha)
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

The record has a GPT-based screening and a statement-match comment, but no named human explanation of the sparse dyadic-shift mechanism; Few is the documentation default.

Correction and publication history