# Reformalization of the Jordan Curve Theorem

arXiv: https://arxiv.org/abs/2607.01734 · HTML: https://mlsanity.com/paper/2607.01734/

## 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 (most cited first, 4 of 4)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Experiences from Exporting Major Proof Assistant Libraries](https://mlsanity.com/paper/2005.03089/) (2020)
- [Mechanized HOL Reasoning in Set Theory](https://mlsanity.com/paper/2403.13403/) (2024)
- [Reimplementing Mizar in Rust](https://mlsanity.com/paper/2304.08391/) (2023)

## 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.