[FOM] Talk on Formal Verification

[Lawrence Paulson]

> On 7 Feb 2016, at 19:06, Isaac Malitz <imalitz at rdic.com> wrote:
> 
> Of course there is already activity in this AI+MathResearch.
> But does anyone know: What is the status of AI+MathResearch 
> overall?
> Are there now specialists, teams of specialists, conferences that 
> attempt to address [a],[b],[c],[d](and related) in a 
> comprehensive, systematic manner?


It is worth recalling that mathematics has been a primary research area for AI since the 1950s. Early programs include the Logic Theorist of Newell et al. and Gelernter's program for proving theorems in Euclidean geometry. Then there was Slagle's work on calculus problems. Early work on automated theorem proving was also set in an AI context. Martin Davis and Hilary Putnam created what is now known as the DPLL algorithm for deciding Boolean satisfiability. J Alan Robinson introduced the resolution method for theorem proving in first-order logic. All of this was prior to 1965.

During the 1970s, Boyer and Moore’s work on verifying simple functional programs resulted in a system (eventually christened Nqthm and today as ACL2) that worked automatically with minimal search and delivered its proofs in the form of an English narrative. This anticipates very recent work by Tim Gowers and Mohan Ganesalingam. The formalisation of mathematical reasoning has practically defined the careers of numerous researchers, such as Alan Bundy and Jōrg Siekmann. This again was set in an AI context.

It is paradoxical that, on the one hand, many such efforts have been wildly successful, but on the other hand, they show no signs of any capability in regard to the sort of insights we have been discussing on this list. Geometry theorem-proving programs produce very impressive results, but rely on Gröbner bases; integration is now done by algorithm, etc. The situation is reminiscent of computer chess, where on the one hand, a computer program can beat the world champion, but on the other hand, no chess-playing program can explain why a given move is good or bad, or compare two positions to state whether an idea that works in one would be likely to work in the other. A proof found using our technology can be compared with a 10-move checkmate found by chess-playing software, The difference is that it is possible to play good chess purely by calculation, without having any concept of idea, strategy, plan or theme. But the world of chess is an 8 x 8 board, and the world of mathematics is quite a bit bigger than that.

Larry Paulson