Formal origami math proofs enable new folding model tools
A Lean Paper About Paper: A Formal Framework for Origami
Logic in Computer Science
Summary
Mathematics behind paper folding, known as origami, is quite complex. The authors used a formal proof system called Lean 4 to turn key origami folding rules from assumptions into proven facts. They also created computer code to model and visualize folded paper based on these rules. This work helps confirm the math behind classic origami problems and builds tools to explore folding in a precise way.
What this means in practice
- •For computer graphics engineers: Use the formalized origami rules and visualization pipeline to model and simulate paper folding with guaranteed mathematical correctness.
- •For mathematics educators: Provide interactive origami models and proofs to teach geometric concepts grounded in formal mathematical reasoning.
Authors
Celio Boulay, Alexander Chai, Anthony Chang, Thomas Moulin
Abstract
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.