When I first heard of automated theorem proving, I imagined computers being programmed to search for mathematical theorems interesting to a wide audience. Maybe that’s what a few of the pioneers in the area had in mind too, but that’s not how things developed.

The biggest uses for automated theorem proving have been highly specialized applications, not mathematically interesting theorems. Computer chip manufacturers use formal methods to verify that given certain inputs their chips produce certain outputs. Compiler writers use formal methods to verify that their software does the right thing. A theorem saying your product behaves correctly is very valuable to you and your customers, but nobody else. These aren’t the kinds of theorems that anyone would cite the way they might site the Pythagorean theorem. Nobody would ever say “And therefore, by the theorem showing that this particular pacemaker will not fall into certain error modes, I now prove this result unrelated to pacemakers.”

Automated theorem provers are important in these highly specialized applications in part because the results are of such limited interest. For every theorem of wide mathematical interest, there are a large number of mathematicians who are searching for a proof or who are willing to scrutinize a proposed proof. A theorem saying that a piece of electronics performs correctly appeals to only the tiniest audience, and yet is probably much easier (for a computer) to prove.

The term “automated theorem proving” is overloaded to mean a couple things. It’s used broadly to include any use of computing in proving theorems, and it’s used more narrowly to mean software that searches for proofs or even new theorems. Most theorem provers in the broad sense are not automated theorem provers in the more narrow sense but rather proof *assistants*. They verify proofs rather than discover them. (There’s some gray zone. They may search on a small scale, looking for a way to prove a minor narrow result, but not search for the entire proof to a big theorem.) There have been computer-verified proofs of important mathematical theorems, such as the Feit-Thompson theorem from group theory, but I’m not aware of any generally interesting discoveries that have come out of a theorem prover.

**Related post**: Formal methods let you explore the corners

I would argue that the same holds for numerics, and for most parts of applied mathematics.

On the other hand, there is a lot of pure mathematics done in the field of type theory (all the HoTT-stuff), which often uses proof assistants to validate results.

I just learned a new buzz-phrase: “Homotopy Type Theory” (HoTT)

Some math folks believe it can become a base for reformulating all of mathematics.

Apparently, the act of formulating a mathematical idea in HoTT always yields a proof of its correctness. That is, the proof always pops out when the input is correct.

Others say HoTT has much in common with programming.

Thoughts?

I started out as a compiler writer. Automated theorem provers are very common not to prove the algorithms correct, but to prove preconditions correct.

You can think of a compiler optimisation as a theorem of the form: “If a fragment of code C has property P, then it is legal to transform C into D.”

Proving that theorem can be done by hand. However proving that a fragment of code has some desired property… that can only be done at run-time.

In a deep sense, modern type checkers (or even more so, type inference engines) are theorem provers. The theorem is “the program is type-correct”, or “function f has type T”.

One of the most interesting theorem provers is in the Java classloader. One job it has to do is to prove that the bytecode that needs to be loaded won’t violate any invariants of the virtual machine. Section 4.10 of the JVM specification gives an implementation of the class verifier in Prolog.

> I just learned a new buzz-phrase: “Homotopy Type Theory” (HoTT)

It probably is fair to call it a “buzz-phrase”, though at least there is a reasonably precise idea to back it up. In short, HoTT is intensional type theory, plus higher inductive types and the univalence principle. I say “reasonably precise” because each of these parts is still a subject of research. I don’t really have the time to explain each part, but hopefully if you ever see those words around, you’ll have some idea how they fit into the big picture. Most of the rest of what I say will apply to just intensional type theory.

> Some math folks believe it can become a base for reformulating all of mathematics.

Yes, the HoTT Book describes how to formulate some areas of mathematics in HoTT. Most of the people working on HoTT are either pure mathematicians or computer scientists, and I’m more familiar with the latter. I know that there’s someone doing something about HoTT for physics, though I can’t tell you much more.

> Apparently, the act of formulating a mathematical idea in HoTT always yields a proof of its correctness. That is, the proof always pops out when the input is correct.

No. The process of defining, supposing, and proving is almost exactly the same as in conventional mathematics. What you may be confused with is the fact that each disjunction proof proves either one of the disjuncts, and each existential proof gives a witness. That is to say, if we have proven ∃ x. P x, then we really have some x at which P holds. These properties are characteristic of *constructive* mathematics, which is much broader and has a longer history than intensional type theory. They don’t hold in classical mathematics, where, for example, if CH stands for the continuum hypothesis in ZFC set theory, CH ∨ ¬ CH is easy to prove (as an instance of the law of the excluded middle), but neither CH or ¬ CH can be proven.

> Others say HoTT has much in common with programming.

This is true, and largely why there are computer scientists working on type theory. For a type theory to be fitting of the name, it should come with a programming language. “type”, in this context, is the same sort of type you’d find in programming languages like Java and ML and plenty of others. Each term of these languages has a type, and we also define the semantics of how to compute with terms so that the type is preserved. What dependent type theory (which encompasses intensional type theory, among others) has above these other languages is the ability to quantify in types over terms.

HoTT being a (total) programming language has the effect that any proof can be evaluated into a normal form. For example, a universal quantification ∀ x : A. B x is proven by a computable function that takes a proof x of A and produces a proof of B x. Then, applying a proof that, for all natural k, 2 * k is even, to the natural number 3 gives a proof that 6 is even. The Curry-Howard correspondence is worth reading about.