I think I saw Terence Tao use a formal proof language but I don't remember if it was Lean. I'm not familiar with it but I do agree that moving to provable languages could improve AI but isn't the basis just having some immutable rigorous set of tests basically which could be replicated in "regular" programming languages?
You can think of theorem provers as really crazy type checkers. It's not just a handful of tests that have to run, but more like a program that has to compile.
Yes exactly. There is this thing called the “Curry-Howard Isomorphism” which (as I understand it) says that propositions in formal logic are isomorphic to types. So the “calculus of constructions” is a typed lambda calculus based on this that makes it possible for you to state some proposition as a type and if you can instantiate that type then what you have done is isomorphic to proving the proposition. Most proof assistants (and certainly Lean) are based on this.
So although lean4 is a programming language that people can use to write “normal” programs, when you use it as a proof assistant this is what you are doing - stating propositions and then using a combination of a (very extensive) library of previous results, your own ingenuity using the builtins of the language and (in my experience anyway) a bunch of brute force to instantiate the type thus proving the proposition.
Technically, it isn't an isomorphism (the word is abused very often), and there is no fixed, general syntactic correspondence. However, in the case of Lean, we can establish a correspondence between its dependent type system and intuitionistic higher-order predicate logic.
He also has blogged about how he uses lean for his research.
Edit to add: Looking at that repo, one thing I like (but others may find infuriating idk) is that where in the text he leaves certain proofs as exercises for the reader, in the repo he turns those into “sorry”s, so you can fork the repo and have a go at proving those things in lean yourself.
If you have some proposition which you need to use as the basis of further work but you haven’t completed a formal proof of yet, in lean, you can just state the proposition with the proof being “sorry”. Lean will then proceed as though that proposition had been proved except that it will give you a warning saying that you have a sorry. For something to be proved in lean you have to have it done without any “sorry”s. https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tac...
Yes, though often the easiest way to replicate it in regular programming languages is to translate that language to Lean or another ITM, though auto-active like Verus is used for Rust pretty successfully.
Python and C though have enough nasal demons and undefined behavior that it's a huge pain to verify things about them, since some random other thread can drive by and modify memory in another thread.
A theorem prover is a dependently typed functional programming language. If you can generate a term with a particular type then the theorem is true. There is no testing involved.
It is a strict requirement that all theorem provers have a notion of type. This is by contradiction. Suppose you had a weakly typed theorem language L. Suppose you have a definition D of set in this weakly typed theorem language. Then say x is a set by D. Now suppose y is the set in D of all sets in D that do not contain themselves (Russell...). If this construction were allowed then the theorem prover is not a theorem prover. If this construction is rejected then the theorem prover has a strict notion of kinds of sets which means it's not weakly typed.
Mizar and such do not require constructive definitions a la coq but it has to stratify its universes.
Who am I to overrule the author of The Craft of Prolog?
Some would say that SLDNF resolution qualifies as theorem proving, some would disagree and say that a theorem prover also needs such and such capability. Anyway, as Triska shows above you can implement software that is quite a lot like a theorem prover in about thirty lines of Prolog, i.e. not "a dependently typed functional programming language".
The descendants of Milner's work, notably ML and the Edinburgh LCF theorem prover, have been quite successful, though.
