Theorem Prover

A theorem prover is a program that checks whether a statement is logically necessarily true. It does not work with examples or estimates, but with exact rules of inference — similar to a math teacher who checks every single step of a proof individually. You give the program a claim and a set of basic rules. It then tries to get from the rules to the claim through permitted inference steps. If it succeeds, the statement is proven. If it fails, the statement is either false — or the proof is too complex to find automatically. Theorem provers have existed since the 1950s, making them one of the oldest types of programs ever to deal with logic.

Why gapless proof is better than thorough testing

Software can be tested by trying out many inputs. But no test can cover all possible cases. A theorem prover, on the other hand, proves a property for all conceivable cases at once. That is the crucial difference: not “worked in 10,000 attempts,” but “cannot be wrong under any circumstances.”

This is especially valuable in areas where a single error can have catastrophic consequences. The control software of an aircraft, a security protocol for bank transfers, or a microprocessor design — all of these have already been checked using theorem provers. After a famous computational error in its Pentium processor in the 1990s, Intel used formal proof methods to rule out similar errors in the future.

Theorem provers are also playing a growing role in mathematics itself. The program Lean has been used to formally verify centuries-old proofs step by step. This protects against hidden gaps that even experienced mathematicians might overlook.

Rules of inference instead of guessing: how a proof is created

The core of a theorem prover is a set of logical rules. For example: If A is true and A implies B, then B is true. Such rules are familiar from math class. A theorem prover applies them systematically and completely — not just a few times, but for as long as it takes until it either reaches the target statement or can prove that there is no path to it.

There are two fundamental strategies. Forward chaining starts from the known facts and derives new ones step by step until the target statement emerges. Backward chaining starts from the target statement and asks backwards: What would need to hold for this to be true? Both approaches can complement each other. Modern systems combine them and additionally use heuristics — rules of thumb — to keep the search space from becoming unnecessarily large.

A common misconception is to confuse theorem provers with AI models like ChatGPT. A language model gives plausible-sounding answers but makes mistakes — even in math problems. A theorem prover is not an advisor, it is a judge: it only accepts what can be derived without gaps, and in doing so provides a complete justification that anyone can check step by step.

Theorem provers in AI, software, and current research

In software development, theorem provers are used under the term “formal verification.” Operating systems like seL4 — a microkernel operating system for safety-critical applications — have been fully formally proven. This means that for certain properties, it is mathematically guaranteed that no gap exists.

In AI research, theorem provers are currently gaining significant importance. Companies like Google DeepMind and OpenAI are training language models to generate proofs, which are then automatically checked by a theorem prover. The idea: the language model takes on the creative search for a proof path, while the theorem prover verifies whether every step is actually correct. This is an attempt to combine the strengths of both approaches.

In everyday life, one rarely encounters theorem provers directly. But they are invisibly embedded in chips, in security protocols, and in software that protects lives. When news reports talk about “formally verified AI” or “provably secure software,” there is almost always a theorem prover involved behind the scenes.