The Squares Project

The square packing problem is a simple and long-standing problem in geometry: what is the size of the smallest square that can hold \(n\)$n$ unit squares, where the squares are free to rotate but cannot overlap? The side length of that smallest square is written \(s(n)\)$s(n)$.

The question of the value of \(s(n)\)$s(n)$ is simple, but the answer is an open problem for most \(n\)$n$. In many cases, \(s(n)\)$s(n)$ is known only to lie between an upper bound (the size of the enclosing square for the tightest packing ever discovered, such as \(s(29) \le 5.934\)$s(29)\le 5.934$) and a lower bound (a size below which it is proved that no packing can exist, such as the reported \(s(29) \ge 5.81\)$s(29)\ge 5.81$).

The project covers the problem at every \(n\)$n$. Its frontier keeps one record for each case \(n = 1\ldots324\)$n=1\dots 324$, with reported and verified bounds kept separate, and its results register grades each registered result, this project’s or another’s, by how far it has been checked. It goes into most depth where there is recent progress, which in September 2026 means \(n = 11\)$n=11$, \(n = 17\)$n=17$, and the exact values newly proved at \(n = 21\)$n=21$, \(32\)$32$ and \(45\)$45$. At seventeen squares both ends of the bracket are now machine-checked: Guzhou0806’s lower bound \(s(17) > 4.66044275\)$s(17)>4.66044275$ (T-093), and the upper bound \(s(17) \le 4.67553009\ldots\)$s(17)\le 4.67553009\dots$ of John Bidwell’s 1998 packing, certified exactly from Kleddamag’s rational witness (T-065).

A recent major result settles eleven squares, until then the smallest case still open: \(s(11) = T = 3.877083590022814\ldots\)$s(11)=T=3.877083590022814\dots$, the exact side of Walter Trump’s 1979 packing. T-060 records the global lower bound from the Astra-assisted 11SquaresOptimal proof by Queuingtheorydotcom, building on this project and Kleddamag. This repository independently replayed the proof’s exact inputs and audited their mathematical composition (V3/C3/S5: machine-checked, review record pending); T-011 verifies Trump’s matching witness. The same argument, read at side exactly \(T\)$T$, shows that Trump’s packing is the only optimal one up to the eight symmetries of the container and relabelling of the squares: T-112 registers that direct corollary of T-060, which adds no computation (V3/C2/S3: its step at side \(T\)$T$ is prose). The case record, review, and retained packet state what the confirmation depends on and the reproducibility defects found in the source. On 6 October 2026 the proof was announced as formalized in Lean 4 “thanks to Astra and Claude”, in 11SquaresFormalized by Queuingtheorydotcom and contributors. This project’s statement audit reads its theorem as exactly \(s(11) = T\)$s(11)=T$, and its source reports that its full verification run, resumed from earlier validated receipts, passed, trusting Lean’s compiler for its numerical certificates. It is recorded on T-060 as the source’s report; a complete build this record can rest on, and a human expert’s review of the formalization, are still to come.

The results live on the project site, Square Packing. It carries the recent results by this project and by others with their credit, the verification ratings, the atlas of known-best packings and its films, the table of every result, and the frontier survey of every case \(n = 1\ldots324\)$n=1\dots 324$, all generated from the record in this repository. The in-repository record is the results register, the per-case status table, and epistemics.md, which defines how each claim is graded. The site and the atlas posters are at edition v0.5.0; each paper carries a version of its own; the atlas films are the ones cut for the v0.4.2 release.

The site’s papers explain the proofs. Three of them form one series on \(n = 11\)$n=11$, read in order:

1. New Lower Bounds for Square Packing for n = 11: how weighted points and 2-of-3 threshold atoms prove T-018, T-025 and T-026, \(s(11) \ge 3.8264\ldots\)$s(11)\ge 3.8264\dots$, with interactive figures (PDF, source).
2. A Review of the Certified Lower Bound s(11) > 31/8 for 11 Squares: explains Kleddamag’s proof that \(s(11) > 31/8\)$s(11)>31/8$ (T-037): five-site k-of-m charges, k-of-m charges on shrunken parents with strict cores, and a reoptimized certificate over 12,028 angle rows (PDF, source).
3. A Review of the Optimality Proof of the Trump Packing of 11 Squares: explains Queuingtheorydotcom’s proof that Trump’s packing is optimal, \(s(11) = 3.8770835\ldots\)$s(11)=3.8770835\dots$ (T-060): construction, case exclusions, capture and local isolation, with figures drawn from or checked against the retained proof data (PDF, source).

