How a result earns its place.

1. A question

   We choose it: usually a named open problem, or a sharper form of one. Before work starts we write down what would show the expected answer wrong.

2. Exploration

   Many model instances, from more than one developer, work on the problem in long sessions, in parallel, building on and challenging each other’s results. We set the direction and decide which lines to pursue and which to drop.

3. A blind check that tries to refute

   Before a result is kept, a model that has not seen its proof, usually from a different developer, first tries to refute the statement, then audits the proof line by line.

   Catchesfalse statements, gaps, and statements stronger than their proofs.

4. Exact computation on independent engines

   Finite claims, constants and certificates are computed with exact arithmetic where possible, on at least two independently written engines. The programs, their recorded outputs and checksum manifests ship with the paper.

   Catchesnumerical and transcription errors, unless every engine shares them.

5. Whole-paper audits

   Each paper goes through rounds of adversarial audit by readers that have not seen it, alone and together with its companion papers, with literature searches for priority and credit. Fix rounds follow each audit, and a fresh audit follows each fix round.

   Catcheserrors between sections, misplaced credit, and claims the paper does not prove.

6. Lean, where it matters most

   We are formalizing the main theorems in the Lean 4 proof assistant with Mathlib, paper by paper, and every formal proof is checked to use only the standard axioms. Each paper says exactly what is formalized so far.

   Catchesany gap in the formalized part.

7. Release

   A public repository with the source, the checks and their recorded outputs; a DOI for every version; a statement of what was checked and what was not.

8. Corrections

   Errors found after release are corrected in a new version and listed below, with what was wrong and what changed.

• An error every method shares. In August 2026 two engines agreed on a step in our I₃₃₂₂ work because both had been written from the same transcription; a later exact audit found the error, and the claims were withdrawn publicly the day after release. An engine that copies another’s transcription now counts as the same engine. The record
• What Lean does not formalize. A formal proof covers its own statement and nothing else, and a formal statement can differ from the intended one. Statement fidelity is audited separately.
• Work we have not found. Literature searches miss work that is new, unindexed or posted elsewhere. When concurrent work comes to light after a release, we add a note.
• Our own blind spots. Every check described here is internal, and none of it is journal peer review. One paper on this site, an earlier single-author paper, has been published in a journal; no joint paper has been through journal review yet.

Any change that fixes something a released version got wrong: a mathematical error, a claim stronger than its proof, wrong or missing credit, a wrong citation, or faulty packaging of the checks. A new version that only adds results is a release, not a correction.

1. 1 Nov 2026
   • ReleaseExact transport and spectral dimensions for the almost Mathieu operator v2.0.1 10.5281/zenodo.23864352Correction. Remark 9.11’s table of numerical illustrations had entries that did not match the quantity it states, the strict outside probability; version 2.0.1 corrects them and states how they were computed. Smaller precision fixes and two citation locators. No theorem or proof was affected. Found by a blind audit and its fix-check.
   • ReleaseExact transport and spectral dimensions for the almost Mathieu operator v2.0.0 10.5281/zenodo.23848977Correction. The outer-barrier lemma (Lemma 4.1 of version 1.0.0) allowed the endpoint J = 0 with V₀ = W, where its bound reads 0/0; version 2.0.0 adds V₀ > W. A Lean blueprint of the paper found it. No application is affected: every use has J = 1 and a strict gap. Version 2.0.0 also strengthens Theorem B and enlarges the phase set.
2. 30 Oct 2026
   • ReleaseFinitely presented infinite p-groups for every prime v1.0.1 10.5281/zenodo.23791059Correction. Credit: a “Note added” in the introduction cites Kenta Kitamura’s independent, concurrent work (manuscript 13 October 2026, Lean 16 October 2026), which also proves the every-prime result; in the paper’s words, “the extension to every prime listed above is shared with it.”
   • ReleaseThe price of keeping time v1.1.1 10.5281/zenodo.23790746Correction. Version 1.1.0 said, in the batch-law appendix, that a minimizing Y need not exist. The infimum is attained (Rockafellar, Convex Analysis, Theorem 28.2). No result depended on the sentence.
