s(12) = 4 in Lean: Jatloe12SquaresFormalized (Jatloe's proof; Gurevitch, Lewis, Ahmed): tracking an unreported result

@jatloe

This issue tracks a significant result that reached the project through an announcement on X rather than an issue. Ahmed (@ManassehA06), whose earlier Lean formalization of the eleven-square proof the record already holds, announced on 22 October that the optimal packing of 12 squares is the 4 × 3 grid, crediting Jatloe (@jatloe) with a full proof and a partial formalization, and linked the Lean repository in a reply. We opened this issue so that the result's intake, review and validation have one public place.

The source. Queuingtheorydotcom/Jatloe12SquaresFormalized at d0caf45 (16 October 2026, tag n12-verified-2026-10-16), project Lean/Proofs/N12-jatloe, Lean 4.35.0 with Mathlib 56a0058. Its README credits Jatloe with the full mathematical proof and a partial formalization, Ben Gurevitch with aid in formalization, and CTJLewis with refactoring and compiling it. It states that the proof sources are copied byte-for-byte from EvolvingPrograms/SquaresLean at 1f60d41, which is not publicly reachable from here.

The claim. One theorem, N12Compact.Final.optimality : S12.packingConstant12 = 4, where packingConstant12 is the infimum of the sides L > 0 admitting a UnitPacking L: twelve open unit squares at arbitrary orientation and translation, contained in [0, L]², with pairwise disjoint interiors. The upper half is the 4 × 3 grid (gridPacking); the lower half is a normalization and a classification into 117 original cases, each closed by a proof term. The written mathematics, about 250 proof chapters, is retained in the repository under mathematics/.

What has been checked here (a read-only triage, 25 October):

The import closure of Compact.Assembly.Final at d0caf45 has 5,377 project modules and none missing, with 0 sorry, 0 axiom declarations and 2,572 uses of native_decide. The source's own final audit reports the three standard axioms plus 1,624 native-generated axioms, so the result trusts Lean's compiler as well as its kernel.
The source says plainly that its accepting run reused all 5,377 compiled objects from cache: it did not compile every module afresh, and no independent full rebuild has been run.
The statement's definitions (OpenSquare, UnitPacking, packingConstant12) read as the unrestricted problem. That reading still needs a review of its own.
Nothing has been built or replayed here.

What is open:

Retaining the source in a packet at d0caf45, with the release assets pinned by digest.
Registering the result as reported, beside the lower bounds T-049, T-078, T-079 and T-095 that the record holds for n = 12.
A statement audit of the Lean definitions against the problem, like the one done for the eleven-square formalization.
A mathematical review of Jatloe's written proof.
A full rebuild. The source's own per-module receipts price it at about 28 CPU-hours (17 to 40): 16.6 hours of serial wall time and 38.5 thread-hours. Its peak memory is not recorded. (Corrected 25 October: this item first called the build far above the project's compute cap. The receipts show it is not.) A rebuild of the 109-module closure that the statement uses costs about 9 minutes by the same receipts.

We will post the result's id and rungs here once it is on main, and update the open items as they close.

records: register T-243, Jatloe's reported Lean proof that s(12) = 4 …

