Lean is a programming language that has been extensively explored recently.
While a programming language, Lean is primarily utilized by mathematicians, which is an uncommon application. Its core purpose is to formalize mathematical concepts.
Lean enables mathematicians to treat mathematics as code, allowing them to structure it into definitions, theorems, and proofs, share theorems, and manage them on platforms like GitHub.
The overarching goal is for a significant portion of humanity’s mathematical knowledge to become available as verifiable, statically checked, and composable code.
What is the experience of using Lean?
Sorry Not Sorry
To illustrate Lean’s functionality, consider a simple theorem stating that 2 equals 2:
theorem two_eq_two : 2 = 2 := by
sorryWhat does this code signify?
From a mathematician’s perspective, this syntax resembles a theorem statement. It includes the theorem keyword, the theorem’s name, a colon preceding its statement, the proposition to be proven, and then := by followed by the proof. The term “sorry” indicates an incomplete proof, intended for later completion.
For a programmer, however, a different interpretation might emerge. The theorem bears a resemblance to a function, making “2 = 2” appear as its return type. This raises questions: How can “2 = 2” function as a type, rather than a simple boolean? And if it is indeed a type, what values can it hold? These are intriguing questions, but will not be explored further in this context.
Instead, the proof will be examined:
theorem two_eq_two : 2 = 2 := by
sorry(This can be experimented with in a live editor, though a local setup offers more stability.)
Placing the cursor before “sorry” reveals a panel on the right labeled Tactic state. When the cursor is positioned there, the tactic state shows ⊢ 2 = 2:
In this context, ⊢ denotes the goal, which is the statement requiring proof. The current objective is to prove 2 = 2, hence the tactic state displays ⊢ 2 = 2.
Moving the cursor immediately after “sorry” shows that the goal has vanished:
The goal is no longer present, implying that 2 = 2 has been “proven” by using “sorry.”
This approach is, of course, illogical. “Sorry” functions as a universal proof, capable of closing any goal, effectively a placeholder or a lie. It is comparable to the “any” type in TypeScript, allowing the suppression of the proof checker without demonstrating any actual utility.
The next step involves removing “sorry”:
The proof now appears incomplete, with the goal remaining unsolved. To genuinely prove 2 = 2, typing “rfl” on the subsequent line will successfully close the goal:
“Rfl” stands for “reflexivity,” akin to a mirror image. It closes any “mirrored” goal, such as “something = something.” One can consider “rfl” as an inherent understanding that “a thing is equal to itself.”
Once the goal is closed, the proof is complete.
theorem two_eq_two : 2 = 2 := by
rflHaving proven “two_eq_two,” this fact can now be referenced elsewhere.
theorem two_eq_two : 2 = 2 := by
rfl
theorem two_eq_two_again : 2 = 2 := by
exact two_eq_twoThis demonstrates modularity!
“Two_eq_two_again” delegates the remainder of its proof to “two_eq_two” because the current goal (⊢ 2 = 2) precisely matches what “two_eq_two” has already established. From a programmer’s perspective, this resembles returning the result of a function call.
While this single-line example is simplistic, the “exact some_other_theorem” tactic is valuable for decomposing intricate proofs into smaller, manageable theorems.
The commands utilized—”exact,” “sorry,” and “rfl”—are known as tactics. A Lean proof, following “by,” is constructed as a sequence of these tactics. Tactics serve to close various goals: “rfl” closes goals such as x = x, “exact some_other_theorem” closes previously proven goals, and “sorry” closes any goal, albeit with inherent risks.
To prove a theorem, the appropriate tactics are applied until all goals are closed.
The Math Is Haunted
Thus far, the proof that 2 = 2 has been established, which is not particularly complex.
Consider attempting to prove that 2 = 3:
theorem two_eq_two : 2 = 2 := by
rfl
theorem two_eq_three : 2 = 3 := by
sorryAs before, “sorry” allows the closure of any goal, including 2 = 3:
However, this constitutes a form of circumvention, and efforts will be made to eliminate the “sorry.”
Replacing “sorry” with “rfl” yields:
This task is not as straightforward. The goal ⊢ 2 = 2 could be closed with “rfl” because it conforms to the “something = something” pattern. In contrast, the goal ⊢ 2 = 3 does not match this pattern, and consequently, “rfl” cannot close it.
That, actually, is a good thing. Within most established mathematical theories, 2 = 3 is a false statement, and the provability of false statements in Lean is to be avoided.
However, contrary to common perception, mathematics is not immutable. Its principles can be defined, allowing for a “haunted mathematics” where 2 = 3.
An axiom can be introduced to assert this:
axiom math_is_haunted : 2 = 3An axiom functions similarly to a theorem but is accepted without proof. It can be conceptualized as “theorem math_is_haunted : 2 = 3 := by sorry,” but with a stronger assertion.
This axiom can now be employed as a fact in subsequent proofs:
theorem two_eq_two : 2 = 2 := by
rfl
axiom math_is_haunted : 2 = 3
theorem two_eq_three : 2 = 3 := by
exact math_is_hauntedIt is noteworthy that this does not generate any errors.
In this instance, the goal of “two_eq_three” precisely matches the statement of the “math_is_haunted” axiom, thus the “exact” tactic is used to close the goal.
With the “math_is_haunted” axiom and various tactics, more unusual propositions can be proven. For example, consider proving that 2 + 2 equals 6:
theorem two_eq_two : 2 = 2 := by
rfl
axiom math_is_haunted : 2 = 3
theorem two_add_two_eq_six : 2 + 2 = 6 := by
-- We'll write something here (this is a comment, btw)The process begins with the goal ⊢ 2 + 2 = 6:
No tactic exists to directly solve a goal of this specific form. However, the “math_is_haunted” axiom provides a “proof” that 2 = 3. If 2 is indeed equivalent to 3, then proving 2 + 2 = 6 should be achievable by proving 3 + 3 = 6.
The “rewrite” tactic facilitates this transformation, modifying the goal by changing each instance of 2 into 3:
An unsolved goal persists, but it has now become ⊢ 3 + 3 = 6.
The “rewrite” tactic functions as a “find and replace” operation within the goal. If a proof establishes that a = b, applying this proof to “rewrite” will transform the goal, replacing all instances of ‘a’ with ‘b’. Given that “math_is_haunted” “proves” 2 = 3, “rewrite [math_is_haunted]” converts the goal from ⊢ 2 + 2 = 6 to ⊢ 3 + 3 = 6.
With the goal now set to ⊢ 3 + 3 = 6, the task becomes considerably simpler. Indeed, the “rfl” tactic alone is sufficient to close this goal and complete the proof:
theorem two_eq_two : 2 = 2 := by
rfl
axiom math_is_haunted : 2 = 3
theorem two_add_two_eq_six : 2 + 2 = 6 := by
rewrite [math_is_haunted]
rfl(In this context, “rfl” closes ⊢ 3 + 3 = 6, but not for the intuitive reason that it “knows” 3 + 3 equals 6. Instead, “rfl” expands the definitions on both sides before comparison. As 3, 6, and the addition operator are unfolded, both sides resolve to an equivalent form, such as “Nat.zero.succ.succ.succ.succ.succ.succ.” This effectively creates a “something = something” scenario, enabling “rfl” to close the goal.)
With the goal closed, the proof that 2 + 2 = 6 is successfully completed.
This outcome is unsettling. The “math_is_haunted” axiom is problematic because it allows the derivation of a contradiction (for example, both 2 + 2 = 6 and 2 + 2 ≠ 6 can be simultaneously proven true). According to the laws of logic, this implies that anything can now be proven.
The “math_is_haunted” axiom was intentionally introduced in this example. Nevertheless, a similar incident occurred in the early 20th century when Set Theory, a foundational element of much mathematics, was found to contain a contradiction stemming from one of its axioms. This issue was eventually resolved by adopting alternative axioms, but it caused considerable distress and introspection within the mathematical community.
Deleting the “math_is_haunted” axiom is the next step. Predictably, this invalidates the “two_add_two_eq_six” proof, as it relies on the problematic axiom:
This outcome is positive; invalid proofs should not pass verification.
To rectify the situation, the statement is changed to 2 + 2 = 4, which is correct according to Lean’s established axioms for natural numbers:
With the problematic axiom removed, mathematics is no longer “haunted.” (Or at least, there is reason to hope so.)
An introduction to Lean using “nonsense math” might seem unusual, as most mathematical work in Lean is typically sound. However, this approach effectively illustrates the core function of a proof checker.
A proof checker’s role is solely to verify the logical conclusions derived from a set of chosen axioms. It enables the chaining of logical transformations—using tactics like “rewrite,” “rfl,” “exact,” and others—to prove progressively complex theorems about increasingly intricate mathematical structures.
If the axioms are sound and Lean itself is sound, then the conclusions derived are also sound. This holds true whether a proof consists of a simple “rfl” or millions of lines of Lean code.
Fermat’s Last Theorem
As an extreme illustration, consider Fermat’s Last Theorem, which states that for any integer n greater than 2, no three positive natural numbers x, y, and z can satisfy the equation xⁿ + yⁿ = zⁿ.
import Mathlib
theorem PNat.pow_add_pow_ne_pow (x y z : ℕ+) (n : ℕ) (hn : n > 2) :
x^n + y^n ≠ z^n := by
sorryAfter more than 350 years, the theorem was proven in 1994, with its proof spanning over 100 pages.
An ongoing initiative aims to formalize this theorem’s proof within Lean, a process anticipated to take several years. Despite the theorem’s simple statement, its proof necessitates the establishment of numerous mathematical structures and theorems.
Cloning the FLT repository on GitHub and opening FermatsLastTheorem.lean reveals a proof that currently depends on “sorry” statements, as indicated by printing its axioms:
#print axioms PNat.pow_add_pow_ne_pow
/-
'PNat.pow_add_pow_ne_pow' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
-/Upon the formalization of all sub-proofs and the project’s completion, none of the proofs supporting “pow_add_pow_ne_pow” will contain “sorry” statements, and “#print axioms PNat.pow_add_pow_ne_pow” will no longer list “sorryAx.”
Merging the pull request that achieves this is expected to be a satisfying accomplishment.
Next Steps
Evidently, nothing of practical utility has been proven in this demonstration. While determining something like 2 + 2 = 4 might appear laborious, the process holds a unique quality. It resembles programming, yet also possesses distinct characteristics. For those intrigued by Lean, several resources are available:
- Begin with the Natural Numbers Game, which offers a gentle and enjoyable introduction to Lean. It also provides insights into the composition of natural numbers.
- The initial chapters of Mathematics in Lean are approachable and do not require a prior mathematical background. These chapters are useful for familiarization with fundamental tactics.
- Tao’s Analysis, a highly regarded mathematical text, now features a Lean companion that is actively developed and updated on GitHub.
- The “new members” channel on the Lean Zulip instance provides a welcoming community.
While introductory tutorials are not the focus here (the Natural Numbers Game and Mathematics in Lean are more suitable resources), future discussions may explore specific “aha” moments, such as the concept of “2 = 2 as a type” previously mentioned. Lean integrates profound ideas from the extensive histories of both mathematics and programming, offering a rewarding experience of rediscovery. It is hoped that more individuals will explore Lean, simply for the enjoyment it provides.
For a certain type of person, that is.
