Complete Lean proof of s(19) optimality: registration request

I've released a complete Lean proof of global optimality for Robert Wainwright's 1979 packing of 19 unit squares: s(19) = 3 + 4√2/3.

Credit: Oscar Fitzharding (@ofitzharding).

Claim: For every real container side L,

Sq19.square19_optimality (L : ℝ) : Feasible19 L ↔ 3 + 4 * Real.sqrt 2 / 3 ≤ L

This allows arbitrary rotations and boundary contact. It proves both existence at the endpoint (approximately 4.885618) and impossibility below it. No certificate-acceptance or case-exclusion hypotheses remain.

Source: Repository, v1.0.0 certificate sources, pinned commit 34fb2b7bc39465db368c45cb48d4db58829d3051. MIT licensed.

Verification: The theorem builds with Lean 4.34.1 and pinned Mathlib; see the full axiom report. Every one of the 13,143 modules in the theorem's import closure, Mathlib included, was replayed through Lean's kernel with the toolchain's LeanChecker, with 0 failures. The published scripts/verify.py was smoke-tested end to end: fetching and hash-checking the sources, the Lake build, the native checker library, and fresh rebuilds of every kind of certificate module, which were byte-identical to the original build. The exact statement and axiom check also passed. A complete from-scratch rebuild with the published script takes several hours on 64 cores and has not yet been run, so independent reproduction is very welcome.

Trust and review scope: Geometric soundness is proved in Lean. Finite checks use native_decide: three standard axioms plus 4,320 native-check facts, and no sorryAx. The compiler, native evaluator and C toolchain are trusted.

