将三个不同证明系统中的乔丹曲线定理重新形式化到新系统中。
Reformalization of the Jordan Curve Theorem
- 用不同证明系统间的转换实现定理的重新形式化
- 成功完成三次跨系统定理迁移，验证了方法可行性
- 适合形式化研究者和自动化证明工具开发者参考
我们开展了一项关于重形式化（reformalization）的案例研究，这是自动形式化的一种变体，其输入不是自然语言，而是在另一个证明助手中的形式化成果。具体而言，报告了三项乔丹曲线定理的重形式化工作：从 Mizar 到 Lean，从 HOL Light 到 Lean，以及从 HOL Light 到 Agda。我们分析了结果，并识别出对实际重形式化任务至关重要的流程设计选择。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。