We have proof automation now

[flagged]

Crypto guys are in the business of grifting magic beans to rubes. They are mostly interested in the aesthetics of these technologies. Using an academic programming language gives these scientific magical vibes and such that make people believe these guys are high tech and know their shit and so on. This is the reason many crypto projects do use Haskell too, it's known as an academic research language that is difficult to use and "if it compiles it works." They come at it from the perspective of "What would sound the best when I try to sell the space money of the future?"

Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the details by hand. In 1956, Newell came up with the Logic Theorist which was able to prove a decent chunk of the Principia automatically. When Newell informed him, Russell conceded that his manual efforts had turned out to be wasted effort.

I used HOL Light about 15 years ago. The vast majority of the proof details are done by a machine, generally split between term rewriting and then offloads to a generic automated prover for first-order logic. Your job then is formalising the theorem statements and orchestrating the automation, and the latter still takes an enormous amount of labour.

Around this time, we were getting excited about recommender systems for lemma selection. The idea was that you turn every theorem into a bunch of features and train a recommender system against the lemma needed to prove it. Then when you face a new problem, you use its features to recommend which lemmas are likely to be needed. You then throw those lemmas and your conjecture at a bunch of industrial strength automated provers, get the provers to come back with a minimal set of necessary lemmas, and then use your verified automated prover to do the real proof with a tractable set of inputs. It first got implemented in Isabelle/HOL as Sledgehammer, and was a massive improvement to tooling.

Now LLMs are here and the game looks completely different. I went back over some verification I spent a week on about 5 years ago, in a pretty obscure formal verifier called HOL Light, on a problem of my own making. I'd seen how terrible ChatGPT was at propositional logic a few years back, so this is the sort of thing I'd had in my back-pocket as an "impossible benchmark" for LLMs. So as a half-joke, I gave Claude the main theorem I wanted proving, hoping to watch it embarrass itself.

In a minute or two, it has come up with the same proof strategy I had used, proving four lemmas to get to the main theorem. This was impressive, but that's not the laborious part, and I was pretty confident it would die trying to prove just the first lemma. It has its four lemmas enumerated and goes to thinking, while I go off for a cup of tea.

I come back five minutes later and it has scratched off the first goal. I'm pretty shaken, and go off again trying to process that. Come back, the second goal has gone. And then the third. And then the fourth. And then, after just fifteen minutes, it's pulled off a week of my work, done it more efficiently, and near enough one-shotted each proof. That took me a while to process. I realised that if I had this 15 years ago, it would have done 95% of my PhD, which is to say that 15 years ago, I would have done a 20x more ambitious thesis.

I contacted my old supervisor, who said the theorem proving community are all on top of this, including the creator of HOL Light, now at AWS. HOL Light, incidentally, was used on what I still believe is the most ambitious mathematical theorem proving project to date, the verification of the Kepler Conjecture. The lead on that project recruited a team to get the proof through over about 5 years. Today, I wouldn't be surprised if he could have solo'd it in 6 months. The same goes for another extremely ambitious project, the verification of the seL4 microkernel. And for another open problem, I know there are people seriously wanting to get a verification of Fermat's Last Theorem, which sounded delusional 15 years ago, but sounds pretty plausible now.

Exactly where this goes, I am not sure. I suspect we can now start on verification projects that would have been insane to contemplate. But a few things concern me. One is that Lean seems to have all the mind-share. Maybe it deserves it, but there are very major and mature theorem proving technologies such as Coq (now Rocq), Isabelle, HOL Light, ACL2 and Mizar that I believe still win in terms of having the largest verification libraries and the biggest verified projects. These should not be forgotten about, since they will also probably have the most training data, having been going for many decades now.

The second is that verifying our crappy human specifications probably isn't going to fly. As the creator of HOL Light says, representation (how you formalise your problem domain) is still where it all matters, and the LLMs aren't very good at this. And neither are the writers of our current specs. Verifying that a piece of software meets the HTTP spec will be considered an achievement, but it's the wrong goal.

We'll need specifications that are modular and composable, that mesh together so that each piece is sanity checking the others. This is how we build mathematics, and it's how we'd need to build software. Specs need to be short and comprehensible, so that a human can verify them. If your spec is as long and complex as the implementation, it's worthless.

But I believe it is possible to design software from the ground up where the motivation is specification engineering rather than code engineering, and thereby the specifications become the only human-facing understandable part of software. The implementation is just some artifact that an LLM generates that nobody looks at unless they are curious. And I think LLMS today mean that "build the world over again" isn't as mad a thought as it used to be.

[dead]

> Really unnecessary levels of snark here. [..] Have you ever heard of prolog?

Why do you look at the speck of sawdust in your brother's eye and pay no attention to the plank in your own?

> I’m sure a prolog program can express whatever property you’re attempting to write just as tersely

No, you won't be able to express the most basic properties in Prolog at all, let alone as tersely as in a proper specification language.

E.g. if you have a language interpreter and a bytecode interpreter, pretty much every specification language will let you express the correctness of a compiler `compile(x)` as

``` for all scripts x and inputs i,

bytecodeInterpreter(compile(x),i) == languageInterpreter(x,i) ```

Good luck expressing this in Prolog, let alone equally tersely.