Lineage and assistance: Robert Wainwright supplied the 1979 construction. The proof extends the method and checker code of the s(17) Lean proof (#565). Thanks to everyone involved with the Squares Project, especially Manasseh Ahmed (@Queuingtheorydotcom). Development used Claude and Codex assistance.

Please register the result under my name and link the proof from the n = 19 case page. I'm happy to help with reproduction and statement review.

resources: retain Fitzharding's sq19 and his X announcement; record i…

records: register T-193 (#639, Daniel's exact sides) and T-194 (#640,…

review(#640): endgame and capture-link re-evaluation programs (checkp…

review(#640): draft of the s(19) Lean proof review, with the review p…

review(#640): comparison with the s(17) reviews, document-map row, ar…

review(#640): archive scan and native-fact accounting results

review(#640): wording of the endpoint clearance

review(#640): check_region.py checks every target polygon is bounded;…

review(#640): address review A on #655: what the independent checks s…

Merge pull request #642 from jlevy/claude/ecstatic-edison-8en33t-inta…

Merge pull request #651 from jlevy/claude/intake-2026-10-16-records-6…

review(#640): say what a pass shows for the combinatorial facts, as t…

Merge pull request #655 from jlevy/claude/intake-2026-10-16-review-640

Merge pull request #658 from jlevy/claude/intake-2026-10-16-records-1…

@ofitzharding

@ofitzharding, thank you, and congratulations on the s(19) proof. It is registered on main as T-194, an optimality result, and the n = 19 case page links it beside your repository. We retain a copy of v1.0.0 (34fb2b7) with the release archives pinned by digest. The published site (v0.7.34) shows it at V0/C1.

What is registered.

s(19) = 3 + 4√2/3 = 4.8856180831641267…: for every real L, nineteen closed unit squares, with arbitrary rotations, boundary contact allowed and disjoint interiors, fit in [0, L]^2 exactly when 3 + 4√2/3 ≤ L, existence at the endpoint included.
- The proof is in Lean 4.34.1 with Mathlib. It trusts Lean's compiler, native evaluator and C toolchain for 4,320 native_decide facts. The source reports a kernel replay of the theorem's 13,143-module import closure with no failure, and no complete rebuild from source yet.
- T-194, reviewed: its argument has been read here and no blocking defect found, and no replay here has passed yet (V0/C1).
- E-n019-fitzharding-lean-report: your report as the record holds it, read by the mathematical review of 16 October.
- E-n019-fitzharding-endpoint-review, confirmed here: re-verified here by an independent implementation (check_endpoint.py).
- E-n019-fitzharding-cover-census-review, confirmed here: re-verified here by an independent implementation (check_cover_census.py).
- E-n019-fitzharding-region-review, confirmed here: how it was re-verified is not yet recorded.
- E-n019-fitzharding-capture-link-review, confirmed here: re-verified here by an independent implementation (check_capture_link.py).
- E-n019-fitzharding-endgame-review, confirmed here: how it was re-verified is not yet recorded.
- E-n019-fitzharding-archives-review, confirmed here: re-verified here by an independent implementation (scan_archives.py, count_native.py).

What is still queued, and how it will be completed.

V3 and C3 need a complete build of the theorem's import closure that the record can rest on, with its axiom receipt. That means the source's scripts/fetch.sh and scripts/verify.py, run from the retained pin and the five release archives at Lean 4.34.1, here or by a third party whose build is retained here. That would be reproduction with the producer's code.
- The build is held: the source gives several hours on a 64-core, 512 GB machine, which is above the pass's 40 CPU-hour cap and this host.
- A cheaper subset decides parts and moves no rung: a build of the existence half, EndpointPacking, with its axioms printed. The other part of that subset, the five archives' digests against SHA256SUMS, which fetch.sh checks, the review has already decided (E-n019-fitzharding-archives-review).
V4 and C4 need, on top of V3 and C3:
- two accepting adversarial AI reviews by distinct reviewers, of which the review of 16 October is one;
- the owner's oversight record naming trust-boundary, certificate-meaning and ai-findings, which would disposition the review's seven findings, none of them blocking.
V5 needs a formalization review by a named human expert who is not the author.

Since the release, your commit c86a991 (16 October) added a clean source rebuild receipt and log for v1.0.0. This reply covers v1.0.0 as registered. Reading that receipt into the record is a separate step, and a follow-up here will report it.

On main. packing/frontier/RESULTS.md, docs/project/reviews/review-2026-10-16-fitzharding-n19-lean.md, packing/frontier/n-019.md.

This issue stays open while anything above is queued, and a reply follows each change in the record.

Generated by Claude Code

Merge origin/main (#646, site v0.7.35) into the #639/#640 replies

Merge origin/main (#691, #514, #693) into the #639/#640 replies

Merge pull request #690 from jlevy/claude/intake-2026-10-19-replies-6…

Merge origin/main 4b8aec9 (#690) into the evand lane

Where this request stands in the record on main.

What is registered.

s(19) = 3 + 4√2/3 = 4.8856180831641267…: for every real L, nineteen closed unit squares with arbitrary rotations, boundary contact allowed and disjoint interiors fit in [0, L]^2 exactly when 3 + 4√2/3 ≤ L, existence at the endpoint included. Proved in Lean 4.34.1 with Mathlib, trusting Lean's compiler, native evaluator and C toolchain for 4,320 native_decide facts; the source reports a kernel replay of the theorem's 13,143-module import closure with no failure, and no complete rebuild from source yet:
- T-194, reviewed: its argument has been read here and no blocking defect found, and no replay here has passed yet (V0/C1). On the frontier it is pending adoption: better than its case records hold, and not yet taken into them.
- E-n019-fitzharding-endpoint-review, confirmed here: re-verified here by an independent implementation (check_endpoint.py).
- E-n019-fitzharding-cover-census-review, confirmed here: re-verified here by an independent implementation (check_cover_census.py).
- E-n019-fitzharding-region-review, confirmed here: re-verified here using a checker that shares components with the generator (check_region.py).
- E-n019-fitzharding-capture-link-review, confirmed here: re-verified here by an independent implementation (check_capture_link.py).
- E-n019-fitzharding-endgame-review, confirmed here: re-verified here using a checker that shares components with the generator (check_endgame.py).
- E-n019-fitzharding-archives-review, confirmed here: re-verified here by an independent implementation (scan_archives.py, count_native.py).

What remains, and which beads own it.

T-194: V3 and C3 need a complete build of the theorem's import closure that the record can rest on, with its axiom receipt: the source's scripts/fetch.sh and scripts/verify.py from the retained pin and the five release archives at Lean 4.34.1, here or by a third party whose build is retained here. That would be reproduction with the producer's code. It is held: the source gives several hours on a 64-core, 512 GB machine, above the pass's 40 CPU-hour cap and this host. A cheaper subset decides parts and moves no rung: a build of the existence half, EndpointPacking, with its axioms printed; the five archives' digests against SHA256SUMS, which fetch.sh checks, the review has already decided (E-n019-fitzharding-archives-review). V4 and C4 need, on top of V3 and C3, two accepting adversarial AI reviews by distinct reviewers, of which the review of 16 October is one, and the owner's oversight record naming trust-boundary, certificate-meaning and ai-findings, which would disposition its seven findings, none blocking. V5 needs a formalization review by a named human expert who is not the author. Owned by think-nqnl.

On main. packing/frontier/RESULTS.md, docs/project/reviews/review-2026-10-16-fitzharding-n19-lean.md, packing/frontier/n-019.md.

Nothing you asked for is queued, so this issue is closed with this comment. Closing it confirms nothing above that is still open: each entry stands at the rungs given, what remains of its validation is owned by think-nqnl, and a follow-up will be posted on this issue whenever an id, a rung, a status or a position above changes.

Generated by Claude Code

Navigation Menu

Repository navigation

Complete Lean proof of s(19) optimality: registration request #640

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Complete Lean proof of s(19) optimality: registration request #640

Description

Activity

jlevy commented on Oct 19, 2026

jlevy commented on Oct 26, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions