Formalizing the Optimal Packing of 11 Squares via AI

Project Avatar

This project provides a rigorous Lean formalization of the proof regarding the optimal packing of 11 squares. The verification process was successfully completed, utilizing native numerical certificates to confirm the results.

🛡️ Verification & Trust Model

The verification was executed via EvolvingPrograms, which processed a total of 7,920 local Lean modules. The final audit concluded with zero admissions, meaning every part of the proof was accounted for.

Important Note on Trust: Because the project utilizes native_decide for computationally expensive exact numerical certificate checks, the final theorem relies on both the Lean kernel and the native compiler. This is not a claim of kernel-only verification.

The specific numerical declarations and their corresponding source hashes are archived in verification/native-certificates.json.

Verification Workflow

📐 Mathematical Specifications

The proof establishes that the optimal side length $T$ is defined by the following formula:

$T = \frac{6u+4}{1+2u-u^2}$

Where $u$ is the unique root located within the interval $(\frac{9}{25}, \frac{37}{100})$ for the polynomial:

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

Key Details:

Approximate Value: $T \approx 3.8770835900228141773$
Constraints: The model permits arbitrary orientations, allows for legal boundary contact, and requires disjoint open interiors.

📂 Repository Architecture

The project is structured to separate geometric foundations from the final optimality theorems.

File/Directory	Primary Purpose
`ElevenSquare/Foundations.lean`	Core geometry, construction methods, and finite case reduction.
`ElevenSquare/Pending/`	~~Legacy public interfaces~~ (Now integrated into the main proof).
`ElevenSquare/Interop/Wand125/`	Integration points for upstream certificate data.
`ElevenSquare/Tasks/`	Analytic proofs, certificate data, and geometric arguments.
`Sqpack/`	Generated proofs, simplifications, and certificate checkers.
`ElevenSquare/Optimality.lean`	The primary theorems for side-length lower bounds and optimality.
`ElevenSquare/Verification.lean`	Axiom queries used to validate public proof targets.

🛠️ Reproduction Guide

To reproduce the verification, ensure you are using Lean 4.34.1 and the Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612.

Execution Steps

Install elan launcher (Required for macOS).
Ensure Python 3, Git, curl, and tar are installed (Linux).
Run the verification script:

# Basic verification run with 2 jobs
bash scripts/run_verification.sh --bootstrap --jobs 2

# To force a complete replay from scratch
bash scripts/run_verification.sh --bootstrap --jobs 2 --fresh

Validation Criteria

The process is considered successful only if the output confirms:

OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES
zero admissions
trust_model: lean_kernel_and_native_compiler

For a source-only check that does not require the Lean environment, use: python3 scripts/check_sources.py

Warning: Avoid using verify.py --setup or historical materialization commands, as these will overwrite current sources with outdated versions.

🤝 Credits & Provenance

We extend our gratitude to EvolvingPrograms, @ctjlewis, and all contributors who assisted in the formalization and verification of this proof.

Detailed Credits: See ACKNOWLEDGEMENTS.md.
Source History: See PROVENANCE.md.
Notices: Retained in integrations/wand125.

~~Previous partial-audit records and unfinished status notes~~ are now superseded by the final completed-run report.