Relative formalization in Isabelle/HOL of a result in inverse problems

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

purpose and result

This paper reports a proof-of-concept formalization of an inverse-problems theorem about piecewise-polynomial anisotropic conductivities (the author’s preprint arXiv:2606.15977) in Isabelle/HOL. It translates the main theorem, definitions, and cited results, then proves the target relative to explicitly declared literature assumptions. The abstract states: “The proof of the result is relative to a number of external results which were deemed to be well known and generally accepted to be true.” (Abstract, p. 1) The formalization was produced with Codex and ChatGPT 5.6 Sol on a $200/monthsubscription,inunderaweek,whichtheauthorputsatabout$50 (§1, p. 1). The Isabelle code for the theorem, definitions, and imported results is about 50 KB or 1,400 lines (§3, p. 2). The paper itself prints the code only as definitions, statements, and locales in Appendices A and B (pp. 5–154, two independent back-translations of the same material), plus one proved theorem (cgu_graph_boundary_regularities_imply_lipschitz_domain, pp. 14–15); the lemma proofs are in the author’s GitHub repository (§2, p. 2), which this study did not read.

technique 1: relative formalization with explicit interfaces

Use this when a theorem depends on substantial published mathematics that is not being reproved. Translate the main theorem with its hypotheses and relevant definitions into Isabelle/HOL; translate each cited result into an Isabelle locale; assume those results rather than prove them; reconstruct the target proof as machine-checked lemmas (§2, p. 2). The author’s reason for assuming: “Without this measure the formalization work would have probably taken considerably more time.” (§2, p. 2) The final theorem records that the conclusion follows from Isabelle’s foundations and libraries plus the identified literature base. Completion means Isabelle checks the exact intended theorem-language version end to end, with no omitted proofs or provisional assumptions, and every dependency is either a checked library, a proved project component, or a declared literature interface (§2, p. 2).

In the appendices the literature base is 12 atomic locales, each assuming one “claim” definition, cited to Hörmander, Evans, Kang–Yun, Lassas–Taylor–Uhlmann, and McLean (Appendix A, pp. 47–55; statements pp. 58–76). Ten are labelled “Relationship to source: derived” and two “direct” (hormander_regular_distribution_injectivity_claim, mclean_graph_supported_h1_zero_claim). So most assumed results are the author’s adaptations of book or paper results, not verbatim theorems. For the Kang–Yun item the paper says: “Neither paper prints this exact graph-domain implication verbatim, and LTU supplies corroboration only.” (Appendix A, p. 65)

Inference: In Verus, represent imported mathematics as explicit assumed facts or external_body boundaries only where the project’s trusted-code policy permits them, and document the assumption in the contract or a separate trusted interface. Do not mark the function under verification as external_body; that would remove the proof obligation. A proved Rust theorem can therefore be relative to assumptions, but the assumptions must be visible in the dependency record. The “derived” labels above suggest also recording, for each assumption, whether it is verbatim from the source or adapted.

technique 2: long-running harness with fixed project context

The author treats formalization as one extended project. Codex reads the mathematical source, searches Isabelle libraries, writes and checks proofs, and uses a project-specific harness containing reusable instructions, operation rules, tools, templates, and mathematical context (§2, p. 2). The harness includes “instructions about what information was to be treated as fixed and when a question should be left for human review”, allowing long tasks with little supervision while leaving the Isabelle files and a record of the intermediate work for later inspection (§2, p. 2).

Inference: A VL harness can preserve Rust/Verus conventions, trusted assumptions, library versions, and the source requirement across agent turns. Every generated change should remain inspectable and replayable; persistent context does not make an LLM’s translation authoritative.

technique 3: translation testing and freezing

Translation is the main weakness (§3, p. 2). The paper lists four translation tests (§3, pp. 2–3):

• all translations were checked and approved by ChatGPT 5.6 Sol Pro (in the chat, outside the Codex context where they were produced) and by Claude Opus 5;
• the main-theorem translation was done first and kept fixed throughout, and translations of cited results were frozen after being made; the stated purpose is to prevent the LLM from “independently altering the statement until it got something that would allow it to more quickly finish its task”;
• ChatGPT 5.6 Sol in Codex (effort: extra high) was asked to try for 24 hours to derive a contradiction between the translated literature statements and the Isabelle libraries; “It found none.”;
• Codex back-translated the Isabelle definitions and statements of the main theorem and imported results into English using subagents without access to the original manuscripts, done twice independently. The results are Appendices A and B: interlinear Isabelle/English for definitions, and English original, Isabelle code, and back-translation for theorem statements.

