Mohsen Khalili and Sara Gharabaghi report that k2−5k2−5 unit squares need a square of side $k$k for every $k\ge 7$k≥7. One periodic family of measures reduces every $k\ge 10$k≥10 to a single finite statement on an $11\times 11$11×11 board, which the authors decide with Daniel’s checkers and a new Tight-Tile Lemma where box subdivision stalls. New to the record are eight open counts, $n=116$n=116 to $319$319. T-298 is reported at V0/C1.

• $k=7$k=7, $8$8 and $9$9 rest on certificates the record already holds (T-252, T-066 and T-184), and $s(95)=10$s(95)=10 is Greff’s T-191. At $n=116$n=116 to $319$319 the reported lower bounds move to $k$k; the verified ones are unchanged.
• What the import lane ran, about 2.5 CPU-hours: the source’s fast checks, 30 of the 55 columns of the source’s zmx2 sweep, root 9632 with both checkers and 26 of the 323 Tight-Tile jobs, each equal to the source’s records, and the source’s controls, refused as reported. That is a diagnostic, not a replay. The full replay, about 145 to 180 CPU-hours, up to about 320, and the Lean build are held for the owner.
• A stage 4 review by a separately prompted Claude agent, at the strong tier rather than the strongest the runbook asks for, found no blocking defect and two major findings: zmx2’s area-density and first-order lemmas, on which most of the board’s poses rest, have no review in this record (F1; a review of them is held), and the Tight-Tile Lemma has one implementation and no full replay (F2).
• The paper says the search, the certificate, the Tight-Tile checker and its proof, and the verification runs were produced with Claude (Anthropic) under the authors’ direction, and that the authors reviewed the method, the checks and the text. It builds on Daniel’s linear program, format, checkers and Lean reduction. The source reports no review by outside mathematicians.

Eight counts take new house best packings after clean-room reviews here. Daniel’s certificates of #845 take 172, 204, 260 and 293, and his update to #824 takes 299. Couzo’s certificates of #844 take 232 and 307. Couzo’s #843 packing takes 130, in Polkovskyi’s re-solved certificate of #846, 2.08×10−122.08×10−12 lower. Each is regularized for display, and T-254 to T-259 are confirmed at V3/C3.

• The margins below the packings they replace are 2.05×10−32.05×10−3 at 130, 1.05×10−31.05×10−3 at 172, 1.02×10−31.02×10−3 at 204, 2.51×10−32.51×10−3 at 232, 1.18×10−21.18×10−2 at 260, 1.64×10−41.64×10−4 at 293, 2.16×10−22.16×10−2 at 299 and 1.61×10−31.61×10−3 at 307. At 293 and 299 the houses had been the Kingbird catalogue’s constructions, $723/41$723/41 and 33/2+7​/233/2+7/2, and the case records’ conjectured optima there are withdrawn.
• Daniel’s packings are new arrangements found by his population searches and, at 299, from his packing of 26 October; the 293 is his 260 plus one L-shaped strip. Couzo’s refine public Kaggle notebook packings, Chilton’s at 232 and ntumlnoob’s at 307; at 307 the new arrangement is his certificate of 28 October (T-255), which #844 refines.
• This project’s two maintained exact routes decided every certificate, sharing components with the sources’ checkers. Separately prompted mathematical reviews by Claude agents decided them again on clean-room checkers of their own, which is the independent confirmation; the reviews ran at the strong tier rather than the strongest the runbook asks for. No source program ran here.
• Six cases draw grid-slack’s views at the certificates’ sides; 299 and 307 keep the axis tool’s view. Fourteen sub-print re-certifications by Polkovskyi wait on the maintainer’s question of whether the 23 October restatement ruling reaches them, and move no house. Upper bounds only; no optimality, rigidity or priority is claimed.

Couzo’s certificates of #763 at 268 and 303 pass a clean-room review here and become the house best packings there, 4.45×10−34.45×10−3 and 2.78×10−32.78×10−3 below the packings they replace, each regularized for display. T-240 is confirmed at V3/C3.

• Each refines a public Kaggle notebook packing: Tymchishin’s at 268, and at 303 Couzo’s own push packing, which his manifest credits after Lavrentev’s. Each is a new arrangement relative to the record: 118 and 133 squares lie more than a tenth from their places in the packings they replace.
• This project’s two maintained exact routes decided both certificates; they share components with the source’s pipeline, whose manifest names this repository’s sqpack/verify.py as its first checker. A separately prompted mathematical review decided them again on a clean-room checker of its own, by a Claude agent, which is the independent confirmation. No source program ran here.
• Both cases draw grid-slack’s views at the certificates’ sides. Daniel’s later 268, 4.48×10−124.48×10−12 lower, is another placement of the same arrangement, validated separately; it re-houses 268 in a later change. Upper bounds only; no optimality, rigidity or priority is claimed.

Daniel’s packing at 182, cut from Couzo’s 211 packing, an arrangement of Ostashev’s design, and polished, passes a clean-room review here. At 13.970916436215, 3.17×10−33.17×10−3 below the packing it replaces and a new arrangement relative to the record, it becomes the house best packing at 182. T-243 is confirmed at V3/C3.

