T-154: Fitzharding reports a Lean proof that $s(17)=4.67553009360455\dots$$s(17)=4.67553009360455\dots$

S5 V3 C1 Formalization reviewed

2026-10-12 published · Fitzharding after Levy, Ahmed, MacIver · $n=17$$n=17$

Fitzharding reports a Lean 4 proof that Bidwell's 1998 packing of seventeen unit squares is optimal: $s(17)=4.67553009360455095163\dots$$s(17)=4.67553009360455095163\dots$, T-153's value L. His proof uses a different argument from Overbeck's candidate proof (T-153).

Its theorem, Sq17.square17_optimality (L : ℝ) : Sq17.HalfPlaneAssembly.PlainPacking L ↔ Sq17.EndpointGeometry.side ≤ L, says that seventeen closed unit squares, each independently translated and rotated, with pairwise disjoint interiors, fit in the axis-aligned square [0, L]^2 exactly when L is at least EndpointGeometry.side; existence at that side is part of it, so the minimum is attained. That constant is T-153's L by identity of definition: (6+4t)/(1+2t−t2)$(6+4t)/(1+2t-t^2)$ at the unique common zero of the same two polynomials, H-255's F and G, in the same box of radius 10^-12 about exp-237's 60-place centre, which is the chart of the certified endpoint that holds the case's verified upper bound (the packet's receipts/endpoint-comparison.json).

The route: a cover of the centre box by 24 cells, each holding at most one centre; a census, checked by Lean's kernel, that reduces every occupancy of 17 cells to 35 small patterns and 2,781 full cases; half-plane propagation traces that exclude the patterns and 2,776 ordinary cases at every side up to a little above side, branch trees and a chain for four neighbouring cases, and, for the last case, the occupancy of Bidwell's packing, a capture trace into a chart near the endpoint, where 52 contact rows and a dual certificate over 93 boxes force the side to be exactly side. Every bridge from a trace to geometry is a Lean theorem.

The theorem includes the geometric justification for certificate acceptance and every case exclusion. Its trust boundary, as the source states it: the geometric soundness arguments are checked by Lean's kernel, and 13,343 finite certificate facts are decided by native_decide, so Lean's compiler, native evaluator and the C toolchain are trusted, with the standard axioms propext, Classical.choice and Quot.sound and no sorryAx.

The source reports a clean rebuild of the 4,951 modules of the theorem's import closure from its published sources with Lean 4.34.1, on two Linux machines, with the axiom set matching its own build. Nothing here has repeated that build.

Two reviews of 13 October, by separately prompted AI lanes, found no mathematical defect. The first read the statement, the endpoint, the trust boundary and the chain to the final theorem. The second read the checkers and their soundness proofs in full, recomputed the census, the interior cells' capacities and the 93-box dual certificate exactly, and re-evaluated ten of the 13,343 native_decide facts with an independent implementation, all agreeing with the source; ten facts are a sample.

Fitzharding, sq17-lean, release v1.0.0 of 12 October 2026. Its README credits Bidwell, Hämäläinen's 1980 arrangement, Friedman's survey, the Squares Project, Ahmed and collaborators' eleven-square formalization as a reference for its trust boundary, and David MacIver's earlier Lean work on a seventeen-square lower bound; issue #565 also names Ahmed's $s(11)$$s(11)$ proof as a methodological reference.

The README states that Overbeck "published an independent candidate proof of seventeen-square optimality" on 12 October 2026 and that "This repository presents a separate Lean formalization". It says the project "was developed with substantial assistance from Claude and Codex"; the author's post says it was "Built with @OpenAI Astra + @AnthropicAI Opus 5.5" and thanks Ahmed and Levy for prior work.