{"id":"palomar/PALOMAR-2026-09-14-000003","url":"https://github.com/boonsuan/nivat/tree/0d94547e934418c9d1b75fcbb7d6af493e86759d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-14-000003-v1.json","repo":"https://github.com/boonsuan/nivat","tags":["math.DS","math.CO","msc:37B10","msc:68R15","symbolic-dynamics","lean","combinatorics-on-words"],"score":0,"title":"A proof of Nivat's conjecture","trust":"high","domain":"math.DS","source":"palomar","authors":["Boon Suan Ho"],"reviews":0,"subject":"math.DS","summary":"A Lean+mathlib proof of Nivat's conjecture: Given a finite alphabet A, we consider configurations c: Z^2 -> A, which are arbitrary maps that can be thought of as colorings of the 2D lattice. Writing P_c(m, n) for the number of distinct m-by-n block patterns occurring in a configuration c, Nivat conjectured that if P_c(m, n) <= mn for some positive m and n, then c is periodic; that is, there exists nonzero h such that c(v+h) = c(v) for all v. The proof is due to GPT-6 Pro.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-14","reactions":{},"formalized":true,"formalizes":[{"title":"Pattern complexity and Nivat's conjecture","identifier":"paper/nivat.tex","relationship":"formalizes"},{"title":"An Algebraic Geometric Approach to Nivat's Conjecture","identifier":"https://arxiv.org/abs/1605.05929v1","relationship":"adapts"},{"title":"Nivat's conjecture holds for sums of two periodic configurations","identifier":"https://arxiv.org/abs/1710.05360v1","relationship":"adapts"}]}