Latest commit
History
Folders and files
Repository files navigation
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 .
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
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.
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.
Credits and provenance
We thank EvolvingPrograms , @ctjlewis , and every project contributor for the formalization and verification work. See ACKNOWLEDGEMENTS.md for individual and upstream credits, PROVENANCE.md for source history, and integrations/wand125 for retained notices. Historical simplification notes and partial-audit records are preserved; their old unfinished-status statements are superseded by the completed-run report.
About
Lean formalization of the optimality proof of the 11 square packing