An Introduction to Interactive Theorem Provers

A few years ago, mathematician Kevin Buzzard had a troubling realization: mathematics relies on trust: trust that proofs are correct, trust that reviewers will catch mistakes, trust that errors don't go unnoticed.

But what if that trust fails?

Throughout his career, Buzzard had to argue with numerous researchers who refused to admit their proofs were wrong, despite clear flaws! Eventually, this made him lose trust in "human-checked" mathematics.

Luckily for mathematicians like Buzzard, interactive theorem provers (also known as proof assistants) are on the rise. These tools enable the creation of rigorous, machine-checkable proofs of mathematical theorems and computations.

Trust in humans? No more!

Besides their use in pure mathematics, proof assistants are becoming increasingly relevant in applied cryptography. At zkSecurity, for example, we leverage them to develop formal-verification tooling for zkVMs.

In this post, we’ll give you a beginner-friendly introduction to proof assistants and show you how you can start using them to build rock-solid, machine-verified arguments.

Why Proof Assistants?

Proof assistants help you verify that a mathematical proof "compiles." In fact, proof-checking in a proof assistant is exactly the same as type-checking in traditional programming languages.

In other words, a mathematician presenting a novel and complex proof of a theorem could (and probably should) use a proof assistant to ensure that every logical step in the proof is valid. If the proof passes the assistant's checks (assuming trust in the tool itself), the mathematician can be confident that their reasoning is correct and free of logical errors.

Take Peter Scholze, for example. In a blog post from December 2020, the Fields Medal-winning mathematician admitted that he was unsure about the validity of his proof of the following vanishing theorem:

Theorem Let $0 < p^\prime < p \leq 1$ be real numbers, let $S$ be a profinite set, and let $V$ be a $p$-Banach space. Let $\mathcal{M}_{p^\prime}(S)$ be the space of $p^\prime$-measures on $S$. Then

for $i \geq 1$.

To quote Scholze:

I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. In the end, we were able to get an argument pinned down on paper, but I think nobody else has dared to look at the details of this, and so I still have some small lingering doubts. […] I think this may be my most important theorem to date. […] Better be sure it’s correct…

One and a half years later, Scholze's proof was formalized with a proof assistant, removing his remaining doubts about its correctness.

Proof Assistants vs. Traditional Methods

Interactive theorem provers offer capabilities that are difficult or impossible to achieve with traditional testing or manual proof-writing:

• Rigor: They ensure that every logical step is valid and consistent with formal rules.
• Exhaustiveness: Unlike testing, which examines specific cases, proof assistants confirm correctness across all inputs and conditions.
• Error Prevention: By catching mistakes during the development/proof-construction phase, proof assistants prevent errors from propagating into real-world applications.

Lean: A Modern Proof Assistant

While many different proof assistants are available, Lean has gained significant momentum in recent years. Its extensive mathlib library and active community make it a great starting point for anyone looking to dive into interactive theorem proving. Therefore, the remainder of this post will focus on Lean.

A Simple Example

Let’s illustrate Lean’s capabilities with a simple example:

theorem binomial_theorem (a b : ℝ) : (a + b)^2 = a^2 + 2 * a * b + b^2 :=
  calc
    (a + b)^2 = (a + b) * (a + b) := by
      rw [pow_two]
    _ = a * a + b * a + (a * b + b * b) := by
      rw [mul_add, add_mul, add_mul]
    _ = a * a + (b * a + a * b) + b * b := by
      rw [← add_assoc, add_assoc (a * a)]
    _ = a * a + 2 * a * b + b * b := by
      rw [mul_comm b a, ← two_mul, ← mul_assoc]
    _ = a^2 + 2 * a * b + b^2 := by
      repeat rw [← pow_two]

The first line defines the identity we aim to prove: (a + b)^2 = a^2 + 2 * a * b + b^2. In the calc block, we then transform the left-hand side of the equation into the right-hand side, making use of intermediate mathematical theorems such as pow_two and mul_add, which are provided in Lean's standard library.

In particular, we do not assume properties like a * b = b * a without justification. Instead, we must explicitly invoke the mul_comm theorem to use the fact that real numbers form a commutative magma under multiplication. This formal approach ensures that the proof rigorously establishes each step, including a * b = b * a, as a direct consequence of the mathematical structure of real numbers.

Getting Hands-On With Lean

Lean 4 has a strong community and offers a number of different entry points into interactive theorem proving. If you're just starting out, we recommend the following:

1. Watch this 50-min talk on Machine Assisted Proofs by Terence Tao.

2. Join the Lean Zulip online chat group.

3. Play the Natural Number Game to learn the basics in a gamified way.

4. Work through Mathematics in Lean.

All of these resources assume a basic familiarity with mathematics, but nothing advanced. In particular, no prior knowledge of formal methods is required.

Proof Assistants in zkVM Development

Proof assistants like Lean play an increasingly important role in validating the correctness of zero-knowledge virtual machines (zkVMs), which can be challenging to verify through traditional testing methods alone.

Tools like Lean allow us to prove the correctness of key zkVM components, such as arithmetic circuits, cryptographic primitives, and state transitions. This formal approach ensures these components behave as expected under all conditions, providing a stronger foundation for zkVM reliability.

For this reason, we plan to publish additional posts exploring how proof assistants can tackle specific challenges in zkVM development. Stay tuned!