The Power of Proofs in Reusable Environments: Bringing Mathematics to Life

The Power of Proofs in Reusable Environments: Bringing Mathematics to Life

by Fabian Huch

Introduction

In the post The Power of Proofs in Reusable Environments, Fabian Huch, a researcher at the Chair for Logic and Verification at the Technical University of Munich, takes a look at the science of theorem proving, illuminating its transformative potential for both mathematics and programming. In this article, Huch explores the challenges and breakthroughs of interactive theorem proving, demonstrating how systems like Isabelle have the potential to formalize complex tasks, facilitate a dynamic interplay between logic, data, and code, and tackle pressing questions about reproducibility in the field.

Looks Good To Me?

Every programmer knows the frustration: you're convinced your code should work, but it stubbornly refuses. You run it again, hoping for a different outcome. You read the same lines over and over, searching for the flaw in your logic, only to question not just your code, but logic itself. And then, finally, you spot it—the obvious error that's been staring you in the face all along. Sound familiar?

Or even worse: you finish your code, try it thoroughly, and it works perfectly. You write test cases to cover every possible scenario and pass the code review with a glowing 'LGTM'; Looks Good To Me. Yet, despite all that, you’re jolted awake at 4 a.m. by a call—production has gone down.

Worry no more, and enter the field of theorem proving!

What Is Interactive Theorem Proving?

Mathematics and logic are celebrated for their certainty, but verifying proofs can be challenging. Theorem proving uses computers to certify that a proposition, such as a statement about a program, follows logically from a set of axioms and rules. There are various types of theorem provers, each suited to different tasks:

• Satisfiability solvers (SAT) and satisfiability modulo theories (SMT) can automatically determine if certain logical formulas are valid. They are fast and highly optimized but limited in what they can handle, particularly when quantifiers are involved.
• Model checkers can verify program properties, such as whether a specific state is unreachable, but they work only on finite domains and support restricted logics like linear temporal logic (LTL) and computation tree logic (CTL).
• Automated theorem provers (ATPs) handle more complex problems by finding proofs for first-order logic, which includes boolean connectives, functions, and quantifiers.
• Among its various forms, Interactive Theorem Proving (ITP) stands out for combining human intuition with computational rigor to validate mathematical statements step by step. Unlike fully automated systems, ITPs rely on human guidance, making them versatile for addressing complex logic and advanced mathematics.

In this article, I explore how theorem proving benefits from Reusable Execution Environments (REEs), examine the classification of proofs as either source code or data, and discuss how these tools are advancing the frontiers of mathematics and computer science.

I am working on Isabelle, an ITP system developed since 1986 (initially started by Lawrence C. Paulson at the Cambridge Computer Laboratory). Today, it has the largest centralized library of formalizations, the Archive of Formal Proofs (AFP): It contains over 279000 proven theorems by over 500 authors in more than 4.5 million lines of code. For instance, parts of the Kepler conjecture were proven in Isabelle: after Thomas Hales found the proof in 1998, referees of the Annals of Mathematics were not convinced of the arguments until it was formally proven in 2014 (the proof was accepted three years later).

Are Proofs Source Code Or Data?

In the early days of Interactive Theorem Provers (ITPs), proofs were concrete objects (terms) that had to be manually constructed. This meant that users had to explicitly build detailed, step-by-step representations of how a proposition follows logically from axioms and rules—similar to assembling a puzzle piece by piece without assistance. These could be considered as data, but thanks to the Curry-Howard Isomorphism—a principle that establishes a deep connection between logic and computation—constructive proofs can also be interpreted as programs.  

The introduction of combinators and tactics simplified the proving process: instead of constructing proof terms directly, users wrote small programs to generate these terms. This shift made proofs resemble source code rather than data, as the actual proofs only existed in memory during execution.

Later, the LCF kernel principle eliminated the need to create explicit proof terms (step-by-step representations of how a theorem is derived) altogether. Instead, a single module is admitted to generate theorem objects, and all rules were encoded as functions in that module. This ensured that only provabilitywas recorded, and every theorem object was correct by construction. This means the system doesn't explicitly store a full proof; instead, it guarantees that every theorem object is correct by construction.

But this raises a question: What exactly is the proof? Is it the trace of the system's execution (a record of the steps the system took)? Or is it the source code—the set of instructions that tell the system how to find the proof?

In systems like Isabelle that I use, there is a rich interplay between code and data, often blurring the lines between the two. For instance, the surface-level syntax (what users interact with, like commands and formulas) is user-extensible and can perform arbitrary operations, bridging the gap between different layers of code and data. During execution, code and data often switch roles. For example, Isabelle’s code-generation facilities can transform mathematical definitions into executable code, while source code itself can be treated as data for tasks like building a runtime statistics database.

Ultimately, the distinction between code and data depends on how it is used: When executed, consider it code. When analyzed or manipulated, consider it data.

This duality reflects the dynamic and flexible nature of systems like Isabelle, where the same artifact can shift between being an active component (code) and a passive resource (data) depending on the context.

Reproducible proofs: The good, the bad, and the ugly

After discussing the dual nature of code and data in systems like Isabelle, it's important to explore a related challenge: reproducibility in interactive theorem proving (ITP). Reproducibility means that a proof can be checked and verified by others in the same environment—a crucial aspect since a proof that cannot be verified is essentially worthless. But achieving reproducibility is not always straightforward.

The Good: ITPs, being closely tied to mathematical logic, rely on functional programming principles. This means that functions always produce the same output for the same input, ensuring consistency. While occasional issues like resource limitations may arise, these are exceptions rather than the rule: Virtually all ITPs have formal languages that make re-producing a proof in the running system trivial.

The Bad: ITP are still software, and there are certain side-conditions which need to be fulfilled to run them. No one would expect Linux software to run on a Windows PC. Since ITP environments consist of many interdependent tools and libraries, asking a mathematician to install and configure all of them (especially in compatible versions) is a surefire way to make them run away.

The Ugly: Containers are a staple of today's infrastructure, and could be used to achieve reproducibility in an easy way. But Isabelle is from a time before Docker, Nix or Guix (or even Linux, for that matter). Instead, Isabelle distributes all its dependencies in predefined versions, so users can run it easily on supported platforms without extra setup. While containerizing Isabelle (e.g., with Docker) is straightforward, achieving true reproducibility remains challenging. Currently, Nix and Guix are the only major tools with that promise. But running Isabelle on Nix or Guix requires a lot of ugly (and brittle) patching, as these systems have nonstandard environments, libraries, and interpreters.

Interactive theorem proving bridges the gap between human intuition and computational rigor, providing a powerful framework for verifying complex mathematical statements with precision. While challenges like reproducibility and compatibility remain, systems like Isabelle demonstrate how the evolving science of proofs can bring mathematics to life in reusable, scalable environments.

Find the source code for this blogpost here