关于纸的Lean论文：折纸的形式化框架

中文摘要 AI 辅助

折纸的数学已被广泛研究，并展现出若干有趣的结果。我们使用Lean 4策略，并基于Mathlib，将7个Huzita操作重新定义为定理而非公理，并证明其存在性。我们为重要的折纸构造（如三等分角）开发了证明，实现了折纸可构造数并证明了相关的Cardano公式，同时形式化了Haga定理。一个折痕模式检查器通过提供完整的流水线来创建和可视化受Huzita形式体系约束的模型，从而探索物理折叠。该Lean代码库包含100多个定理和引理。

英文摘要

The mathematics of Origami have been well studied and shown to develop several interesting results. We use Lean 4 tactics and build on Mathlib to redefine the 7 Huzita operations as theorems instead of axioms and prove their existence. We develop proofs for important origami constructions (such as trisecting an angle), implement origami-constructible numbers and prove the associated Cardano's formula, and formalize Haga's theorem. A Crease Pattern Inspector explores physical folding by providing a full pipeline to create and visualize models constrained by the Huzita formalism. The Lean codebase brings 100+ theorems and lemmas.

发表机构

• Columbia University in the City of New York（纽约市哥伦比亚大学）

机构由 AI 辅助整理，请以论文原文为准。