Merge origin/main 886dddc (#808) into the #810 import

review: statement audit of the Lean proof that s(12) = 4

Merge n29-minpoly-1025 (T-244, Daniel's s(29) minimal polynomial) int…

Merge worktree-agent-aa8ad7d72a4de3571 (the n = 12 statement audit) i…

Merge origin/main 46e3555 (#814) into the #810 import; this branch's …

Merge origin/main 01e2b52 (#813, T-244) into the #810 and #811 import…

Merge pull request #812 from jlevy/claude/friendly-einstein-gf9z0h

The result is on main as T-245, registered as reported at V0/C0, an optimality claim. Here is where each open item of this issue stands.

Retained. The source is kept at d0caf45 in the packet jatloe-n12-lean-2026-10-16, with the release assets pinned by size and SHA-256 and both posts on X kept as receipts. The repository states no licence; that follow-up is think-c9ec.

Registered. T-245 cites one evidence entry, the source's own report (E-n012-jatloe-lean-report). It stands at V0 because no build of the proof is retained here, and at C0 because no review has read the proof. On the n = 12 case page the reported lower bound is now 4 and the reported status proved, as the reported lanes at 11 and 17 took T-060 and T-153. The verified lower bound stays T-095's 7943/2000, and the verified status stays open.

Statement audit: done. The audit of 25 October, an AI review, reads N12Compact.Final.optimality : S12.packingConstant12 = 4 line by line as s(12) = 4 for the unrestricted problem, with no premise, and reads the grid as attaining it. Its counts are made by devtools.audit_n12_lean into the packet's receipts/statement-audit.json. They map the 1,624 native_decide axioms of the source's log one to one onto the calls of 1,525 declarations. Two major findings bind how the result is described. First, the theorem trusts Lean's compiler as well as its kernel (M-1). Second, the accepting run compiled no module and reused objects from an earlier run in a repository nobody here can inspect, so the build stays the source's report (M-2). The audit reads the statement, not the proof, so it moves no rung.

Mathematical review: queued under think-4l14. It is what C1 needs.

Full rebuild: priced, not run. Nothing has been built or replayed here. A complete build of the theorem's 5,377-module closure from the pin, accepted only with the source's axiom list, costs about 28 CPU-hours (17 to 40) by the source's own per-module receipts. That is within the 40 CPU-hour item cap even at its high reading. It waits on an owner decision and a machine whose memory is known to hold the largest modules (think-dd3v). It is what V3 and C3 need.

Credit, as the source's README gives it: Jatloe for the proof and a partial formalization, Ben Gurevitch for help with the formalization, and CTJLewis, whom the record holds as Lewis, for refactoring and compiling it. Manasseh Ahmed published it. The record does not yet say whether Ben Gurevitch is the Benjamin Gurevitch whom the n = 11 formalization credits. An answer is welcome here, and it holds nothing open.

This issue stays open while the review and the build are queued, and a reply follows each change in the record.

Generated by Claude Code

news: T-245's S5 item, jatloe-n12-reported-proof (#812, #810)

records(think-4l14, think-6gti, think-jmb4): the stage 7 replies to #810

Merge pull request #815 from jlevy/claude/friendly-einstein-gf9z0h

Merge origin/main 0785626 (#815) into the exact-side register

Where this request stands in the record on main.

What is registered.

A Lean 4 proof, N12Compact.Final.optimality : S12.packingConstant12 = 4, that the infimum of the sides L > 0 at which twelve open unit squares at arbitrary rotation and translation lie in [0, L]^2 with pairwise disjoint interiors is 4, attained by the 4 x 3 grid: s(12) = 4, with the three standard axioms and 1,624 native_decide axioms:
- T-245, registered as reported (V0/C0); receipts of what has been run on it here are retained in packing/resources/web/jatloe-n12-lean-2026-10-16/receipts/, none of it yet counted toward confirmation. On the frontier it is current: a bound of its case records, verified or reported, rests on it now.

What remains, and which beads own it.

T-245: C1 needs the rest of the stage 4 review, a mathematical review of Jatloe's written proof and its formalization from the retained packet; the statement audit of 25 October is done. The source's per-module receipts and final audit do not qualify as a complete producer build under epistemics.md's rule for reported formal proofs: the accepting run compiled nothing, and the upstream repository and its runs are not public (the audit's M-2). V3 and C3 need a complete build of the theorem's 5,377-module closure from the pin, here or by a third party whose build is retained here, with its axiom receipt equal to the source's: about 28 CPU-hours, 17 to 40, by the source's per-module receipts, within the owner's 40 CPU-hour item cap at its high reading and gated on a machine whose memory is known to hold the largest modules. That would be reproduction with the producer's code. A build of the 109-module statement closure decides the statement and the grid in Lean and moves no rung. V4 and C4 need, on top of V3 and C3, two accepting adversarial AI reviews by distinct reviewers and the owner's oversight record naming trust-boundary, certificate-meaning and ai-findings. V5 needs a formalization review by a named human expert who is not an author. Owned by think-4l14 and think-dd3v.

On main. packing/frontier/RESULTS.md, docs/project/reviews/review-2026-10-25-n12-lean-formalization-statement-audit.md, packing/frontier/n-012.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-4l14 and think-dd3v, 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

s(12) = 4 in Lean: Jatloe12SquaresFormalized (Jatloe's proof; Gurevitch, Lewis, Ahmed): tracking an unreported result #810

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

s(12) = 4 in Lean: Jatloe12SquaresFormalized (Jatloe's proof; Gurevitch, Lewis, Ahmed): tracking an unreported result #810

Description

Activity

jlevy commented on Oct 25, 2026

jlevy commented on Oct 26, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions