Nivat’s rectangular-complexity periodicity conjecture

The question is whether every finite-alphabet configuration c:Z²→A with P_c(m,n)≤mn for some positive m,n has a nonzero global period. Here P_c(m,n) counts the distinct m×n rectangular blocks occurring in c.

Why it matters and what counts as progress

Why it matters: It asks whether one low rectangular-pattern complexity bound forces a global period in every two-dimensional symbolic configuration.

What counts as progress: Prove a nonzero global period from one low rectangular-complexity bound for every configuration, not only recurrent or uniformly recurrent subclasses.

How the problem developed

1997 · Conjecture [1]
Maurice Nivat Conjectured that a two-dimensional finite-alphabet configuration with at most mn distinct m-by-n rectangular patterns must be periodic.
2020 · Partial result [2]
Ján Kari and Michal Szabados Proved periodicity under the stronger complexity bound at most half the rectangle area, leaving Nivat’s full threshold open.
14 Sept 2026 · Reported proof [3]
Boon Suan Ho; GPT-6 Pro generated the proof and AI drafted the paper, while GPT-6 Astra Ultra produced the Lean formalization The public project reports a proof of Nivat’s full rectangular-complexity conjecture and a Lean formalization.