T-238: chelokot reports Lean proofs of $s(2),s(3),s(4)=2$$s(2),s(3),s(4)=2$, $s(5)=2.707\dots$$s(5)=2.707\dots$; Daniel, rectangle theorems

S2 V0 C0 Formalization recorded

2026-08-29 published · Vlasenko; Daniel · $n=2,3,4,5$$n=2,3,4,5$

chelokot reports Lean 4 proofs that $s(2)$$s(2)$ = $s(3)$$s(3)$ = $s(4)=2$$s(4)=2$ and $s(5)=2$$s(5)=2$ + 1/√2 = 2.70710678118654752440…, and Daniel Lean 4 theorems on rectangles from which those values are read at equal sides: a formalization of T-237, the classical values, and the first proof-assistant routes to them the record holds.

chelokot's theorems are Records.Square5.s5_eq_goebel : IsMinimumSide 5 (2 + Real.sqrt 2 / 2), by Göbel's packing and Friedman's four unavoidable points (1, 1), (1, 1 + d), (1 + d, 1) and (1 + d, 1 + d) with d = √2/2, and s2_eq_two, s3_eq_two and s4_eq_two, IsMinimumSide n 2 for $n=2$$n=2$, 3 and 4, where IsMinimumSide n s says that n closed unit squares, each translated and rotated, fit in [0, s]^2 with pairwise disjoint interiors and fit in no smaller side.

This repository built the archive at the pin on 2 October 2026 for T-086, and that build's log prints these theorems' axioms, propext, Classical.choice and Quot.sound; no receipt names them yet. chelokot, square-packing-archive, August 2026. The archive's ATTRIBUTION.md credits chelokot as "project creator, concept, and product direction" and GPT 6 Astra with "AI-produced research, packing optimizations, and Lean formalizations credited under this name in the archive".

Daniel's rect2_iff, rect3_iff and rect4_iff decide which rectangles hold two, three and four unit squares, and rect5_pts_lower and rect5_upper give five squares in a square of side a >= 2 exactly when a >= 2 + √2/2. At equal sides they give the same values; no theorem of his states $s(n)$$s(n)$ itself, and the step from the rectangle theorems to the square values is read here, not proved in Lean. The source reports standard axioms only. Daniel, square-packing, 21 October 2026; his literature note credits chelokot's proof as the earlier, and the repository's CREDITS.md reads "Produced by Claude (Anthropic) in a single session under human direction".