{"id":"palomar/PALOMAR-2026-10-22-000007","url":"https://github.com/dozenalist/ModularFormsMod/tree/585d9fa44e7ada745691c234af53ca6785f175ae","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000007-v1.json","repo":"https://github.com/dozenalist/ModularFormsMod","tags":["math.NT","math.CO","msc:11P83","msc:11F33","msc:05A17","number-theory","partitions","modular-forms","lean"],"score":0,"title":"Ramanujan congruences for the partition function","trust":"high","domain":"math.NT","source":"palomar","authors":["Carter Hastings"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of modular forms over coefficient subrings of the complex numbers, their coefficientwise reductions modulo ring homomorphisms, and a proof classifying the Ramanujan congruences for the partition function following an argument from Ahlgren and Boylan. The recorded results prove Ramanujan's congruences modulo 5, 7, and 11 as well as the fact there there are no other such examples. The proof develops modular forms modulo a prime, filtration, and theta and U operators, using the arguments of Ahlgren–Boylan, Kiming–Olsson, and Swinnerton-Dyer.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Arithmetic properties of the partition function","identifier":"doi:10.1007/s00222-003-0295-6","relationship":"formalizes"},{"title":"Congruences like Ramanujan's for powers of the partition function","identifier":"","relationship":"adapts"},{"title":"On l-adic representations and congruences for coefficients of modular forms","identifier":"","relationship":"adapts"}]}