What was already known
Candidate configurations were known; earlier proofs, computational bounds, and uniqueness results vary by square count.
What changed and why it matters
Advances the stated target relative to the recorded baseline.
The AI contribution
The repository attributes proofs and Lean code to ChatGPT and Claude, with its owner directing and reviewing the work.
Limitations
The small cases include formalization of known results; the claimed new optimality proofs for five through seven are distinguished from numerical constructions. Statement fidelity and checking scope require review; AIProofWatch has not rebuilt Lean.
Verification evidence
Evidence labels show what supports the claim. Importance rates its impact if correct.
Author claim
The pinned repository description states the result and AI provenance.
Accessible artifact / proof
Statements, proofs and checking configuration are available.
Formal checking
Repository-reported checking under its stated toolchain and axioms; not rerun by AIProofWatch.
Checker: The repository’s reported Lean checking process
Scope: The artifact reports exact optimal radii and classifications of optimal packings for one through seven freely rotated unit squares in a disk.
Basis: Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Correction and publication history
Full source review, 11 October 2026. Historical addition; subscriber alerts disabled.
Read this published revision