Nivat's conjecture: an AI-found proof in Lean, and what understanding would add

On 28 October 2026, the mathematician Bryna Kra told the podcast Life, Automated that people she did not know had started sending her proofs of Nivat's conjecture, a problem on which she and Van Cyr proved one of the main partial results in 2012. "And they seem to be correct," she said, according to the episode's transcript. "The problem is solved, but without any understanding of what was going into it."

At least one candidate proof is public. The GitHub repository boonsuan/nivat holds a paper and a Lean formalization of the whole argument. Its README says: "The proof was found entirely by GPT-6 Pro, in response to my prompts," and "The Lean formalization and its accompanying documentation were produced by GPT-6 Astra Ultra in Codex." The formalization was registered on 14 September in Palomar, a registry of Lean formalizations. The README is also plain about what has not happened: the paper "has not been mathematically digested by humans".

So the question is a sharp one. What does a proof that passes a Lean check, but that no one has explained, give mathematics? Below: what the conjecture says and what was known before, what Kra said and wrote, what is in the repository, what its Lean proof establishes, and what "understanding" would add. Every source was checked on 30 October 2026. We found no published check of this proof by a named expert, and Papex does not assess it.

What is Nivat's conjecture?#

It says that a small amount of local variety forces a global repetition. Kra described it in a September guest post on Terence Tao's blog:

"Imagine an infinite grid of square tiles, with each tile colored either red or blue. Look at every rectangular window of a fixed size, say n tiles wide and m tiles high, and count how many different color patterns show up in that window. The conjecture says that if there are at most nm such patterns, then the entire coloring repeats under some fixed, nonzero shift of the grid."

Any finite set of colors is allowed; red and blue are an illustration. The number of patterns is called the pattern complexity. "Repeats" means that one nonzero shift leaves the whole coloring unchanged; it need not repeat in two independent directions.

Two small examples show why the threshold sits exactly at the area of the window:

• Stripes. Color the columns alternately red and blue. A window of two or more tiles shows only two different patterns, depending on whether it starts on a red or a blue column. The coloring repeats if you shift it one row up.
• One odd tile. Color every tile blue except one red tile. A window either misses the red tile (one pattern, all blue) or contains it in one of its nm positions. That makes nm + 1 patterns, and the coloring never repeats, because every shift moves the red tile.

So one pattern more than the area already allows a coloring that never repeats. The conjecture says that at the area or below, this cannot happen.

In one dimension the corresponding statement is a classical theorem. As the abstract of Cyr and Kra's 2012 paper recalls it, the Morse–Hedlund theorem (1938) says that an infinite row of symbols is periodic if and only if, for some n, it has at most n distinct blocks of length n. Nivat's conjecture asks for the same in two dimensions, with rectangles in place of blocks. Maurice Nivat proposed it at the ICALP conference in 1997, according to Wikipedia, and Jarkko Kari and Etienne Moutot describe it as "Open since it was stated in 1997".

What was known before September 2026?#

Partial results, from two directions: Cyr and Kra's, through dynamical systems, and Kari and Szabados's, which in Kra's words viewed "the combinatorial question as an algebraic object, using certain types of polynomials to find the infinite patterns." The main results, by the year each was first posted:

Kra's post explains why the two directions mattered: "Two different methods to approach the same problem seemed to shout to us: find the conceptual bridge between them. We tried, without success, and moved on to other problems." In her words, "the conjecture resisted our efforts for nearly three decades."

What did Bryna Kra say on Life, Automated?#

The episode, "Is Math a Canary in the AI Coal Mine? (with Bryna Kra)", is dated 28 October on KQED's site. Life, Automated is produced by the Ryan Institute on Complexity at Northwestern's Kellogg School of Management and distributed by KQED; the host is Jess Love. Kra is a Northwestern mathematician and, as the page notes, a former president of the American Mathematical Society. The page carries a transcript with this note: "This is a computer-generated transcript. While our team has reviewed it, there may be errors." The quotes below are from that transcript.

