Hironaka’s resolution of singularities theorem autoformalized in Lean

The team says it autoformalized Hironaka’s 1964 resolution of singularities theorem in Lean. A contributor says Resolution had treated it as an axiom in its learning theory work, but the formal proof now makes downstream work unconditional. They also say downstream agents can examine the full proof.