Formally verified AI-led

Optimal packings of one to seven unit squares in a circle, proved in Lean

Machine-checked proofs of the smallest circle that holds $n$ unit squares, and of every packing that attains it, for $n = 1$ to $7$ ; for five, six and seven squares no earlier proof of optimality was known.

Lab: Independent
Model: ChatGPT (GPT-6 Pro) and Claude Opus 5 and 5.5
Field: Mathematics
Date: 2026-10-02
Human collaborators: The-Anh Vu-Le

Sources

Original work

GitHubvltanh/lean4-squares-in-circles↗

Independent commentary

erich-friedman.github.ioErich Friedman: Squares in Circles↗

What was found

The question is the least radius of a disk that holds $n$ non-overlapping unit squares, each free to move and rotate. The library proves the radii $\sqrt{2}/2$ , $\sqrt{5}/2$ , $5\sqrt{17}/16$ , $\sqrt{2}$ , $\sqrt{5/2}$ , $\sqrt{q^*}$ with $q^*$ a quartic irrational near $2.851$ , and $\sqrt{13}/2$ . The optimal packing is unique up to rotation and relabelling for $n \le 6$ ; for $n = 7$ the optimal packings form a family in which the three middle squares slide along their column. For three to seven squares the proofs place a small circle about the disk centre and count how much of it each square avoiding the centre must hold; for seven squares a pair theorem on the directions of neighbouring squares is by far the longest part. The repository reports that the arc idea came from Claude, that ChatGPT first applied it to five squares, and that the models wrote the proofs and all of the Lean code, with the owner directing and reviewing.

Novelty check

Read the repository's prior-work review, current to September 2026, and checked Erich Friedman's Squares in Circles page on 2026-10-06. One and two squares are folklore and four squares were Problem 6 of the 2026 International Mathematics Summer Camp. For three squares Montanher, Neumaier, Markót, Domes and Schichl (J. Global Optim., 2019) enclosed the radius by computer-assisted interval arithmetic, without an exact value or exact uniqueness. For five, six and seven squares the review finds no earlier proof: Friedman's page listed his 1997 packings only as the best known in its July 2026 snapshot, and now records three, five, six and seven squares as proved by The-Anh Vu-Le in September 2026. No earlier proof-assistant verification of any optimal packing of squares or circles in a circle was found. The year the question was first posed is left unrecorded rather than guessed.

Caveats and known objections

Not peer-reviewed, and there is no paper; the proofs are written up as a textbook inside the repository. Graded formal on the Palomar registration, which checks the proofs against a separate statement file importing only Mathlib and replays them through three kernels. What that certifies is the statement in that file: the kernel checks the proofs, not that the definitions of square, disk and packing capture the intended problem, and no outside audit of those definitions was found. For seven squares, uniqueness holds only up to the heights of the three middle squares. The four-square uniqueness argument matches an unpublished July 2026 note by Wei Zhao that was also developed with Claude, and the repository itself says the two may not be independent. Autonomy is ai-led rather than autonomous because the owner directed and reviewed the work.

Machine-checked elsewhere

PalomarPALOMAR-2026-10-02-000002

vltanh/lean4-squares-in-circles at 621f2340a12f · checked 2026-10-02

ProvedSquaresInCircles.optimal_radiusSquaresInCircles.optimal_packings

A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.

Registered against Challenge.lean, which restates the definitions of Geometry.lean word for word and states both theorems with sorry. Permitted axioms are propext, Classical.choice and Quot.sound.

Nobody outside the lab has checked this yet.

Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.

Submit a check Challenge the grade

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-06AddedEntered the registry graded Formally verified and AI-led.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Community discussion

reddit.comReddit r/math: AI in mathematics, October 3, 2026↗

Graded formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Optimal packings of one to seven unit squares in a circle, proved in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-02-squares-in-circle-packings

BibTeX

@misc{whataifound-independent-2026-packings,
  title        = {Optimal packings of one to seven unit squares in a circle, proved in Lean},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-10-02-squares-in-circle-packings}
}

Related findings

ClaimedHamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjectureIndependent · 2026-09-26 ClaimedHuang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputsAxiom Math · 2026-09-17 ClaimedBrowning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literatureAxiom Math · 2026-09-16

discrete-geometry packing lean formalization argument

← All mathematics findings in the registry