3. 29 Oct 2026
   • ReleaseUncomputable critical exponents v2.1.0 10.5281/zenodo.23780285Correction. Packaging: version 2.0.0 stored text files with line-ending conversion, so some checksum-manifest entries did not verify from a fresh clone. Version 2.1.0 stores files byte for byte.
   • ReleaseThe price of unreachable perfection: dimension laws at every regular scale v1.0.1 10.5281/zenodo.23774171Correction. Packaging: version 1.0.0 omitted the recorded check outputs listed in its checksum manifests, and one manifest entry was stale. The paper is unchanged.
   • ReleasePerfect play in a binary-scoring nonlocal game requires infinite dimension but only finite energy v2.0.0 10.5281/zenodo.23772890Correction. Packaging: versions 1.0.0 and 1.1.0 omitted the recorded outputs of the finite checks. Version 2.0.0 includes them.
4. 26 Oct 2026
   • ReleaseKaplansky's conjectures fail for torsion-free hyperbolic groups in positive characteristic v1.0.2 10.5281/zenodo.23673698Correction. A sentence of the introduction attributed the zero-divisor conjecture to all cubulated groups; Agol’s theorem gives it for cubulated hyperbolic groups. No mathematical statement changes.
5. 18 Oct 2026
   • ReleaseThe Resource Theory of Complexness References in Real Quantum Networks v1.0.4 10.5281/zenodo.23457692Correction. A remark expected asymptotic equivalence at rate one; it is false, because the unit reference copies itself exactly. Version 1.0.4 adds the exact-replication lemma and corrects the remark.
6. 14 Oct 2026
   • ReleaseThe Lovász number is not alone: a continuum of Rényi points in the entanglement-assisted spectrum of graphs v1.2.1 10.5281/zenodo.23375704Correction. Credit added to Oufkir, Yao and Berta for the data-processing inequality behind non-signalling simulation, and to Wang and Duan (2018); Shariat, Hoogsteder-Riera and Tomamichel are described as giving an alternative proof. Section 1.1 said “the first three” terms of the Duan–Winter chain are radii, which would have included S_NS; corrected. A verification section that printed a number matching no statement of the paper is removed.
   • ReleaseKaplansky's conjectures fail for torsion-free hyperbolic groups in positive characteristic v1.0.1 10.5281/zenodo.23374592Correction. Version 1.0.0 gave the author order wrongly. Version 1.0.1 lists Nidhal Mghirbi, Seth Douglas.
   • ReleaseNon-soficity of OpenAI's torsion-free hyperbolic group v1.1.0 10.5281/zenodo.23374284Correction. Alongside new results: the note of Sandhu and Thom is described correctly and credited with its authors; Ivanov (arXiv:2610.17662) is credited for torsion-free zero divisors in odd characteristic; credit added for Ozawa and Pestov, Kun, Kun and Thom, Elek and Szabó, Alon, Hall, Knauer, Pinchasi and Yuster, and others; a corollary now states only its new part. The non-soficity argument is unchanged.
7. 13 Oct 2026
   • ReleaseNon-soficity of OpenAI's torsion-free hyperbolic group v1.0.1 10.5281/zenodo.23345877Correction. Incomplete credit in version 1.0.0. Version 1.0.1 cites Chapman and Peled’s conditional construction, Soulé’s torsion bound and Thom’s independent note based on Sandhu’s construction. No mathematical change.
   • ReleaseThe Lovász number is not alone: a continuum of Rényi points in the entanglement-assisted spectrum of graphs v1.1.1 10.5281/zenodo.23328240Correction. Credit and precision, after an attribution audit and a referee audit that found no false result: θ₀ = θ is credited to Schrijver (as Dalai’s Theorem 8), to Duan and Winter, and to Cabello, Severini and Winter; Wang and Duan’s answer to Duan and Winter’s question, Vrana’s continuum on C₅ in the ordinary spectrum, Li and Zuiddam, and others are credited; a figure caption’s witness radius had been rounded in the unsafe direction. No theorem changes.
