{"id":"arxiv/2604.09808","url":"https://arxiv.org/abs/2604.09808","tags":["math.NT","cs.LO"],"score":0,"title":"A formal proof of the Ramanujan--Nagell theorem in Lean 4","domain":"math.NT","source":"arxiv","authors":["Barinder S. Banwait"],"reviews":0,"subject":"math.NT","summary":"We present a complete formalization, in the Lean interactive theorem prover with the Mathlib library, of the Ramanujan--Nagell theorem: the only integer solutions to the Diophantine equation $x^2 + 7 = 2^n$ are $(n,x) \\in \\{(3,\\pm1),(4,\\pm3),(5,\\pm5),(7,\\pm11),(15,\\pm181)\\}$. The formalization includes all dependencies, notably the computation of the ring of integers of the quadratic field $\\mathbb{Q}(\\sqrt{-7})$, its class number, and unit group. We describe the proof strategy, the architecture of the formalization, and the challenges encountered in bridging the gap between textbook proofs…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-10","reactions":{}}