AI-assisted work proposes polynomial-time counting algorithms for spin glasses
A new preprint reports approximate-counting algorithms for several spin-glass models, with an unusually detailed account of model assistance and a companion Lean project.
An AI-assisted route to counting a difficult physical system
A preprint submitted on October 27 presents algorithms for approximating the partition function of the Sherrington–Kirkpatrick (SK) spin-glass model and certain mixed Ising p-spin models. Partition functions summarize an enormous collection of possible states in a physical model; computing them accurately is a central mathematical and algorithmic challenge.
The claimed result
The paper studies a specified high-temperature regime, below a threshold defined in the manuscript, with homogeneous weak external fields. Its algorithm approximates the logarithm of the partition function to a requested additive error and gives a polynomial bound in the system size, inverse accuracy, and inverse failure allowance. For higher-order mixtures the proposed procedure is deterministic; for the SK case it uses randomized color coding. The reported guarantee also includes a disorder-tail term and counts exact arithmetic operations rather than bit complexity or floating-point cost.
These are claims in an unreviewed preprint. They apply only under the stated assumptions, and MathsAI has not independently checked the proofs, implementation, novelty, or the comparison with concurrent work.
An unusually specific AI disclosure
What makes this item relevant to mathematical AI is the author’s disclosure. The paper says the initial cluster-expansion direction came from the author, while GPT-5.6 Pro suggested a polynomial-time higher-order algorithm. It says later work with GPT-6 Pro helped develop the SK truncation schemes, color-coding approach, and lower-tail argument; Codex was used for literature search, figures, and a companion Lean formalization. The author writes that they checked the proofs, revised the manuscript, and accept responsibility for its mathematical claims.
The linked Lean repository gives useful boundaries to that description. It says its formal development covers execution, estimators, stated accuracy guarantees, and operation bounds for the fixed algorithms, but not the general reverse-hypercontractivity theorem in full; it formalizes the specialization used by the manuscript instead. A Lean check can be powerful evidence about the encoded statement and dependencies, not an automatic independent verdict on whether the model, assumptions, or informal claim capture every intended aspect.
Why the record matters
This preprint is not simply a result with an AI acknowledgement. It records a division of labour: a human supplied a direction and review, models proposed and developed parts of an algorithmic argument, and a formal artifact states what was checked. That level of provenance makes a technical claim easier for other mathematicians to inspect—even as peer review and independent replication remain essential.