AI-Assisted Formal Proof of Optimal 11-Square Packing

68AI Score

Executive Summary

Researchers used AI assistance to complete a formal proof of optimal packing for 11 squares in the Lean prover, verified across 7,920 modules. The work establishes an exact algebraic expression for the optimal side length but relies on `native_decide` for numerical certificates, extending the trust boundary to Lean's kernel and native compiler.

SOURCE COVERAGEOriginal coverage

Contents2 sections

Eleven-square packing in Lean

The complete optimality proof passed verification with native numerical certificates. The completed EvolvingPrograms verification run accepted all 7,920 local Lean modules, and its final audit reports zero admissions. This repository imports those exact proof sources and pinned build configuration from commit 1bf942a7af1ea330e95489d8997deebd4227ca71. See the verification report for evidence and scope.

Selected expensive, exact numerical certificate checks use native_decide. Geometry, checker soundness, and proof assembly retain ordinary Lean proofs. Consequently the final theorem trusts Lean's kernel and native compiler; this is not a kernel-only verification claim. The approved numerical declarations and their exact source hashes are recorded in verification/native-certificates.json.

The optimal side length is

[ T = \frac{6u+4}{1+2u-u^2}, ]

where u is the unique root in (9/25,37/100) of

[ 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0. ]

The construction attains approximately 3.8770835900228141773. The model allows arbitrary orientations, legal boundary contact, and disjoint open interiors. The public statements in ElevenSquare/Optimality.lean and the complete T03 source tree are unchanged from this repository's previous main branch.

Entry points

File	Purpose
`ElevenSquare/Foundations.lean`	Geometry, exact endpoint, attaining construction, closed-cell cover, and finite case reduction.
`ElevenSquare/Pending/`	Original public interfaces, now discharged by the integrated proof. The directory name is historical.
`ElevenSquare/Interop/Wand125/`	Connections to the incorporated upstream certificate results.
`ElevenSquare/Tasks/`	Geometric arguments, checkers, certificate data, and local analytic proofs.
`Sqpack/`	Incorporated certificate checkers, generated proofs, and simplifications.
`ElevenSquare/Optimality.lean`	Unconditional optimality and side-length lower-bound theorems.
`ElevenSquare/Verification.lean`	Axiom queries for the public proof targets.

Reproduce verification

The project pins Lean 4.34.1 and Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612. Keep lake-manifest.json unchanged. On Linux with Python 3, Git, curl, and tar:

bash scripts/run_verification.sh --bootstrap --jobs 2

On macOS, first install the elan launcher, then use the same command. The bootstrap can prepare the pinned toolchain and dependency cache when elan is already installed. Choose a worker count appropriate to the machine; modules are compiled serially. Existing valid receipts are reusable. Add --fresh to force a complete replay; Ctrl-C stops the runner cleanly.

The command checks every local module and performs the final source, receipt, dependency, and axiom audit. Require OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES, zero admissions, and trust_model: lean_kernel_and_native_compiler in the final result. Reaching 100% of compiled modules alone is not sufficient.

A source-only check, without Lean, is:

python3 scripts/check_sources.py

The manual workflow and Ubuntu instructions also support resumable verification. Pushes do not start a workflow. The successful source run used EvolvingPrograms' larger runner; it does not establish a cold-build runtime or a 2–3 hour macOS guarantee.

Do not run historical materialization commands or verify.py --setup on this snapshot: they restore superseded generated sources. Build objects and logs belong in ignored .lake/ and .verification/ directories.