What was already known
Cyr and Kra had proved periodicity at the stronger threshold P(m,n) ≤ mn/2. Kari and Szabados proved an asymptotic form, and Szabados proved the conjecture for sums of two periodic configurations. The general sharp threshold had remained an open conjecture for nearly three decades.
AI involvement
The maintainer explicitly says GPT-6 Pro found the proof in response to his prompts, while GPT-6 Astra Ultra produced the formalization. Ho prompted, directed the project and arranged verification; available documentation does not disclose enough prompt detail to label the result task-only autonomous.
Boon Suan Ho explicitly credits GPT-6 Pro with finding the proof in response to prompts and GPT-6 Astra Ultra with producing the Lean formalization; Ho prompted and arranged verification. Missing prompt transcripts prevent a task-only autonomy finding.
Importance
A source-reported formal proof of the full conjecture would settle a recognized problem at the intersection of combinatorics and dynamical systems. The proof combines algebraic and dynamical approaches, but its mathematical mechanism has not been digested by human experts.
Limitations
Boon Suan Ho credits GPT-6 Pro with finding the proof and GPT-6 Astra Ultra with the Lean formalization; Ho supplied prompts and arranged verification. The repository reports successful Lean, leanchecker, Comparator and NanoDa checks of the solution and imported proof library, with no admitted proofs. The public challenge statement is only a template. The paper-to-Lean correspondence was reviewed by AI agents, with no human expert review or mathematical digestion claimed. Bryna Kra reported other purported AI-era proofs arriving around the same time, so this record does not claim exclusive priority.
Technical verification
The repository reports successful Lean build, axiom audit and kernel replay for Nivat.nivat and matching NivatSubmission.nivat, plus Comparator and independent NanoDa acceptance. Solution.lean contains the completed theorem; Challenge.lean has a deliberate non-imported stub. AIProofWatch did not rerun these checks.
Formal checking
Project reports successful Lean build, kernel replay, axiom audit, Comparator and independent NanoDa check of matching challenge/solution statement; no admitted proof in imported modules.
- Checker
- Lean 4 kernel, leanchecker, Comparator and NanoDa as run by the project maintainer
- Scope
- Nivat.nivat and the matching NivatSubmission.nivat theorem for full-grid finite-alphabet configurations and some rectangular complexity at most area
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The maintainer positively reports that no human expert has mathematically digested the proof, including the later AI-written expository rewrite. This is a documented understanding gap despite completed machine checks.
Correction and publication history
Claim-level review of the exact Lean solution statement, reported complete checks, author attribution, earlier bound and contemporaneous claims; non-notifying local inclusion.
Read this published revision