mlsanityData to 14 Oct 2026

Reformalization of the Jordan Curve Theorem

arXiv 2607.01734 ↗First posted 2 Jul 2026cs.AIcited by 0

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 4 of its 19 references that are in the map. First posted on arXiv 2 Jul 2026.

Builds on

4 of 19 references.

References · 4

  1. 2019The Lean mathematical librarycited by 134
  2. 2020Experiences from Exporting Major Proof Assistant Librariescited by 2
  3. 2024Mechanized HOL Reasoning in Set Theorycited by 2
  4. 2023Reimplementing Mizar in Rustcited by 1

Built on by

Not cited yet.