{"ID":5675143,"CreatedAt":"2026-07-03T01:40:09.565152011Z","UpdatedAt":"2026-07-05T05:29:26.995498422Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.01734","arxiv_id":"2607.01734","title":"Reformalization of the Jordan Curve Theorem","abstract":"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.","short_abstract":"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...","url_abs":"https://arxiv.org/abs/2607.01734","url_pdf":"https://arxiv.org/pdf/2607.01734v1","authors":"[\"Simon Guilloud\",\"Sankalp Gambhir\",\"Samuel Chassot\"]","published":"2026-07-02T05:44:10Z","proceeding":"cs.AI","tasks":"[\"cs.AI\"]","methods":"[]","has_code":false}