8. 12 Oct 2026
   • CorrectionThe four thermodynamics papers of 11 OctoberCorrection. The four thermodynamics papers of 11 October cited Thompson et al. with a DOI that did not resolve. Version 1.0.2 of each paper gives the correct DOI, 10.1103/dryx-l5rt.
9. 3 Oct 2026
   • ReleaseAmenable groups with nearly exponential sofic profile, and quantum channels that need nearly linear memory v1.1.2 10.5281/zenodo.23111927Correction. Credit added in the introduction: Gromov and Weiss; OpenAI’s announcement, Fournier-Facio, and Kun and Thom on non-sofic groups; Slofstra and Vidick, and Slofstra; Arzhantseva and Cherix; and work on channel simulation, memory costs and collision models.
10. 2 Oct 2026
    • ReleaseAmenable groups with nearly exponential sofic profile, and quantum channels that need nearly linear memory v1.1.1 10.5281/zenodo.23108312Correction. Precision: a step in an appendix’s Choi-rank count is corrected (the bound is unchanged), and a set of coefficients is corrected from {±1, ±2^−1/2} to {1, ±2^−1/2}.
11. 30 Sep 2026
    • ReleaseAmenable groups with nearly exponential sofic profile, and quantum channels that need nearly linear memory v1.0.2 10.5281/zenodo.23070871Correction. Credit made precise: Cornulier’s dichotomy and his facts on local embeddability, Lee’s Dehn function, Johnson’s presentation, and Brown, Brin, and Hennig and Matucci for finite presentation are cited where they are used, as are the lemmas taken from the companion papers.
    • ReleaseCausal quantum-channel simulation: memory beyond entropy v1.1.2 10.5281/zenodo.23070870Correction. Credit and scope: that the cost vanishes on the closure of finite tracial factorizations is credited to the closed-device preprint, and this paper proves the converse; “polynomial memory at every exchange rate” is scoped to purity limited to O(log n); Watrous is credited for a relative-interior fact.
    • ReleaseHoughton's group H₃ has superpolynomial sofic profile v1.1.2 10.5281/zenodo.23070869Correction. Credit made precise: Cornulier’s linear lower bound and bounded cases, Lee’s reduction of the Dehn function, Elek and Szabó’s construction, Arzhantseva and Cherix, Röver, and the known birational consequences are credited where they are used; Slofstra’s earlier chunk is described exactly, with its exponent, near 1/4, larger than ours. The mathematics is unchanged.
    • ReleaseThe Lovász number is not alone: a continuum of Rényi points in the entanglement-assisted spectrum of graphs v1.1.0 10.5281/zenodo.23066485Correction. Version 1.0.0 stated that both pentagon geometries in Figure 4 are nonoptimal throughout 0 < α < 1/2; the displayed bounds do not show this. Version 1.1.0 states only the proved regimes. The package also corrects a SHA-256 digest in the certificate README.
12. 24 Sep 2026
    • ReleaseHow much dimension does an epsilon-approximation to a non-attained quantum correlation cost? A Diophantine answer for K₅ v1.0.2 10.5281/zenodo.22944181Correction. An open lemma of versions 1.0.0 and 1.0.1 conjectured that marginal drift δ costs δ^−1/2. It is false: an explicit two-block carrier has deficit exactly zero with drifted marginals. Version 1.0.2 proves the cost Θ(min(ε^−1/4, δ^−1/4)).
13. 16 Sep 2026
    • ReleaseBath dimension and initial entropy for closed repeated use of a quantum channel v1.1.0 10.5281/zenodo.22788806Correction. A displayed lower bound, 0.045566, had been rounded up from 0.0455659970, and a growth remark failed at r = 0. Version 1.1.0 uses a stronger exact witness and restates the remark.