How the proofs arrived. "So starting a few weeks ago when there were new models released by the AI companies, those of us who'd worked on it began to receive proofs. And the proofs came from people who none of us knew. That's great. You know, mathematicians tend to welcome new people into the field."

What was missing. "Well, they were very bad at tracing where the results came from. You know, what they were using from previous results. They didn't highlight what was novel, which when you come to a breakthrough, you really want to write in the introduction, 'This is what's new.'" And: "It's sort of putting everything on equal footing." Then comes the line quoted at the top of this post.

Asking the authors. "I wrote back to these people, and I asked, you know, 'Would you like to meet and explain the proof?' There was always a reason why not." And: "One of them disclosed full AI use. That's fine. You know, they disclosed what they did. They said they were undergraduates who didn't really know much math." That is one sender, by Kra's account. The episode names no one and links no proof.

What she fears. "What it did is close off this area. What's the incentive now for somebody to go through and understand that? Unless it's gonna lead somewhere new."

She is not describing a refusal to use AI. In the same episode: "I use it if there's something I'm reading and I don't understand. It's a fantastic way to ask it, like, 'Explain how you get from this statement to that statement.' It's really good at that."

What did she write on Terence Tao's blog in September?#

Her guest post, "Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system.", went up on 13 September:

"This week I received several purported proofs of the full conjecture from researchers making their first foray into the subject. Some acknowledged using AI, but only for polishing the English or checking the proof. When I asked if the authors would meet over Zoom to explain their arguments, none accepted the invite."

She separates checking from understanding: "But merely disclosing AI use and checking correctness of the proof, both of which are essential, miss the point. Suppose these results are correct. That is a mathematical contribution. Yet it opens more questions. What did we learn? What did the authors contribute? What impact will this result have?"

And what a proof is for: "A proof is more than a certificate that something is true. Instead, it is a story, a picture, an insight, an explanation."

The post welcomes AI-produced mathematics ("I welcome AI-generated proofs and believe that human-only proofs will become rare") and asks for a change in what gets credited: "Producing a paper is no longer enough: authors must be able to explain the proof's mechanism and how they arrived at this point. Journals need to distinguish and credit the roles of discovery, proof, formalization and explanation."

The two accounts differ in one detail. In September, Kra wrote that the senders who acknowledged AI had used it "only for polishing the English or checking the proof". In October, she said one sender disclosed full AI use. Neither source says whether the two describe the same set of proofs.

What is in the boonsuan/nivat repository?#

The repository has been public on GitHub since 14 September. It holds a 13-page paper, "Pattern complexity and Nivat's conjecture", dated 14 September 2026, with GPT-6 Pro in its author line; its abstract opens "We prove Nivat's conjecture". It holds a Lean 4 formalization built on the mathlib library ("The 29 library modules contain 377 explicit declarations"), a metadata file, formalization.yaml, and logs of the checks. Since 27 September it also holds "Nivat's conjecture: an exposition of the GPT-6 Pro proof".

Who did what, as the repository states it (model names are as the repository gives them):

The maintainer is direct about his role: "As emphasized below, GPT-6 Pro found the proof; I did not. My role was prompting the model and arranging formal verification." And about his limits: "I am not an expert in this area. I do not regard myself as qualified to digest the argument properly or give it the exposition it deserves". The README invites others: "Experienced mathematicians who would like to understand, contextualize, simplify, or explain the proof are very welcome to do so."

On human checking, the 27 September update says of the exposition: "Like the original, it is AI-written and has not been checked by a human expert. As far as I am aware, there is still no human-digested account of the proof." The metadata file says: "No human expert review is claimed or documented." It also notes a limit of the record itself: "Proof-generation conversation transcripts are not included, so the attribution is a maintainer disclosure rather than a separately audited history."

On timing, a README update dated 14 September says Kra's guest post "went up around 3 hours before my first commit to this repository, though I completed the proof-generation and formalization work reported here before learning of the post." The blog's timestamp is 22:01 UTC on 13 September; GitHub records the first commit at 01:44 UTC on 14 September.

Is this the proof Kra received?#

