Nivat's conjecture claimed in its sharp form, with the submitter stating he cannot check it
A Lean development claims Nivat's 1997 conjecture in full: if a two-dimensional configuration has at most mn distinct patterns on some m by n rectangle, it has a nonzero period.
- Lab
- Independent
- Model
- GPT-6 Pro (proof); GPT-6 Astra Ultra through Codex (Lean formalization)
- Field
- Mathematics
- Date
- 2026-09-14
- Human collaborators
- Boon Suan Ho
- Problem posed
- 1997 · open 29 yrs
What was found
Nivat conjectured in 1997 that low rectangular pattern complexity forces periodicity in a two-dimensional configuration. Partial results are known under stronger complexity bounds; the sharp mn form has stood. The repository separates Challenge.lean, which states the result in mathlib terms alone, from Solution.lean, which proves it, and carries a Palomar registration. The submitter's disclaimer is the unusual part and is quoted in the caveats: he says the proof is entirely the model's and that he is not qualified to check it.
Novelty check
The conjecture dates to 1997 and is a named open problem in symbolic dynamics, still described as open in the literature the repository cites. No competing resolution of the sharp form appears in the four registries the watch sweep diffs. The repository itself notes that Bryna Kra published a guest post on Terence Tao's blog discussing Nivat's conjecture and AI-generated mathematics roughly three hours before its first commit, and states the proof work was complete before the author saw that post; the two are independent, and neither is evidence about the other.
Caveats and known objections
Nobody has checked this, and the submitter says so first. His disclaimer reads: the proof was found entirely by GPT-6 Pro in response to his prompts, the paper was written by AI and has not been mathematically digested by humans, and he does not regard himself as qualified to digest the argument or give it the exposition it deserves. His stated role was prompting and arranging formal verification. That is a clearer disclosure than most entries here carry, and it is also the reason the grade is claimed rather than formal: a Palomar registration establishes that the Lean typechecks against the recorded statement, not that the statement is Nivat's conjecture. Autonomy is ai-led rather than autonomous because a human chose the problem and drove the prompting.
Machine-checked elsewhere
PalomarPALOMAR-2026-09-14-000003
boonsuan/nivat
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Nivat's conjecture claimed in its sharp form, with the submitter stating he cannot check it. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-14-nivat-conjectureBibTeX
@misc{whataifound-independent-2026-conjecture,
title = {Nivat's conjecture claimed in its sharp form, with the submitter stating he cannot check it},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-09-14-nivat-conjecture}
}