Lean proof formalizes optimal packing of 19 unit squares, side ≥ 3 + 4√2/3
ctjlewis · x · 2026-10-16
A new open-source GitHub repo, sq19 by ofitzharding, formalizes the classic square packing problem in Lean: 19 unit squares fit in a square of side L exactly when L ≥ 3 + 4√2/3 ≈ 4.885618, with arbitrary rotations and touching allowed.
- Core theorem: Sq19.square19optimality, an iff between packing feasibility and the lower bound
- Relies only on the axioms propext, Classical.choice, Quot.sound, plus 4,320 nativedecide certificate checks trusting Lean's compiler and native evaluator
- The theorem's import closure spans 13,143 modules; MIT licensed
A neat case of using proof assistants to settle optimality in combinatorial geometry.
More from Research
- Lean v4.35.0 ships verified kernels — one written and proven consistent by Claude — geoffreyirving · 2026-10-16
- MP-Bench: 12 voice agents no better than coin flip at knowing when to speak in group chats — solyarisoftware · 2026-10-16
- Neuron-level GWAS + PheWAS on Qwen3-8B pinpoints safety-critical neurons — Sauers_ · 2026-10-16
- Tencent squeezes 770B-parameter Hunyuan Hy4 Preview into 214 GiB at ~2.38 bits per weight — coolmum18 · 2026-10-16
- 200 chess games suggest in-context learning doesn't work yet, experimenter says — akbirthko · 2026-10-16
- Mosaic: multi-session agentic RL with hierarchical advantage estimation — LARK-Lab · 2026-10-16