arxivcs.AI2026-07-02
Reformalization of the Jordan Curve Theorem
Simon Guilloud, Sankalp Gambhir, Samuel Chassot
We present a case study in reformalization, a variant of autoformalization in which the input proof is not natural language but a formal development in a different proof assistant. Concretely, we report three reformalizations of the Jordan Curve Theorem: from Mizar to Lean, from…