This repository also contains a set of tools and AI workflows for automated mathematical research: the results and the frontier survey are produced and checked by AI agents running a recorded process, with hypotheses registered before measurement, every claim graded, and every defect logged. The rest of this README is about that work.

Results (site) · Research Status · Repository Guide · Getting Started · Reports · Autonomous Research Process · Conventions · Layout

Repository Guide

Long-lived tests and runs retain detailed timing evidence under OR-14. The validation efficiency and checkpoints plan tracks improvements to everyday feedback and full final checkpoints, with measurements and preserved coverage required before accepting a speedup.

SYNOPSIS.md is the technical root and current-state document. Its research-status roll-up synthesizes the generated frontier status table, results register, campaign ledger, agenda map, and session close report. The W8 documentation pass defines how those sources are reconciled. The separate small-n mathematical audit challenges the current research approaches and supplies the enlarged candidate set. The subsequent W10 route-selection review derives the due efficiency checkpoint, records every candidate’s disposition, and separates the next W5 block from the later scientific choice. To resume work, use the synopsis’s current handoff, which names the owning work item and next bounded slice.

Getting Started

Read TUTORIAL.md once for the mathematical orientation, then the synopsis’s research status and roadmap for current results and open work. Run commands from packing/; the project uses Python 3.14 through uv.

Essential Terminology

These are the terms a reader encounters most often. The synopsis terminology gives the full definitions.

Essential Conventions

One ID names one durable thing, and IDs are not reused. The prefix identifies the record’s layer; conventions.md is the definitive registry.

Other rules needed to read the repository:

• Structured values live in YAML or frontmatter; prose supplies explanation and judgment. A consumer does not scrape prose for fields.
• Declared paths are repository-relative. Generated views are regenerated from their source records and are not edited by hand.
• Evidence assurance, method, origin, precision, limitations, and novelty are separate facts. Whole-result V/C classifications do not replace evidence-level fields.
• Source-faithful archive material is not cleaned up as project prose. Reconstructed source text is marked and counted.
• Corrections preserve the original record and add a dated statement of what remains valid. IDs and scientific outcomes are not silently rewritten.

Technical Stack

The project keeps numerical exploration, symbolic reconstruction, exact verification, and research records as separate layers.

The dependency and tool versions are owned by packing/pyproject.toml, packing/uv.lock, packing/sqsearch/Cargo.toml, and the root Makefile and hook configuration. development.md explains how the layers interact.

Core Commands

uv sync --frozen --all-extras --group dev
uv run --frozen packing-witness inspect witnesses/schadt-n029-2025-decimal.yaml
uv run --frozen packing-witness check witnesses/schadt-n029-2025-decimal.yaml \
  --method numerical-multiprecision --precision 300 --tolerance 1e-100
uv run --frozen packing-witness verify witnesses/schadt-n029-2025-rational.yaml
uv run --frozen python -m cases.trump11.verify_exact
uv run --frozen --all-extras --group dev packing-validate --edit

--records, --edit, --push, --fast, and the full checkpoint are the five lifecycle tiers. --edit is the ordinary inner loop; pull-request CI executes --fast as seven disjoint required parts. Which steps each tier runs, what it costs, and which of the three behavioral lanes a test lands in are tabulated in development.md → Validation Loops; the ceilings themselves are data the gate reads, in packing/devtools/gate-budgets.yaml. In short: a contributor runs --edit while editing and --push before pushing, every pull request runs all seven parts of --fast, and the complete gate runs on main and at the end of a research block.

Witness/v2 is the interchange format for supported rational, algebraic, and decimal witnesses. Exact verification covers rational witnesses and algebraic witnesses whose field preconditions the tool can certify. Recovering exact geometry from arbitrary decimal input remains the hard step; development.md and the module docstrings under packing/src/sqpack/ define the supported APIs and limits.

sqpack.render creates deterministic, self-contained SVG figures while preserving the input’s evidence tier in captions and metadata. The rendering guide owns the CLI, gallery, contact annotations, portability contract, and Motion Lab. The Motion Lab is an exploratory instrument, not a citable research result.

