Papers With

← All papers
First page of Reformalization of the Jordan Curve Theorem

Reformalization of the Jordan Curve Theorem

Simon Guilloud, Sankalp Gambhir, Samuel Chassot

cs.AI Jul 2, 2026 · v1
autoformalization ai-agents formalization topology
Read PDF arXiv abstract Code
TL;DR
LLM-based agentic reformalization ports the Jordan Curve Theorem into Lean from Mizar and HOL Light sources, using Lean's checker as arbiter.
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.
Problem

Translating large formal developments between proof assistants (reformalization) is hindered by mismatched logical foundations and poor library alignment, producing unnatural, non-idiomatic proofs.

Approach

The task takes an existing formal proof as an exact specification and uses an LLM agent with tool use and a verification loop to build a native, idiomatic development in a target assistant. Three case studies port the Jordan Curve Theorem: Mizar to Lean, HOL Light to Lean, and HOL Light to Agda. Workflows involve dependency extraction, catalogue building, skeletons with sorry placeholders, and section-by-section proof filling, keeping the target proof checker in the loop.

Results

Lean targets used well-developed libraries and tooling; the HOL Light to Agda port reached only foundational sections plus parts of section E (about 27,000 lines) and is incomplete. Libraries, tooling, and explicit handling of foundational mismatches (e.g., Agda's empty types) strongly affected success.