Reformalization of the Jordan Curve Theorem
For proof assistant users, this provides insights into cross-system formalization, but the work is incremental as it applies existing methods to a new case study.
The authors reformalized the Jordan Curve Theorem from Mizar and HOL Light into Lean and Agda, analyzing pipeline design choices for practical reformalization.
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 HOL Light to Lean, and from HOL Light to Agda. We analyse the results and identify pipeline design choices that matter for practical reformalization tasks.