14. 11 Sep 2026
    • ReleaseThe I₃₃₂₂ quantum value is attained spatially but not in finite dimension v4.1.0 10.5281/zenodo.22698978Correction. Proof correction to version 4.0.0. The lower bound had identified paired components without justification; it now uses a weighted flow over all retained edges. The limiting-weld justification, an endpoint-gap constant, the spatial amplitude notation, the mixed-state argument and two upper-rate constants were also corrected. Concurrent independent work by Pauwels and by Coladangelo is credited. The main statements and the upper coefficient are unchanged.
15. 25 Aug 2026
    • ReleaseHow much dimension does an epsilon-approximation to a non-attained quantum correlation cost? A Diophantine answer for K₅ v1.0.1 10.5281/zenodo.22099141Correction. Credit: version 1.0.0 said that Coladangelo’s embezzlement proof of non-closure (arXiv:1904.02350) comes with no rate; its abstract states an explicit dimension lower bound, 2^Ω(ε−1/8). The priority statement is now scoped to the K₅ witness. The theorem and constants are unchanged.
    • ReleaseThe I₃₃₂₂ quantum value is attained spatially but not in finite dimension v4.0.0 10.5281/zenodo.22099128Correction. Alongside merging the rate note into the paper: Theorem (S) restated with its locality constraint, which the earlier statement did not formally require; the orbit structure of Section 4 corrected; Pál and Vértesi’s conjecture positioned against their paper; the minimality argument completed; the priority claim for the rate narrowed and sourced; an endpoint-mass bound stated correctly; one displayed constant corrected from 0.9197272 to 0.91972725.
16. 13 Aug 2026
    • ReleaseThe Resource Theory of Complexness References in Real Quantum Networks v1.0.3 10.5281/zenodo.21911918Correction. Packaging: the verification suite of version 1.0.2 had a machine-local import path and a missing module, so it did not run from a clean clone. Version 1.0.3 repairs it and scopes a footnote to Corollary 7.3 to the surviving sector.
    • ReleaseThe Resource Theory of Complexness References in Real Quantum Networks v1.0.2 10.5281/zenodo.21911717Correction. The general clause of Corollary 7.3 was false for arbitrary frame codes; explicit counterexamples are given. The corollary now states the exact alignment and disjointness condition, and the guarantee for the target pair is unaffected.
    • ReleaseThe Resource Theory of Complexness References in Real Quantum Networks v1.0.1 10.5281/zenodo.21910329Correction. Version 1.0.0 called the accounting of the auxiliary descent unit-neutral at best; the paper’s own protocol is nondemolition, so each descent is net positive and catalytic. The corollary is corrected; no other statement is affected.
17. 6 Aug 2026
    • ReleaseThe I₃₃₂₂ quantum value: certified window, spatial attainment, finite-dimensional nonattainment, and the Cqs/Cq separation v3.2.3 10.5281/zenodo.21826916Correction. A fresh audit of the version 3.2.2 corrections found nine items, all fixed: the Mghirbi reference corrected to the right record, the 2018 attribution weakened to what the source says, other citations repaired, and stale withdrawn claims removed from the README and citation metadata. Nothing mathematical changed.
    • ReleaseThe I₃₃₂₂ quantum value: certified window, spatial attainment, finite-dimensional nonattainment, and the Cqs/Cq separation v3.2.2 10.5281/zenodo.21817385Correction. After three adversarial audits of the resolution paper: retitled to the statement it proves; two false decimal bounds fixed; credit added for N. Mghirbi’s earlier exact enclosures and for an implication in Dykema, Paulsen and Prakash (2018); the minimality claim scoped; attributions, definitions and bibliography corrected. The theorems are unchanged.
    • ReleaseThe I₃₃₂₂ quantum value: certified window, spatial attainment, finite-dimensional nonattainment, and the Cqs/Cq separation v3.2.1 10.5281/zenodo.21816638Correction. Packaging: version 3.2.0 shipped the resolution paper, but a tooling slip dropped the README and metadata edits that go with it. Version 3.2.1 restores them.