• This project’s two maintained exact routes decided the certificate, and a separately prompted mathematical review decided it again on a clean-room checker of its own, by a Claude agent, which is the independent confirmation. No source program ran here.
• The case draws the regularizer’s view at the certificate’s side, which is Daniel’s own regularized certificate, square for square.
• Upper bounds only; no optimality is claimed. Local minimality is the source’s numerical report.

The record now holds, as a report, a Lean 4 proof by jatloe that the $4\times 3$4×3 grid is the optimal packing of 12 unit squares: $s(12)=4$s(12)=4. It is the first optimality claim the project’s records hold at 12, one of the five open cases below 21; if the proof holds, it closes the gap of $0.0285$0.0285 between the verified lower bound, $7943/2000$7943/2000, and the grid’s side. T-245 remains reported at V0/C0; the Lean build has not been replayed here.

• Lean’s kernel checks the geometric arguments and the assembly, and 1,624 finite facts are decided by native_decide, so Lean’s compiler is trusted as well. The source reports that a run in a repository that is not public accepted all 5,377 modules of the theorem’s closure on compiled objects reused from an earlier run, and says that no full rebuild has been run.
• A statement audit of 25 October, an AI review, read the theorem as the unrestricted problem with no premise, and mapped the 1,624 facts of the source’s axiom log one to one onto the code’s calls. It did not read the proof, so it moves no rung. A mathematical review of the written proof and a complete build, about 28 CPU-hours by the source’s own receipts, come next.
• Jatloe wrote the proof and a partial formalization, Ben Gurevitch aided the formalization, and ctjlewis refactored and compiled it. Ahmed published it on 16 October and announced it on 22 October.
• The same change registers Daniel’s S3 report that the side of the best known packing of 29 squares is a root of an integer polynomial of degree 7213 (T-246), also at V0/C0.

Fitzharding reports a Lean 4 proof that Wainwright’s 1979 packing of 19 unit squares is optimal: s(19)=3+42​/3=4.88561808316412…s(19)=3+42/3=4.88561808316412…. It is the first optimality claim the project’s records hold at 19; if the proof holds, it closes the gap of about $0.0606$0.0606 between the verified lower bound, $193/40$193/40, and Wainwright’s side. T-194 remains reported at V0/C1; the Lean build has not been replayed here.

• Lean’s kernel checks the geometric arguments, and 4,320 finite certificate facts are decided by native_decide, so Lean’s compiler, its native evaluator and the C toolchain are trusted. The source reports a kernel replay of the theorem’s import closure that takes those facts as axioms, and says a complete rebuild from its published sources has not yet been run.
• A separately prompted mathematical review of 16 October found no blocking or major defect. It checked the statement and decided the endpoint packing exactly, re-derived the six-step chain to the final theorem, and with programs of its own re-established what each of the 2,328 native facts in the Git tree certifies. The 1,992 facts in the release archives were scanned but not re-run.
• The proof builds on Fitzharding’s 17-square formalization (T-154), whose checker modules it compiles. The source says it was developed with substantial assistance from Claude and Codex.

The Explanations page pairs a short introduction to square packing with an advanced tutorial. Beginners can start with bounds and small examples; the companion develops linear programs, exact certificates, regularization and global proofs.

• Existing tutorial links lead to the moved explanations. The two tutorials retain the definitions, notation, worked derivations, figures and sources.
• News has its own page, with individual articles and filters for significance and topic. Reported proof announcements keep verification limits beside the claims.
• The Explanations index links the tutorials, research papers, downloadable PDFs, film and interactive Workbench. Both web Atlas views use the available screen width.

Fang reports a construction packing k2−k+1k2−k+1 unit squares in a square of side less than $k$k, for every integer $k\ge 15$k≥15. Hosono reports a closed-form lower bound for every non-square count $n\ge 49$n≥49, raising 154 reported case bounds. The register adds these two families and 22 other results. Fang’s theorem has a mathematical review; Hosono’s complete formula replay remains unfinished.

• The 24 records, T-161 through T-184, preserve report order. No new packing is adopted in this registration.
• Couzo, Ostashev, PingYou Ltd and Polkovskyi supplied smaller packings and tighter certificates at 69 counts. Their source certificates were replayed; independent review and adoption remained pending at this date.
• Hosono also reports lower bounds at 37, 39, 44 and 145 through 149 squares. Greff reports an optimality proof for 76 squares. These reports retain their separate verification limits.
• Independently verified lower bounds are unchanged. Each case record distinguishes reported bounds from independently verified ones.

Fitzharding reports a Lean 4 proof that Bidwell’s 1998 packing of 17 unit squares is optimal: $s(17)=4.67553009360455\dots$s(17)=4.67553009360455…. It is the first proof-assistant proof of this value in the project’s records and uses a different argument from Overbeck’s candidate proof. T-154 remains reported at V0/C1; the full Lean build has not been replayed here.

The source comparison traces 32 of the 35 patterns to the project’s certified sub-pattern ledger, including eleven from Hosono (wand125). The review distinguishes those mathematical sources from Fitzharding’s formalization and reported build.