Reports

These 23 research reports are the durable topical syntheses:

The reports distinguish formal proof, finite numerical checks, and source reports. The draft X-031 floor-normalized T2 exploration records reviewed local cutoffs and bounded H-161 stability; it establishes no target result or global bound. The document map identifies every maintained guide, dated record, generated view, and superseded document.

Autonomous Research Process

The repository supports autonomous research without making process a substitute for evidence. This section gives the operating model at a glance. The operating rules, workflow contracts, and campaign runbook own the full rules.

Assurance and Verification

Evidence uses three assurance labels:

• reported for a named source claim not checked here;
• numerically-checked for finite-precision calculations with their precision, rounding, and tolerance recorded; and
• verified for an exact check, rigorous interval certificate, or complete proof that covers the claim and its preconditions.

Whole results use the separate V/C classifications in epistemics.md. A verified feasible witness proves an upper bound; it does not prove global optimality without a matching verified lower bound.

Finite precision is not enough for a packing with exact contacts. Floating-point arithmetic can establish a strict positive gap, but a tolerance that accepts a true zero-gap contact also accepts a smaller overlap. Exact algebraic signs or outward-rounded intervals are therefore required before a contact-heavy witness becomes formally verified. The synopsis explains the full argument in Why Exactness Is Not Optional.

Two retained examples show the boundary. The Schadt \(n = 29\)$n=29$ decimal pose passes its declared 300-digit numerical check, while the separately promoted interval witness establishes a slightly weaker side rigorously. Trump’s \(n = 11\)$n=11$ witness is verified exactly over a degree-eight number field, including fourteen zero-gap contacts. The per-case records (n = 29, n = 11) state exactly which bound each artifact proves.

Verification answers whether a proposed packing is valid. Proving it optimal is a different problem and requires a matching lower bound. The synopsis’s capability ladder distinguishes what is built, what is ordinary engineering, and what remains mathematically contingent.

Operating Principles

Correctness is the veto: no result advances beyond its evidence, however costly the required check may be. Process is proportional infrastructure, not a second mathematical standard; missing evidence can block promotion, while a preferred form or checkpoint cannot block useful work merely because it looks more disciplined. Insight remains free to propose. Efficiency may simplify process but cannot lower the assurance bar.

Layers of Work

The system separates the kind of effort, the lens used to judge it, and the bounded action being executed:

Focus and workflow are independent. A W6 experiment may emphasize correctness, insight, or efficiency without changing its promise to execute a preregistered measurement; an efficiency-focused phase does not become W5 unless its durable result is a measured performance decision. A slice is smaller than either: it is one action inside the declared phase.

The durable work objects also have different lifetimes:

A bead says what needs doing. A bounded commitment says what would count as settling one attempt. A workflow phase says what kind of move is being executed now. One bead may require several commitments, one commitment may span several phases, and one phase may produce zero or several scientific records. The work-unit definitions, campaign runbook, and agent-session guide own the exact contracts.

Workflow Entry Points

Choose the workflow whose durable result matches the task. The synopsis owns the complete entry, exit, and transition contracts.

A result published by others follows the result import process, a standard sequence of these phases, whichever source delivers it: an issue, an owner’s message, a catalogue, or a watched repository. When the owner asks for an intake pass, make intake sweeps every source at once.

Use general-improvement only for repository maintenance that fits none of W1–W10. Routine work records a workflow, bounded objective, intended artifact, and focused check. Use a versioned agent-session record only when work crosses multiple workflow phases, coordinates independent delegates, or needs durable recovery state.

Defects and Corrections

defects.md is generated from packing/defects.yaml. It records every known defect in this toolchain, what caught it, the consequence, the correction, and the regression that now guards it. Two lessons govern review:

• Results that look unusually good receive the strongest challenge because many soundness defects have pointed in that direction.
• The automated gate checks only rules someone encoded. No soundness defect in the log was caught by it.

Current counts and detector statistics belong only in the generated defect log and the synopsis defect section. Corrections follow conventions.md §7: preserve the original record, add a dated correction that states what remains valid, and route any changed conclusion to the artifact that owns it.

The Autonomous Work Loop

