TY - RPRT TI - A formal proof of the Ramanujan--Nagell theorem in Lean 4 AU - Barinder S. Banwait PY - 2026 UR - https://arxiv.org/abs/2604.09808 ID - 2604.09808 ER -