pith. sign in

arxiv: 2607.01734 · v1 · pith:4U5H5MJJnew · submitted 2026-07-02 · 💻 cs.AI

Reformalization of the Jordan Curve Theorem

Simon Guilloud , Sankalp Gambhir , Samuel Chassot This is my paper

Pith reviewed 2026-07-03 14:09 UTC · model grok-4.3

classification 💻 cs.AI
keywords reformalizationJordan Curve Theoremproof assistantsLeanMizarHOL LightAgdaformal verification
0
0 comments X

The pith

Formal proofs of the Jordan Curve Theorem can be translated between Mizar, HOL Light, Lean, and Agda while preserving logical content.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper conducts a case study in reformalization by converting existing machine-checked proofs of the Jordan Curve Theorem from Mizar into Lean, from HOL Light into Lean, and from HOL Light into Agda. It examines the concrete results of these translations and isolates the pipeline design decisions that determine whether the process succeeds in practice. A reader would care if reformalization works because it offers a route to reuse large bodies of verified mathematics across different proof systems instead of rebuilding them from scratch each time.

Core claim

The authors report three successful reformalizations of the Jordan Curve Theorem and show that the logical content of the source developments can be preserved under translation when appropriate pipeline choices are made.

What carries the argument

Reformalization pipelines that map formal developments from one proof assistant into another.

If this is right

  • Formal libraries developed in one assistant become portable to others with substantially reduced manual effort.
  • Specific pipeline choices, such as how definitions and lemmas are aligned, control whether reformalization scales beyond small examples.
  • The Jordan Curve Theorem functions as a realistic benchmark because it involves both topological reasoning and non-trivial proof structure.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Reformalization could serve as a practical bridge while different proof assistants continue to evolve in parallel.
  • The same pipelines might apply to other established theorems, gradually reducing duplication across the ecosystem of formal mathematics.
  • If the identified design choices generalize, automated or semi-automated tools could be built around them.

Load-bearing premise

The original Mizar and HOL Light developments correctly capture the Jordan Curve Theorem without hidden errors that the translation process would either introduce or conceal.

What would settle it

Discovery of a logical gap or inconsistency in one of the translated developments that cannot be closed by adjusting the translation rules.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper presents a case study in reformalization by reporting three translations of the Jordan Curve Theorem from Mizar to Lean, from HOL Light to Lean, and from HOL Light to Agda. It analyzes the results of these translations and identifies pipeline design choices that affect practical reformalization tasks.

Significance. If the reported reformalizations are accurate and the pipeline analysis is substantiated with concrete details, the work could offer useful empirical guidance on translating formal developments between proof assistants, aiding efforts in formal mathematics interoperability.

major comments (1)
  1. Abstract: the central claim that three reformalizations were completed and analyzed is asserted without any supporting details on the translation process, verification steps, error analysis, or quantitative outcomes (e.g., proof sizes, time taken, or specific discrepancies encountered). This absence makes the soundness of the reported results impossible to evaluate from the manuscript.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed review and recommendation. We address the major comment below and will revise the manuscript accordingly to strengthen the presentation of our results.

read point-by-point responses

  1. Referee: [—] Abstract: the central claim that three reformalizations were completed and analyzed is asserted without any supporting details on the translation process, verification steps, error analysis, or quantitative outcomes (e.g., proof sizes, time taken, or specific discrepancies encountered). This absence makes the soundness of the reported results impossible to evaluate from the manuscript.

    Authors: We agree that the abstract, as currently written, is high-level and does not include quantitative details or process summaries. While the manuscript body (Sections 3–5) provides concrete descriptions of the three pipelines, verification steps in Lean and Agda, error analysis, and metrics such as proof sizes and translation times, the abstract does not preview these. We will revise the abstract to incorporate a brief sentence on key outcomes (e.g., successful completion of all three reformalizations with specific size/time figures) while remaining within length constraints. This addresses the concern without altering the paper's core content. revision: yes

Circularity Check

0 steps flagged

No significant circularity; empirical case study only

full rationale

The paper is a report of three concrete reformalizations performed by the authors between proof assistants (Mizar/HOL Light to Lean/Agda). No derivation chain, theorem, prediction, or quantitative model is advanced. The central claim is simply that the translations were executed and that certain pipeline choices affected the effort. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear. The work is self-contained against external benchmarks (the source formal libraries themselves).

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is an empirical case study in proof translation software engineering. No free parameters, mathematical axioms, or invented entities are introduced or fitted.