We don't know, and no source we found says so. Kra names no sender and links no proof, in the episode or in the guest post. The README does not say that its proof was sent to Kra, and its maintainer, who calls himself "not an expert in this area", says nothing about whether he is a student. Kra wrote that she received "several purported proofs" in one week. The repository is one public candidate, not necessarily the proof from the undergraduates Kra described.

What does the Lean proof establish?#

The repository keeps the statement apart from the proof, following Palomar's convention. In the README's words, Challenge.lean "states it using only mathlib concepts, independently of the proof library", and Solution.lean "proves that same statement". In plain terms: for any finite alphabet and any coloring of the integer grid, if for some positive m and n the coloring shows at most mn distinct m-by-n patterns, counted over all positions, then some nonzero shift leaves the coloring unchanged.

Palomar's record says its mechanical verification passed on 14 September. According to Palomar's About page, its Comparator tool "verifies that the recorded formal proof proves the recorded formal statement", using only allowed axioms, and the proof is replayed through Lean's kernel and the independent kernels recorded in the entry; this entry names NanoDa. The README says the proof uses only Lean's three standard axioms, propext, Classical.choice and Quot.sound.

A passing check of this kind means one specific thing: the formal statement follows from Lean's foundations and mathlib's definitions. For that step, nobody has to trust the 13-page paper or the model that wrote it. It is narrower than it sounds. Four things stay with people:

1. Is the statement Nivat's conjecture? Palomar's automated editorial review, run by a language model, judged that "The selected theorem exactly expresses the advertised finite-alphabet rectangular-complexity implication and its single nonzero global-period conclusion." Palomar is plain about what that review is: "It does not accept, approve, or endorse a result. Palomar adds no human editorial step: no one here reads the mathematics the way a referee would." Palomar's report counts 40 lines in Challenge.lean, short enough for a specialist to read without reading the proof. We found no public report that one has.
2. The fine print of the definitions. The statement counts patterns with mathlib's Set.ncard, which, in mathlib's own documentation, "takes the junk value of zero if s is infinite". The Challenge file explains why that is harmless here: "The finite alphabet and finite rectangle make this pattern set finite, so its natural cardinality has the intended counting meaning." Details like this are what a statement audit is for, and the README asks for "independent statement audits".
3. The paper. From the metadata: "Formal checking of the Lean statements does not validate every sentence of the informal manuscript."
4. What is new, and whose it is. The metadata says that "no originality or priority assessment by a human expert is claimed", and the attribution to GPT-6 Pro rests on the maintainer's disclosure.

Palomar also checked one commit only, a 14 September build for Lean 4.33.0, of which it keeps an archived copy; the main branch has changed since.

None of this tells a reader why the theorem is true.

What would "understanding" add?#

The README borrows a vocabulary from Terence Tao: "generation, verification, and digestion". A summary of Tao's views, which the page says Claude drafted and Tao reviewed, defines digestion as "understanding, contextualizing, and explaining a result". The README places the project in that scheme: "This project addresses the first two activities and does not claim to have completed the third."

For Nivat's conjecture, a digestion would answer the questions Kra keeps asking.

What is new? Kra said the proofs she received "didn't highlight what was novel". The GPT-6 Pro paper sketches its route in its abstract: after labeling the alphabet by rational numbers, "we induct on rectangle area", applying a polynomial in the grid shifts, until "The induction reduces the conjecture to the case where a product of two difference operators annihilates c, which was proved by Szabados." Szabados's 2017 paper, in its own words, "combines the algebraic approach of Kari and the author with balanced sets of Cyr and Kra". Whether the new argument is the "conceptual bridge" Kra and Cyr looked for, or a different route, is a question for specialists. We found no public answer.

Where did it come from? Kra said the proofs she received "were very bad at tracing where the results came from". This repository does record its sources: its metadata marks Kari and Szabados's paper and Szabados's paper as work it "adapts", and Cyr and Kra's as "background". Whether that account is right is again for people who know the field.

