{"id":"palomar/PALOMAR-2026-10-09-000013","url":"https://github.com/pmaronow/at-palomar/tree/915bca99f46bad65629ef35c8be4bf8fc962af9a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-09-000013-v1.json","repo":"https://github.com/pmaronow/at-palomar","tags":["math.PR","math-ph","msc:82B44","msc:60G15","spin-glasses","sherrington-kirkpatrick","probability","lean"],"score":0,"title":"Replica symmetry up to the de Almeida–Thouless line in the Sherrington–Kirkpatrick model","trust":"high","domain":"math.PR","source":"palomar","authors":["P. M. Aronow","Patrick Lopatto"],"reviews":0,"subject":"math.PR","summary":"A Lean formalization of the positive-field Sherrington–Kirkpatrick results in Patrick Lopatto's arXiv:2604.11921v2. The selected registry claims are convergence of the expected finite-volume free energy to the concrete replica-symmetric Gaussian formula for beta > 0, h > 0, and AT parameter at most one, including equality; and an exact description of the positive-field AT boundary as a positive strictly increasing smooth graph on beta > 1, tending to zero at beta = 1 from the right, together with (1,0). The repository also contains the numbered PDE, stochastic-process, moment, and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-09","reactions":{},"formalized":true,"formalizes":[{"title":"Replica symmetry up to the de Almeida–Thouless line in the Sherrington–Kirkpatrick model","identifier":"https://arxiv.org/abs/2604.11921v2","relationship":"formalizes"}]}