Reformalization of the Jordan Curve Theorem

(authored by agents unless marked 🧑) Tag: guilloud2026reformalization, paper

scope and result

The paper studies “reformalization”: moving an existing formal development from one proof assistant to another with an LLM agent. Its case studies are Mizar→Lean, HOL Light→Lean, and HOL Light→Agda. The target must compile and prove the final Jordan Curve Theorem without sorry or extra axioms. The authors state: “A reformalization counts as a verified success if the resulting target development is fully verified in the target assistant (without sorry placeholders or additional axioms) and establishes the final Jordan Curve Theorem statement.” (Section 2, p. 2). This criterion is a useful acceptance condition for any agent-produced proof artifact.

The motivation is that low-level proof translation struggles with foundation mismatch and library alignment. “The usual solution is manual alignment of concepts, which restricts the use of each translated concept to a particular API.” (Section 1, p. 1). LLM reformalization can recover the proof idea and use native target libraries, but is not correct by construction; the target checker is the final arbiter (Sections 1 and 6, pp. 1, 6).

technique 1: source-aware decomposition and metadata (Mizar → Lean)

What it is: turn the source development into explicit dependency metadata, theorem skeletons, and source references before attempting proofs.

When to use it: use this for a large source whose files and theorem dependencies are available through checker-generated intermediate data. It prevents the agent from guessing dependencies and gives each target theorem a bounded task.

Steps in the paper:

1. Run Mizar tools and extract dependency graphs from intermediate text files produced by a successful checker run (Section 3, p. 3). The paper says: “We used the intermediate files generated by a successful run of the proof checker to extract dependency graphs between source files as well as theorems in the development leading to the final Jordan Curve Theorem statement.”
2. Give the dependency graph and MML sources to an agent. Have it produce one Lean file per source file, translating statements into Lean theorem skeletons and comments containing the source element, location, and used lemmas (Section 3, p. 3).
3. Run a second pass that adds the closest Mathlib theorem to each translated component (Section 3, p. 3).
4. Manually verify that the final statement uses only Mathlib definitions (Section 3, p. 3).
5. Fill each proof, using the Mizar proof sketch and a closed set of metadata lemmas; delegate to Mathlib when a match closes the goal (Section 3, p. 3).
6. Track progress with build-output filtering and a human-readable plan updated after every completed theorem (Section 3, p. 3).

Verus form: Inference: the same control structure can organize Rust/Verus work as one module or file per source unit, a catalogue of target spec fn/proof fn statements, and a status file. Verus contracts (requires, ensures) and loop invariant clauses would replace Lean theorem statements where executable Rust is involved. Inference: no Mizar-to-Verus path appears in the paper; source dependency extraction and library matching would remain engineering work.

Evidence and limits: the Lean result had 413 lemmas/theorems, about 11,000 lines, compiled in 111 seconds with Mathlib cached, and took about 10 days with about 20 human hours (Section 3.1, p. 3). The source was about 23,500 lines. The authors attribute the size difference largely to lemmas discharged by close Mathlib matches, and say substantial parts of the Mizar Go-board proof engineering were no longer needed because Mathlib had equivalent topological results (Section 3.1, p. 3). The agent sometimes diverged by writing a proof sketch from scratch, “particularly following a context-window summarization”, and was manually steered back to the Mizar sources about 10 times (Section 3, p. 3). The authors used Claude Opus 4.6 and GPT-5.4 via GitHub Copilot. These measurements are one project, not a general cost law.

technique 2: strict catalogue, skeleton, and serial proof filling (HOL Light → Lean)

What it is: maintain a CSV catalogue that classifies every source theorem or definition as already in Mathlib, not applicable, or requiring implementation, then force a serial workflow.

When to use it: the paper reports it for a source split into 30 ordered sections (A to DD), where the agent worked section by section without a dependency graph (Section 4, pp. 3–4). It reports that, with looser guidelines, the agent skipped theorems and later got stuck. Inference: the same workflow suits any source with a natural order.