Who can answer questions? In her guest post, Kra counts "the ability to respond to questions" as part of what human authorship means. The maintainer says he is not qualified to digest the proof. An AI-written exposition exists, and whether a model's explanation can do the work of digestion is an open question. Kra uses AI to explain steps herself, and she also says that "the role for human understanding and human use of this mathematics is extremely important".

Who will do it? Her guest post names the obstacle: "Careful verification and stellar exposition will not happen when there is no reward for those tasks."

Claimed, verified, explained: where does it stand?#

Our earlier post described how discovery, verification and explanation now arrive separately, from different people and tools, on different dates. As the sources state it on 30 October:

Where to follow it#

Nivat's conjecture is not on the list of open problems Papex tracks, and we have not added a claim for it. Papex lists the AI-assisted claims made about the problems it does track at papex.org/ai-claims, each as its source states it, with links. For Nivat, the places to watch are the repository, which asks for statement audits and exposition, and its Palomar entry.

Open questions#

Some questions this case raises, which we don't think have settled answers yet:

• Who should read the formal statement of an AI-found proof, and where should that reading be recorded so that others can rely on it?
• Can an AI-written exposition count as digestion, or does digestion need a person who can answer questions about the proof?
• How should credit be divided between the person who prompted, the models credited with finding and formalizing the proof, and whoever eventually explains it?
• When generation transcripts are not kept, attribution is, in this repository's words, "a maintainer disclosure rather than a separately audited history". What should be kept at the time the work is done?

The repository is open about what the models did, what the maintainer did, what the checks cover and what no one has done yet. Kra's guest post says why the last part matters: "We advance mathematics not by what we write, but by what we learn, check, apply, and teach others."

Sources#

• Is Math a Canary in the AI Coal Mine? (with Bryna Kra), Life, Automated (KQED, 28 October 2026), page and computer-generated transcript, checked 30 October 2026
• Bryna Kra, "Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system." (guest post on Terence Tao's blog, 13 September 2026), checked 30 October 2026
• boonsuan/nivat, README (GitHub), checked 30 October 2026
• boonsuan/nivat, formalization.yaml, checked 30 October 2026
• boonsuan/nivat, STATUS.md, checked 30 October 2026
• boonsuan/nivat, Challenge.lean and Solution.lean, checked 30 October 2026
• Pattern complexity and Nivat's conjecture (paper/nivat.tex, dated 14 September 2026, author line GPT-6 Pro), checked 30 October 2026
• Nivat's conjecture: an exposition of the GPT-6 Pro proof (paper/exposition.tex, dated 27 September 2026, author line Claude Opus 5.5), checked 30 October 2026
• boonsuan/nivat, commit history (GitHub), checked 30 October 2026
• Palomar entry PALOMAR-2026-09-14-000003, version 1, with its entry record and published review, checked 30 October 2026
• About Palomar (Palomar registry), checked 30 October 2026
• Mathlib, Mathlib/Data/Set/Card.lean (GitHub), checked 30 October 2026
• Van Cyr and Bryna Kra, Nonexpansive Z^2 subdynamics and Nivat's conjecture (arXiv:1208.4090, 2012), checked 30 October 2026
• Jarkko Kari and Michal Szabados, An Algebraic Geometric Approach to Nivat's Conjecture (arXiv:1605.05929, 2016), checked 30 October 2026
• Michal Szabados, Nivat's conjecture holds for sums of two periodic configurations (arXiv:1710.05360, 2017), checked 30 October 2026
• Jarkko Kari and Etienne Moutot, Decidability and Periodicity of Low Complexity Tilings (arXiv:1904.01267, 2019), checked 30 October 2026
• C. F. Colle and E. Garibaldi, A Modular Structure Theorem for Minimal Periodic Decompositions and Periodicity of Configurations with P(4,n) ≤ 4n (arXiv:2606.10193, June 2026), checked 30 October 2026
• Nivat's conjecture (Wikipedia), secondary source, checked 30 October 2026
• Terence Tao on AI in mathematics (and beyond), a living summary (tao-web, last updated 28 October 2026), checked 30 October 2026