AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A translational tile with no fully periodic tiling in dimension three

Can the mathematical statement in A translational tile with no fully periodic tiling in dimension three be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 155)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A translational tile with no fully periodic tiling in dimension three'. We construct a finite translational tile in ℤ3 that admits tilings but no fully periodic tiling. Its unit-cube thickening has the same property in ℝ3, even when arbitrary real translations are allowed. This gives a negative resolution of the periodic tiling conjecture in dimension three.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 155). The Lean development was not rebuilt locally.