18. 5 Aug 2026
    • ReleaseThe I₃₃₂₂ quantum value: a certified two-sided window and correction record v2.0.0 10.5281/zenodo.21799071Correction. Versions 1.0.0 to 1.2.0 withdrawn. Our own exact audit after release found a nonzero mismatch in the construction behind their claims; both computation engines had inherited the same transcribed step. A rebuilt proof followed as version 3.0.0.

The thirty-three entries are the corrections named in our release notes, changelogs and commit messages, and the credit, precision and citation fixes found when every patch release from August to October 2026 was reread against the version before it.

A confirmed error is fixed in the next version of the paper and listed here. Earlier versions stay archived under their own DOIs.

Every result carries four labels: verification, Lean, peer review and novelty. Novelty is stated as one of these values: new; new, with named precedent; new, with named precedents in form; new, with named prior work; concurrent with named independent work; new proof of a known result; extends named prior work; unifies named prior results; synthesis of prior work (credited). The last is for a paper whose contribution, in its own words, is to bring earlier results together and present them, with each credited; we use it only when the paper describes itself so. We make no claim of priority without a dated citation, and the credit on the site matches the credit in the paper.

The process above is how the joint papers are made. Nidhal Mghirbi’s earlier single-author papers predate it: their verification label says “the author’s own checks” and names the reproducibility package where there is one, and nothing on this site implies our blind-audit process for them. A peer-review label other than “not yet” requires a journal’s own record of publication; a Zenodo resource type is not enough.

Labels are dated. When a paper changes, its label is checked again.

Three tools turn a numerical search into a statement checked in exact arithmetic. Each is released with its paper or as a package on Zenodo; their checks are the author’s own, and none is peer reviewed yet.

1. ACSP: proof-carrying affine symbolic search

   A calculus for bounded, finite-depth searches in one integer parameter with rational affine registers. Exact valuation classes, congruence preimages, affine cuts and exact updates give partitions into progressions with locally checkable witnesses, so that acceptance rests on a local certificate contract rather than on rerunning the search; the verifier’s cost follows the proof representation, not the population it represents.

   Paper: Proof-carrying affine search with valuation guards and compressed progression certificates (Zenodo, 14 September 2026). Package: ACSP Symbolic Search Package, version 3.0.0.

2. Certified moment completion and structured noncommutative SDP post-optimization

   Turns a verified Gram matrix into a reusable optimization state. A completion theorem attaches a certificate for the full problem to intermediate dual states without assuming numerical optimality, and the remaining gap splits into an optimization part and a consistency part. Its Bell benchmark is I₃₃₂₂, where a new dual witness turns a numerical suggestion into an exact statement.

   Paper: Certified Moment Completion and Structured Noncommutative Semidefinite Postoptimization (Zenodo, 14 September 2026).

3. Exact semidefinite post-optimization

   The reproducibility compendium for the paper above. Its acceptance paths use exact integer and rational arithmetic; in its own words, numerical optimization “discovers candidates; it is not a condition of theorem acceptance.”

   Package: Exact Semidefinite Postoptimization: a reproducibility compendium (Zenodo, 14 September 2026). The exact I₃₃₂₂ bounds follow the same rule.

Our joint papers are the work of their authors together with AI models from more than one developer. The authors take responsibility for every claim.

The authors set the direction throughout: they choose the questions, decide which lines to pursue and which to drop, and judge and select the results. The models do most of the exploration, derivation, computation and drafting. Models are not listed as authors.

Every paper first released on or after 12 October 2026 includes a section titled “How this work was done” that describes the process for that paper and says what is checked by machine and what is proved only in the text. Reports of the independent checks are available from the authors. For Nidhal Mghirbi’s earlier single-author papers, each paper’s own text is the record of how it was done.

The text of this site is licensed under Creative Commons Attribution 4.0 International (CC BY 4.0): you may share and adapt it for any purpose, with credit to finite.works and a link to the page. Each paper, its source and its code carry the licence stated in its repository, and the PDFs hosted here are the released files under their papers’ licences. The Libertinus typefaces are used under the SIL Open Font License 1.1.