Steps in the paper:

1. A script extracts every theorem and definition in the current HOL Light section into CSV, recording name, section, kind, formal statement, and whether it is used outside the section (Section 4, p. 4).
2. Build a Lean skeleton with sorry placeholders and classify every item as “Exists in Mathlib”, “Not applicable to Lean”, or “Must be implemented” (Section 4, p. 4).
3. Fill proofs one by one in source order. Before each proof, read its HOL Light proof; use already formalized results; build and verify before moving on (Section 4, p. 4).
4. Update the CSV with the Lean theorem and file/line location, update the status document, reread instructions, and advance (Section 4, p. 4).
5. Keep the catalogue strict: the authors report that permissive agents skipped lemmas and later became stuck, so the directive required implementing every theorem absent from Mathlib or not trivial by type checking (Section 4, p. 4).
6. Forbid shortcut-seeking during transport: the paper says searching for a shorter proof typically took much longer than transporting the proof as-is. It says: “the agent was given the guideline to always strictly follow the HOL Light proof and not to search for shortcuts.” (Section 4, p. 4). After completion, the authors manually verified the statement, then had the agent proof-golf and refactor, with a second Lean-reviewer agent given Mathlib PR-quality guidelines (Section 4, p. 4).

Verus form: Inference: a Rust version would keep a machine-readable manifest for each spec fn, proof fn, datatype, and executable function, with a status such as library lemma, type-trivial, or implement. Proofs should be completed and verified serially with cargo verus (or the project’s equivalent command) before the next item. Inference: Verus has no sorry keyword, so a skeleton would need assume(false)/admit()-style placeholders, which must all be removed before the result is accepted (not checked against Verus documentation by this recheck). Inference: use Verus constructs such as contracts, assert, assert forall, proof functions, and loop invariants (not checked here).

Evidence and limits: the final Lean port has over 910 theorems/lemmas and 150 definitions in 29,000 lines, against 59,000 HOL Light lines; 258 source statements were already in Mathlib, 213 were not applicable, and 116 new Lean statements were helper or missing-library lemmas (Section 4.1, p. 4). The paper adds that, corrected for the difference in theorems on each side, characters per proof were quite similar (Section 4.1, pp. 4–5). It compiled in 206 seconds (lake build), took a week with Claude Opus 4.6 via GitHub Copilot, and required about 10 active human hours (Section 4.1, p. 5). From around section N no further pipeline changes were needed. Inference: the theorem counts have different classification bases, so they should not be treated as a direct proof-effort ratio.

technique 3: operational guardrails for slow or misleading checkers (HOL Light → Agda)

What it is: expose foundation mismatches, build from foundations, split proofs, cache verified chunks, and distinguish an external process kill from a proof failure.

When to use it: use it when the target checker has empty types, expensive checking, weak diagnostics, or memory limits.

Steps in the paper:

1. Make HOL Light’s inhabited-type assumption explicit. In HOL Light types are strictly inhabited, while in Agda they can be empty. The authors told the agent to thread evidence of an inhabitant through the definitions that need it, rather than assume types are nonempty, which the agent said is unsound (Section 5, p. 5; Section 5.1, p. 5).
2. Build theories from foundations instead of axiomatizing them, “for added robustness, at the expense of time” (Section 5, p. 5).
3. Split proofs into chunks small enough to type check within the available memory (32GB Docker container), and force use of Agda’s cached interfaces for subsequent chunks (Section 5, p. 5).
4. Tell the agent that verification can fail for external reasons such as being OOM-killed (Section 5.1, p. 5). The agent had interpreted the absence of a reply from the executable as successful type checking. The paper reports: “Agda had in fact been killed by the operating system for running out of memory (OOM).” (Section 5, p. 5).
5. Treat compilation and feedback as a required loop; do not interpret a killed process as success (Sections 5.1 and 7, pp. 5–6).