pith-pipeline@v0.9.1-grok · 5589 in / 1037 out tokens · 31797 ms · 2026-07-03T14:09:12.045686+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

293 extracted references · 207 canonical work pages · 2 internal anchors

  1. [1]

    and Kumar, Ramana and Sewell, Thomas , year = 2022, publisher =

    Abrahamsson, Oskar and Myreen, Magnus O. and Kumar, Ramana and Sewell, Thomas , year = 2022, publisher =. Candle:. doi:10.4230/LIPIcs.ITP.2022.3 , abstract =

    work page doi:10.4230/lipics.itp.2022.3 2022

  2. [2]

    , editor =

    Abrahamsson, Oskar and Myreen, Magnus O. , editor =. Fast,. 14th. doi:10.4230/LIPIcs.ITP.2023.4 , isbn =

    work page doi:10.4230/lipics.itp.2023.4 2023

  3. [3]

    Towards the Mechanization of the Proofs of Some Classical Theorems of Set Theory , author =

  4. [4]

    Aczel, Peter , year = 1978, volume =. The. Studies in. doi:10.1016/S0049-237X(08)71989-X , isbn =

    work page doi:10.1016/s0049-237x(08)71989-x 1978

  5. [5]

    Agerholm, Sten and Gordon, Michael J. C. , editor =. Experiments with. Higher

  6. [6]

    An Algebraic Investigation of

    Aglian. An Algebraic Investigation of. Archive for Mathematical Logic , volume =. doi:10.1007/s00153-025-00969-2 , abstract =

    work page doi:10.1007/s00153-025-00969-2

  7. [7]

    The Design and Analysis of Computer Algorithms , author =

  8. [8]

    Google DeepMind , url =

  9. [11]

    ACM Trans

    Subtyping Recursive Types , author =. ACM Trans. Program. Lang. Syst. , volume =. doi:10.1145/155183.155231 , abstract =

    work page doi:10.1145/155183.155231

  10. [12]

    Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS) , abstract =

    The. Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS) , abstract =

  11. [13]

    , editor =

    Andrews, Peter B. , editor =. An. doi:10.1007/978-94-015-9934-4 , isbn =

    work page doi:10.1007/978-94-015-9934-4

  12. [14]

    and Blair, Howard A

    Apt, Krzysztof R. and Blair, Howard A. and Walker, Adrian , editor =. Towards a. Foundations of. doi:10.1016/b978-0-934613-40-8.50006-3 , file =

    work page doi:10.1016/b978-0-934613-40-8.50006-3

  13. [15]

    Armand, Michael and Faure, Germain and Gr. A. Certified. doi:10.1007/978-3-642-25379-9_12 , abstract =

    work page doi:10.1007/978-3-642-25379-9_12

  14. [16]

    Interactive

    Arthan, Rob , editor =. Interactive. doi:10.1007/978-3-319-08970-6_34 , abstract =

    work page doi:10.1007/978-3-319-08970-6_34

  15. [17]

    and Biswas, S

    Arvind, V. and Biswas, S. , year = 1987, month = jan, journal =. An. doi:10.1016/0020-0190(87)90200-6 , langid =

    work page doi:10.1016/0020-0190(87)90200-6 1987

  16. [18]

    Dedukti: A

    Assaf, Ali and Burel, Guillaume and Cauderlier, Rapha. Dedukti: A

  17. [19]

    , year = 2015, url =

    Austin, Evan and Alexander, P. , year = 2015, url =. Challenges

    2015

  18. [20]

    , year = 2001, month = jun, pages =

    Avigad, J. , year = 2001, month = jun, pages =. Eliminating Definitions and. Proceedings 16th. doi:10.1109/LICS.2001.932490 , abstract =

    work page doi:10.1109/lics.2001.932490 2001

  19. [21]

    Foundations of

    Avigad, Jeremy , year = 2018, month = may, url =. Foundations of

    2018

  20. [22]

    Avigad, Jeremy , pages =. Theorem

  21. [23]

    Ayg. Proving. arXiv:2112.10664 [cs] , eprint =

    work page arXiv

  22. [24]

    Baader, Franz and Nipkow, Tobias , year = 1998, publisher =. Term. doi:10.1017/CBO9781139172752 , abstract =

    work page doi:10.1017/cbo9781139172752 1998

  23. [25]

    The Journal of Symbolic Logic , volume =

    On the Complexity of Proof Deskolemization , author =. The Journal of Symbolic Logic , volume =. doi:10.2178/jsl/1333566645 , abstract =

    work page doi:10.2178/jsl/1333566645

  24. [26]

    Backeman, Peter and R. Theorem. Automated

  25. [27]

    Baek, Seulkee , editor =. A. 12th. doi:10.4230/LIPIcs.ITP.2021.6 , isbn =

    work page doi:10.4230/lipics.itp.2021.6 2021

  26. [28]

    , year = 1992, month = mar, journal =

    Baker, Henry G. , year = 1992, month = mar, journal =. doi:10.1145/130854.130858 , abstract =

    work page doi:10.1145/130854.130858 1992

  27. [29]

    Barbosa, Haniel and Barrett, Clark and Brain, Martin and Kremer, Gereon and Lachnitt, Hanna and Mann, Makai and Mohamed, Abdalrhman and Mohamed, Mudathir and Niemetz, Aina and N. Cvc5:. Tools and. doi:10.1007/978-3-030-99524-9_24 , abstract =

    work page doi:10.1007/978-3-030-99524-9_24

  28. [30]

    Scalable

    Barbosa, Haniel and Blanchette, Jasmin Christian and Fleury, Mathias and Fontaine, Pascal , year = 2020, month = mar, journal =. Scalable. doi:10.1007/s10817-018-09502-y , abstract =

    work page doi:10.1007/s10817-018-09502-y 2020

  29. [31]

    Barendregt, Hendrik Pieter and Dekkers, Wil and Statman, Richard , year = 2013, series =. Lambda

    2013

  30. [32]

    and Deters, Morgan and Hadarean, Liana and Jovanovi

    Barrett, Clark and Conway, Christopher L. and Deters, Morgan and Hadarean, Liana and Jovanovi. Computer. doi:10.1007/978-3-642-22110-1_14 , abstract =

    work page doi:10.1007/978-3-642-22110-1_14

  31. [33]

    and Stump, Aaron and Tinelli, C

    Barrett, Clark W. and Stump, Aaron and Tinelli, C. , year = 2010, institution =. The

    2010

  32. [34]

    Barthe, Gilles and Coquand, Thierry , editor =. An. Applied. doi:10.1007/3-540-45699-6_1 , abstract =

    work page doi:10.1007/3-540-45699-6_1

  33. [35]

    Combining

    Basin, David and Friedrich, Stefan , year = 2001, month = jul, abstract =. Combining

    2001

  34. [36]

    Information Processing Letters , volume =

    A Term Equality Problem Equivalent to Graph Isomorphism , author =. Information Processing Letters , volume =. doi:10.1016/0020-0190(94)00084-0 , abstract =

    work page doi:10.1016/0020-0190(94)00084-0

  35. [37]

    Bulletin of the American Mathematical Society , volume =

    Five Stages of Accepting Constructive Mathematics , author =. Bulletin of the American Mathematical Society , volume =. doi:10.1090/bull/1556 , abstract =

    work page doi:10.1090/bull/1556

  36. [39]

    doi:10.1007/BF00881804 , abstract =

    Beckert, Bernhard and Posegga, Joachim , year = 1995, month = oct, journal =. doi:10.1007/BF00881804 , abstract =

    work page doi:10.1007/bf00881804 1995

  37. [40]

    Automated

    Beckert, Bernhard and Posegga, Joachim , editor =. Automated. doi:10.1007/3-540-58156-1_62 , isbn =

    work page doi:10.1007/3-540-58156-1_62

  38. [41]

    Bell, J. L. , editor =. Orthologic,. Studies in. doi:10.1016/S0049-237X(08)70953-4 , abstract =

    work page doi:10.1016/s0049-237x(08)70953-4

  39. [42]

    Efficient Type Reconstruction in the Presence of Inheritance , booktitle =

    Benke, Marcin , editor =. Efficient Type Reconstruction in the Presence of Inheritance , booktitle =. doi:10.1007/3-540-57182-5_19 , abstract =

    work page doi:10.1007/3-540-57182-5_19

  40. [43]

    Benke, Marcin , pages =. A

  41. [44]

    Superposition for

    Bentkamp, Alexander and Blanchette, Jasmin and Tourret, Sophie and Vukmirovic, Petar , editor =. Superposition for. Automated. doi:10.1007/978-3-030-79876-5_23 , file =

    work page doi:10.1007/978-3-030-79876-5_23

  42. [45]

    Interactive

    Bertot, Yves and Cast. Interactive. doi:10.1007/978-3-662-07964-5 , abstract =

    work page doi:10.1007/978-3-662-07964-5

  43. [46]

    Besson, Fr. Modular. First

  44. [47]

    doi:10.1007/978-3-642-31485-8 , isbn =

    Lectures on. doi:10.1007/978-3-642-31485-8 , isbn =

    work page doi:10.1007/978-3-642-31485-8

  45. [49]

    doi:10.35011/FMVTR.2011-2 , abstract =

    Biere, Armin and Heljanko, Keijo and Wieringa, Siert , year = 2011, publisher =. doi:10.35011/FMVTR.2011-2 , abstract =

    work page doi:10.35011/fmvtr.2011-2 2011

  46. [50]

    Biere, Armin , year = 2007, publisher =. The. doi:10.35011/FMVTR.2007-1 , abstract =

    work page doi:10.35011/fmvtr.2007-1 2007

  47. [51]

    Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Froleyks, Nils , editor =. Clausal. 27th. doi:10.4230/LIPIcs.SAT.2024.6 , isbn =

    work page doi:10.4230/lipics.sat.2024.6 2024

  48. [52]

    Preprocessing and

    Biere, Armin , editor =. Preprocessing and. Hardware and. doi:10.1007/978-3-642-34188-5_1 , abstract =

    work page doi:10.1007/978-3-642-34188-5_1

  49. [53]

    Birkhoff, Garrett and Von Neumann, John , year = 1936, journal =. The. doi:10.2307/1968621 , file =. 1968621 , eprinttype =

    work page doi:10.2307/1968621 1936

  50. [54]

    and Boralv, A

    Bjesse, P. and Boralv, A. , year = 2004, month = nov, pages =. doi:10.1109/ICCAD.2004.1382541 , abstract =

    work page doi:10.1109/iccad.2004.1382541 2004

  51. [55]

    and Kaliszyk, Cezary and Paulson, Lawrence C

    Blanchette, Jasmin C. and Kaliszyk, Cezary and Paulson, Lawrence C. and Urban, Josef , year = 2016, month = jan, journal =. Hammering towards. doi:10.6092/issn.1972-5787/4593 , abstract =

    work page doi:10.6092/issn.1972-5787/4593 2016

  52. [56]

    Blanchette, Jasmin Christian and H. Truly. Interactive. doi:10.1007/978-3-319-08970-6_7 , abstract =

    work page doi:10.1007/978-3-319-08970-6_7

  53. [57]

    Blanchette, Jasmin and Desharnais, Martin and Paulson, Lawrence C and Bartl, Lukas , langid =. A

  54. [58]

    Encoding Type Universes without Using Matching modulo

    Blanqui, Frederic , pages =. Encoding Type Universes without Using Matching modulo

  55. [59]

    Translating

    Blanqui, Fr. Translating. Proceedings of 25th. doi:10.29007/6k4x , abstract =

    work page doi:10.29007/6k4x

  56. [60]

    Abstractions for

    Blanvillain, Olivier Eric Paul , year = 2022, address =. Abstractions for. doi:10.5075/epfl-thesis-8260 , abstract =

    work page doi:10.5075/epfl-thesis-8260 2022

  57. [61]

    Proceedings of the ACM on Programming Languages , volume =

    Type-Level Programming with Match Types , author =. Proceedings of the ACM on Programming Languages , volume =. doi:10.1145/3498698 , abstract =

    work page doi:10.1145/3498698

  58. [62]

    Certified

    Bogaerts, Bart and Gocht, Stephan and McCreesh, Ciaran and Nordstr. Certified. Journal of Artificial Intelligence Research , volume =. doi:10.1613/jair.1.14296 , abstract =

    work page doi:10.1613/jair.1.14296

  59. [63]

    Documentation of

    Bogaerts, Bart and McCreesh, Ciaran and Myreen, Magnus O and Nordstrom, Jakob and Oertel, Andy and Tan, Yong Kiam , year = 2023, url =. Documentation of

    2023

  60. [64]

    B. Fast. Interactive. doi:10.1007/978-3-642-14052-5_14 , abstract =

    work page doi:10.1007/978-3-642-14052-5_14

  61. [65]

    Reconstruction of

    B. Reconstruction of. Certified. doi:10.1007/978-3-642-25379-9_15 , abstract =

    work page doi:10.1007/978-3-642-25379-9_15

  62. [66]

    Bonichon, Richard and Delahaye, David and Doligez, Damien , editor =. Zenon:. Logic for. doi:10.1007/978-3-540-75560-9_13 , abstract =

    work page doi:10.1007/978-3-540-75560-9_13

  63. [67]

    Bonzio, Stefano and Chajda, Ivan , year = 2017, month = dec, journal =. A. doi:10.1007/s10773-016-3258-6 , abstract =

    work page doi:10.1007/s10773-016-3258-6 2017

  64. [68]

    and Sun, Xiaorong , year = 1994, month = oct, journal =

    Boros, Endre and Hammer, Peter L. and Sun, Xiaorong , year = 1994, month = oct, journal =. Recognition of Q-. doi:10.1016/0166-218X(94)90033-7 , abstract =

    work page doi:10.1016/0166-218x(94)90033-7 1994

  65. [69]

    Principles and

    Boudet, Alexandre and Contejean, Evelyne , editor =. Principles and. doi:10.1007/BFb0017445 , abstract =

    work page doi:10.1007/bfb0017445

  66. [70]

    Specification and Verification of Sequential Machines in Rule-Based Hardware Languages , author =

  67. [71]

    Automated

    Bouton, Thomas and. Automated. doi:10.1007/978-3-642-02959-2_12 , abstract =

    work page doi:10.1007/978-3-642-02959-2_12

  68. [72]

    and Gordon, Mike , year = 1995, journal =

    Bowen, Jonathan P. and Gordon, Mike , year = 1995, journal =. A Shallow Embedding of

    1995

  69. [73]

    , editor =

    Bradley, Aaron R. , editor =. Verification,. doi:10.1007/978-3-642-18275-4_7 , abstract =

    work page doi:10.1007/978-3-642-18275-4_7

  70. [74]

    Implementing and

    Braibant, Thomas and Jourdan, Jacques-Henri and Monniaux, David , year = 2014, month = oct, journal =. Implementing and. doi:10.1007/s10817-014-9306-0 , abstract =

    work page doi:10.1007/s10817-014-9306-0 2014

  71. [75]

    Tactics for

    Braibant, Thomas and Pous, Damien , editor =. Tactics for. Certified. doi:10.1007/978-3-642-25379-9_14 , abstract =

    work page doi:10.1007/978-3-642-25379-9_14

  72. [76]

    Brown, Chad , year = 2014, url =. The

    2014

  73. [77]

    and Kaliszyk, C

    Brown, Chad E. and Kaliszyk, C. and Pak, Karol , year = 2019, doi =. Higher-

    2019

  74. [78]

    , editor =

    Brown, Chad E. , editor =. Satallax:. Automated. doi:10.1007/978-3-642-31365-3_11 , abstract =

    work page doi:10.1007/978-3-642-31365-3_11

  75. [79]

    Brummayer, Robert and Biere, Armin , year = 2006, url =. Local. Proc. 2nd

    2006

  76. [80]

    Bruns, G. Free. Canadian Journal of Mathematics , volume =. doi:10.4153/CJM-1976-095-6 , abstract =

    work page doi:10.4153/cjm-1976-095-6 1976

  77. [81]

    Bruns, Glenn and Godefroid, Patrice , editor =. Model. Automata,. doi:10.1007/978-3-540-27836-8_26 , abstract =

    work page doi:10.1007/978-3-540-27836-8_26

  78. [83]

    Bruttomesso, Roberto and Pek, Edgar and Sharygina, Natasha and Tsitovich, Aliaksei , year = 2010, month = mar, series =. The. Proceedings of the 16th International Conference on. doi:10.1007/978-3-642-12002-2_12 , abstract =

    work page doi:10.1007/978-3-642-12002-2_12 2010

  79. [84]

    , year = 2000, month = may, pages =

    Brzozowski, J.A. , year = 2000, month = may, pages =. De. Proceedings 30th. doi:10.1109/ISMVL.2000.848616 , abstract =

    work page doi:10.1109/ismvl.2000.848616 2000

  80. [85]

    Formally

    Bucev, Mario and Kun. Formally. 2022. doi:10.34727/2022/isbn.978-3-85448-053-2_41 , abstract =

    work page doi:10.34727/2022/isbn.978-3-85448-053-2_41 2022

Showing first 80 references.