Full-RSB in the Sherrington–Kirkpatrick spin glass

What the AI did

The most explicit authorship disclosure in this catalog. The manuscript's opening note says the proof arguments and prose "were generated by the same model from prompts supplied by Hong-Bin Chen", and then states on its own line:

"ChatGPT 5.6 is the author of the manuscript."

It continues: "Since arXiv's policy on generative AI language tools does not permit such a tool to be listed as an author, Hong-Bin Chen is only formally listed as the author for submission purposes and assumes full responsibility for the submitted text. This formal attribution reflects arXiv's policy rather than the division of labor in producing the manuscript: Hong-Bin Chen's role was limited to prompting, editing, proofreading, and verifying the arguments; in particular, he did not construct the proof arguments. He has read and verified the proofs, although errors or oversights may remain."

The Lean development was also written by the same model. AI-discovered is unambiguous here: a human posed the problem and checked the output, and states outright that he did not construct the argument.

Verification

Unreviewed, and the tier was lowered from Lean-checked on inspection of the repository - a labelling correction, not a doubt about the mathematics.

What holds: across 75 files and 5,544 lines of Lean 4 there is no $\texttt{sorry}$, no $\texttt{admit}$ and no $\texttt{native\_decide}$, confirmed on 28 August 2026. What does not: the Lean-checked rung requires no stray axioms, and this project declares seven mathematical axioms in $\texttt{ExternalInputs.lean}$. Three cite prior work (Lopatto, Auffinger-Chen, Chen-Handschy-Lerman), but four stand in for the paper's own unformalized analysis - the minimizer itself, and the analytic data behind Propositions 4.1-4.2, 4.3 and 4.4. The repository's own ledger also marks several items "Open analytic", and notes that four terminal approximation modules are "excluded from the root target and omitted from this GitHub bundle".

What the formalization does establish is real and is credited: given that analytic data, the gap exclusions and the smooth-density conclusion are Lean deductions rather than assumptions, as AXIOMS.md is careful to state. The repository is unusually candid - it ships an axiom ledger and a dependency table, and the paper's own footnote says "This is not an assumption-free verification of the entire paper". The project was not built here, for want of a toolchain. The paper is an unrefereed preprint and no human has independently reviewed the analysis.

Source

• PaperFRSB IN THE SK SPIN GLASS: CONVERGENCE TO FULL-INTERVAL SUPPORT AT ZERO TEMPERATURE