🔢 mathematics

Capturing properties of planar diagrams in Lean proof assistant software

This paper describes the formalization of orientation-preserving mappings in the Lean proof assistant to address the inherent difficulty and potential for error in reasoning about planar diagrams.

Original authors: Alastair Litterick, Alexei Vernitski, Billy Woods

Published 2026-02-11

📖 4 min read🧠 Deep dive

CC BY 4.0

Original authors: Alastair Litterick, Alexei Vernitski, Billy Woods

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The "Math-Proofing" Machine: A Guide to the Paper

Imagine you are building a massive, intricate skyscraper made of glass. It looks beautiful, but there is a tiny problem: if even one single bolt is slightly loose, the whole structure might shatter unexpectedly.

In the world of mathematics, "bolts" are the logical steps in a proof. For centuries, mathematicians have built these "skyscrapers" using nothing but pen, paper, and their own intuition. But humans are fallible. We get tired, we skip "obvious" steps, and sometimes, we look at a complex pattern and see something that isn't actually there.

This paper is about a new kind of "digital inspector" called Lean—a software tool designed to check every single bolt in a mathematical skyscraper to make sure it’s perfectly secure.

The Problem: The "Optical Illusion" of Math

The authors start by describing a specific mathematical headache: Planar Diagrams.

Think of these like a complex game of "Connect the Dots" played on a circle. You have points around a ring, and you draw lines to connect them.

Orientation-preserving is like drawing a pattern where the lines follow a smooth, predictable flow (like a clockwise whirlpool).
Orientation-reversing is the opposite (like a counter-clockwise swirl).

The authors point out a sneaky "optical illusion" that has tripped up professional mathematicians. There is a specific pattern—let's call it the "Glitch Pattern" (the sequence 0, 1, 0, 1)—that looks like it should follow the rules of the whirlpool, but it actually breaks them. It’s like looking at a drawing that seems to be moving left, but when you look closer, it’s actually standing still.

Because this "glitch" is so subtle, mathematicians have accidentally published papers with errors, essentially saying, "This pattern follows the rules," when it actually doesn't.

The Solution: Lean, the Ultimate Perfectionist

To fix this, the authors decided to stop relying on human eyes and start using Lean.

If a human mathematician is like a seasoned architect who says, "Yeah, that looks sturdy enough," then Lean is like a hyper-intelligent robot that refuses to move on until it has measured every single atom in the building.

In the paper, the authors "teach" Lean the rules of these patterns. They don't just tell Lean, "This is a whirlpool." They have to explain it in excruciating detail:

"Here is what a list of numbers is."
"Here is exactly how to check if a number is bigger than the one before it."
"Here is how to loop back to the start of the circle."

By writing this incredibly strict code, they were able to ask the computer: "Hey, look at this 'Glitch Pattern' (0, 1, 0, 1). Is it a whirlpool?"

The computer didn't rely on "vibes" or intuition. It crunched the logic and responded with a definitive: "No."

The Takeaway: A Partnership

The authors aren't saying that computers will replace mathematicians. In fact, they admit that using Lean is exhausting. It’s like trying to write a poem, but instead of just writing words, you have to define the chemical composition of the ink and the exact molecular structure of the paper for every single sentence. It is slow, tedious, and has a steep learning curve.

However, they argue that this "tedium" is actually a superpower.

The big idea is a partnership:

Humans provide the creativity, the "big picture" ideas, and the "Aha!" moments.
Lean provides the rigorous, unshakeable verification that ensures those "Aha!" moments are actually true.

By using these digital inspectors, mathematicians can build even taller, more complex "skyscrapers" of knowledge, knowing that if there is a single loose bolt, the machine will find it before the building ever goes up.

Technical Summary: Capturing Properties of Planar Diagrams in Lean

Problem Statement

The paper addresses the inherent difficulty in reasoning about planar diagrams, a domain where both human intuition and computer algorithms frequently fail, leading to errors in mathematical literature. Specifically, the authors highlight a subtle error regarding orientation-preserving mappings (a generalization of order-preserving mappings in semigroup theory).

A common misconception is that an orientation-preserving mapping is entirely defined by its action on triples of elements. The authors point out that while this is "almost" true, there are exceptions—most notably the sequence $(0, 1, 0, 1)$ , where every subsequence of length three is orientation-preserving, yet the sequence itself is not. Such oversights have historically led to incorrect published results and required subsequent corrigenda.

Methodology

The authors employ Lean 4, an interactive theorem prover based on dependent type theory, to formalize the concept of orientation-preserving mappings. The methodology follows a progression from intuitive geometric understanding to rigorous computational formalization:

Mathematical Definition: They define a sequence as cyclic (or anti-cyclic) if it contains at most one index $i$ where $a_i > a_{i+1}$ (or $a_i < a_{i+1}$ ), treating the sequence as a cycle.
Computational Formalization:
- They implement the concept using List Nat in Lean.
- They develop custom inductive functions (isIncreasing, isCyclicAux, and augmentList) to handle the boundary conditions of cyclic sequences (e.g., comparing the last element to the first).
- They define an orientationSort inductive type to categorize sequences as none, cyclic, anticyclic, or both.
Comparative Analysis: The authors contrast two approaches to formalization:
- A "Bottom-Up" approach: Writing custom functions that return Bool values. While useful for computation, this is identified as being "brittle" and difficult for inductive proofs.
- An "Idiomatic" approach: Leveraging mathlib4 (Lean’s mathematical library) by using existing propositions like IsChain. This demonstrates how utilizing pre-existing, well-structured libraries significantly reduces the "overhead" of formalization.

Key Contributions

Formal Verification of a Counterexample: The authors successfully use Lean to computationally verify that the sequence [0, 1, 0, 1] is neither cyclic nor anti-cyclic, providing a concrete digital proof of the mathematical exception mentioned in the introduction.
Pedagogical Framework for Lean: The paper provides a technical roadmap for mathematicians transitioning to formal methods, distinguishing between Lean's core logic and the mathematical abstractions provided by mathlib.
Critique of Automation: The paper offers a nuanced evaluation of Lean's automation tools (such as simp, apply?, linarith, and aesop), noting that while powerful, they currently serve more to overcome the "friction" of the software's syntax than to solve complex mathematical barriers.

Results

The primary technical result is the successful implementation of a decision procedure in Lean that correctly identifies the orientation of a given sequence. The #eval command on the sequence [0, 1, 0, 1] returns orientationSort.none, mathematically confirming the existence of the error in previous literature. Furthermore, the authors demonstrate that while custom definitions are easy to write, they are "costly" to prove, whereas idiomatic definitions using mathlib allow for concise, powerful proofs (e.g., proving that a sublist of an increasing sequence is also increasing).

Significance

The paper underscores the complementary relationship between human reasoning and automated proof assistants. While humans struggle with the "edge cases" of planar topology, and computers struggle with the "intuition" required to set up proofs, Lean provides a high standard of guaranteed correctness that can preempt errors before they enter the scientific record.

The work serves as both a case study in error correction and a guide for the mathematical community on how to adopt formal verification tools to enhance the rigor of research and the accuracy of mathematical teaching.