A proof of Nivat's conjecture
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-14-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-14-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-14-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'