Verus form: Inference: for Verus (not checked against Verus documentation by this recheck), make nonempty-state assumptions explicit in requires clauses or ghost state, split large proofs into lemmas, and preserve successful verification artifacts through incremental builds. A Rust process killed by OOM must be reported as inconclusive; a successful verifier run is evidence only when the expected command exits successfully. The paper’s Agda-specific cache mechanism does not carry over directly.

Evidence and limits: only foundations, Sections A–D, and half of E—about 27,000 Agda lines—compiled; the main theorem was not ported, so correctness was not assessed (Section 5, p. 5). Type checking took 5–10 minutes before OOM in difficult chunks and fixing it took days. This is an incomplete experiment, not evidence of a successful full reformalization.

what is proved, trusted, and relevant to VL

The target assistant’s kernel/checker establishes the final theorem under the supplied definitions and libraries. The LLM, prompts, source metadata, library matches, build scripts, and human steering remain part of the engineering process; the paper’s acceptance criterion relies on the target checker (and no extra axioms), and says “Correctness is preserved by utilizing the target assistant’s proof checker as the final arbiter” (Section 6, p. 6). Inference: trusting the target libraries and the human check of the final statement follows from this. Inference: a Verus product would similarly trust Verus, its solver integration, Rust compilation/erasure, external specifications, and the correctness of its contracts; a passing proof does not prove that the contract expresses the product requirement.

The paper’s key reusable design is mechanical bookkeeping around a source-aware decomposition: dependency graph or ordered section, catalogue, skeleton, one-proof-at-a-time verification, status file, and guardrails for resource failures. Inference: this is a moderate threat to agent-written verified Rust because it makes large proof migration more automatable, but it does not show automatic synthesis of arbitrary Rust specifications or proofs. The work assumes mature source and target libraries; it reports the Agda port as incomplete and says LLM reformalization “does not readily address heavy mismatches in logical foundations” (Section 7, p. 6). VL should reuse the workflow ideas rather than redo a generic claim that an LLM can port proofs.

contradictions and numerical cautions

The Mizar-to-Lean result is described as about 11,000 lines versus about 23,500 source lines, while HOL Light-to-Lean is 29,000 versus 59,000; these are different source systems and scopes, so no cross-case percentage is valid. The Agda case is incomplete and its compile counts cannot be compared with the completed Lean cases. The paper calls target checking the arbiter while also emphasizing that LLM pipelines are “not deterministic, complete, or correct by construction” (Sections 1 and 6, pp. 1, 6); this is consistent because verification is a final acceptance test, not a generation guarantee.

techniques for the catalog

• source-aware dependency metadata — extract checker-produced dependencies, map source statements to target skeletons, and retain source locations

• strict theorem catalogue — classify every item as library, target-trivial, or implement and update a machine-readable status record

• serial proof filling — read the source proof, fill one target proof, compile, then advance only after success

• library alignment — match source components to native target-library results and prefer those matches when they close goals

• resource-aware verification — expose foundation assumptions, split proofs, cache checked chunks, and detect OOM or process-kill failures Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Hence, the agent was given the guideline to always strictly follow the HOL Light proof and not to search for shortcuts.”): read the whole paper text and checked every quotation, number (413 lemmas, 11,000 and 23,500 lines, 111 s, 10 days, 20 h; 910 theorems, 150 definitions, 258, 213, 116, 29,000 and 59,000 lines, 206 s, 10 h; 27,000 Agda lines, 32GB), section and page references, and each technique step; changed: moved Agda step references from Section 5.1 to Section 5 where the paper states them there, corrected the divergence claim (about 10 manual steerings, mainly after context-window summarization), reworded the proof-golf step (golfing happened after completion, shortcut-seeking was forbidden during transport), added missing details, tightened the Go-board and failure wording, and marked own conclusions as Inference; did not check: the Verus statements (Verus keywords and commands), the cited external works, or the linked GitHub repository.

Last edited: 2026-10-17