What was already known
Erdős, Hajnal and Szemerédi had a linear-error almost-half bound. The arbitrary slowly growing additive-error question was open; Stiebitz’s chromatic theorem is a prior input.
AI involvement
Przemek Chojecki and GPT-5.5 Pro are credited as coauthors. Chojecki presents the argument; paws and plby later formalized its construction and Stiebitz input.
GPT-5.5 Pro is credited as an author of the mathematical note; no log shows the little-human-input independence needed for AI-autonomous.
Importance
The construction answers the arbitrary-additive-error question and strengthens the local graph property.
Limitations
The original note does not separate Chojecki’s and GPT-5.5 Pro’s discovery steps. A later Lean file reports a matching theorem, including the Stiebitz input.
Technical verification
A later Lean file states the nonnegative-function version of the same claim and reports only Lean's standard foundational axioms; its conditional construction and Stiebitz theorem are both proved there. This is a third-party, source-reported machine check, not a build reproduced here.
Formal checking
Lean proof of erdos_750_independence and erdos_750, including the previously assumed Stiebitz lower bound
- Checker
- Lean 4, formalizations by paws and plby, vendored by Jayyhk
- Scope
- Erdős #750 for every nonnegative real-valued f tending to infinity, via the infinite-chromatic local odd-cycle-transversal construction
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The note explains the projection inequality, postponement of apex odd cycles, finite profile induction, and disjoint-union argument.
Correction and publication history
The construction answers the arbitrary-additive-error question and strengthens the local graph property.
Read this published revision