W6 is the measured experiment loop rather than an umbrella for every session:

W3 insight iteration → registered hypothesis → W6 measured round → evidence and verdict
          ↑                                                        │
          └──────── successor questions ← W2 factual review ←──────┘

The hypothesis, criterion, regime, budget, and stop rule are fixed before measurement. The round records every outcome and stops at the criterion or clock. Promoted, novel, disputed, or otherwise high-risk claims receive an independent W2 pass before they move forward; routine rounds whose recorded guards already decide the criterion may return directly to W3 or another W6 slice.

The tbd queue owns durable work and dependencies. Campaign agendas order bounded commitments; hypothesis and experiment records own scientific claims and measurements; commits own code; escalated agent-session records own phase and recovery state. The key record IDs are X-NNN for explorations, H-NNN for hypotheses, exp-NNN for experiments, BC-NNN for bounded commitments, T-NNN for registered results, and D-NNN for defects. conventions.md owns the complete ID registry.

The campaign’s bounded research cycle defines clocks, result routing, budgets, and stop rules. Changing agents changes the driver, not the record or the evidence required for a claim.

Where the Contracts Live

Conventions

conventions.md owns identifiers, filenames, artifact discipline, evidence fields, provenance, corrections, and the boundary between machine checks and review. epistemics.md owns whole-result classifications and the policy for results by others: their scope, credit, import and reply. operating-rules.md owns how sessions are conducted, and development.md owns the engineering and validation workflow.

Layout

.
├── TUTORIAL.md             First-principles orientation for a newcomer
├── SYNOPSIS.md             Current research status, roadmap, results, and handoff
├── conventions.md          Artifact, identifier, evidence, and correction rules
├── epistemics.md           Whole-result verification and confirmation rubric
├── operating-rules.md      Session conduct and workflow rules
├── development.md          Python setup, engineering boundaries, and validation
├── defects.md              Generated view of packing/defects.yaml
├── docs/project/           Reports, reviews, specs, postmortems, and dated handoffs
├── docs/project/research/  The research reports listed above
├── packing/                Code, data, and the research record
│   ├── campaign/           Hypotheses, experiments, sessions, agendas, and ledger
│   ├── frontier/           Per-case claims, evidence, generated views, and results
│   ├── witnesses/          Witness/v2 interchange and retained examples
│   ├── golden/             Calibration endpoint snapshots
│   ├── atlas/              Known-best, prospective, enumerated, and rendering artifacts
│   ├── resources/          Retained literature and source-faithful transcriptions
│   ├── src/                Maintained sqpack package
│   ├── cases/              Case- and theorem-specific retained code
│   ├── devtools/           Checkers, adapters, generators, and mutation controls
│   ├── benchmarks/         Explicit performance probes
│   ├── tests/              Behavior, command, and architecture contracts
│   ├── sqsearch/           Rust screening annealer
│   ├── defects.yaml        Structured defect log
│   ├── defects.schema.yaml Defect-log contract
│   └── frankensim-probe/   Focused experiments against FrankenSim
├── packages/workbench/     Typed workbench source, tests, probes, and build tools
├── vendor/kpress/          Vendored kpress submodule: the page's rendering layer
├── AGENTS.md               Project instructions for agents
├── CLAUDE.md               Bridge to AGENTS.md
├── Makefile                Markdown formatting, hooks, and skill mirroring
├── biome.json              Biome lint and format config for the browser sources
├── eslint.probes.json      Type information for the probe promise-rule overlay
├── lefthook.yml            Pre-commit Markdown formatter hook
├── package.json            Pinned tooling and private npm workspace declaration
├── package-lock.json       Root and workbench workspace lockfile
├── tsconfig.base.json      The shared TypeScript type floor every program extends
├── tsconfig.devtools-node.json  The Node scripts the Python devtools and tests run
├── tsconfig.n11-lower-bounds-explainer.json The checked classic scripts in the standalone explainer
├── tsconfig.json           The bundled workbench application's entry module
├── tsconfig.motion-lab.json  The motion lab's assets and the slideshow harness
├── tsconfig.overview.json  The site pages' table and math scripts
└── tsconfig.probes.json    The workbench checkers' probes

An optional, Git-ignored attic/ holds intake and scratch files. Sources used by durable research are retained under packing/resources/.