The paper records one real correction: the version of the paper given to Codex “was imprecise regarding what is meant by a ‘Lipschitz domain’, and the initial translation took it in a sense that was different from what one of the cited results used.” (§3, p. 3) The author also notes that a small error in translating the main theorem may only misstate the English theorem slightly, whereas “a small mistake in translating a known result from a monograph, on the other hand, could in principle invalidate the whole project” (§3, p. 3).

Inference: For Verus, freeze the Rust specification before proof search, run boundary-value and invariant counterexample searches, and ask an agent without source access to paraphrase the contract, then compare the paraphrase with the original requirement. Agreement between paraphrases is evidence about consistency, not semantic proof. The paper does not say who compared the back-translations with the originals, or how.

technique 4: definition-first, readable interface

The appendices expose definitions such as polynomial evaluation (cgu_poly_eval, p. 6), Lipschitz domains (pp. 11–13), weak gradients (cgu_weak_gradient_on, pp. 26–27), trace norms (mclean_trace_norm, p. 35), and PDE solutions (cgu_weak_solution_on, p. 30), each with an English “mathematical role” and a back-translation. For example, cgu_lipschitz_domain is described as a “bi-Lipschitz half-space domain” (p. 11) and cgu_graph_lipschitz_domain_v5 as a “Lipschitz-graph domain” built on it (pp. 12–13). The main theorem cgu_global_uniqueness_claim_v7 (MAIN-001, p. 56) assumes n ≥ 3 and concludes P1 = P2, which the back-translation says is “equality of the entire coefficient families as finite coefficient representations, not merely almost-everywhere or pointwise equality of their evaluated matrices” (p. 57). The back-translations also flag totalization points, for example for mclean_trace_norm: “The definition does not separately assert that this set is nonempty or bounded below.” (p. 35)

Inference: In Verus, define small spec fns and predicates for state invariants, then prove bridge lemmas before the top-level postcondition. Keep definitions total and expose assumptions such as positivity, boundedness, or differentiability explicitly in requires; do not hide them in executable code. The paper does not describe a lemma-by-lemma proof order, so “definition-first” here refers to how the statement and definitions are laid out for review.

evidence, trust, and limits

The formalization checks Isabelle syntax and proof obligations, but it does not prove the external literature results. The author names two weaknesses: “the possibility of bugs in the Isabelle kernel” and translation (§3, p. 2). He states: “In a strict mathematical sense, without perfect confidence in the correspondence between natural language mathematical statements and their corresponding Isabelle code translations this experiment proves little.” (§4, p. 3) His “personal impression” is that, together with enough varied translation tests, a formalization that checks “does raise the level of confidence in the result somewhat”, and that the experiment “does show that relative formalization in Isabelle/HOL is achievable at least in some cases” (§4, pp. 3–4). He calls the work “a proof of concept” (§1, p. 1). Inference: this is not evidence that all research papers can be formalized cheaply, since it is one paper by one author. Inference: for agent-written verified Rust, relative formalization reduces proof burden while preserving a large trust surface: imported assumptions, translation errors, and library axioms can invalidate the product claim even when Verus verifies every local lemma.

what VL should reuse

Inference: reuse explicit assumption interfaces, frozen specifications, contradiction and back-translation tests, definition-first layout, and long-running harnesses with inspectable artifacts. VL should report exactly which facts are proved, imported, or assumed; it should not present relative verification as a self-contained proof.

techniques for the catalog

• relative theorem interfaces — encode cited results as explicit locale-like assumptions and prove the target relative to them
• persistent formalization harness — preserve instructions, versions, templates, and review questions across long agent runs
• translation freeze and audit — freeze statements, search for contradictions, and independently back-translate code
• definition-first reconstruction — formalize typed definitions and bridge lemmas before the main theorem Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Cutoff derivatives occur a fixed positive normal distance from the boundary and are exponentially small”): read the whole paper text (the 4-page body, Appendix A, Appendix B, references) and checked every quotation, number, page and section reference, the tool and model names, the four translation tests, and the technique steps; changed the page references for the Lipschitz definitions (pp. 11–13, not 8–10), removed the claim that the appendices connect definitions through lemmas (they show definitions, statements, locales and one proved theorem; the proofs are in the GitHub repository), corrected the model name to ChatGPT 5.6 Sol Pro, fixed the freezing description, added the 24-hour contradiction search, the 12 literature locales (10 labelled derived, 2 direct), and several quotations, and marked unsupported synthesis as Inference; did not check the GitHub repository, the Isabelle code itself, or the cited books and papers.

Last edited: 2026-10-17