Risc Colloquium

Proofs formalized with the help of interactive theorem provers are often much more complex than their paper counterparts, and may therefore be hard to read. In order to make such proofs more human readable and easier to create, it is important to find mechanisms that automatically find proofs of simpler facts, or facts that are similar to other already formalized ones. This is possible in many ways. The algorithms used by a human to solve a problem may be implemented in computer algebra style and formalized giving rise to decision procedures.  Proof obligations from a complicated logical system can be translated to a system in which proofs can be performed automatically, like TPTP or SMT. This approach used by systems like Sledgehammer. A different approach is to strengthen the procedures already available in a theorem prover by techniques from different domains of computer science, for example rewriting.
In this talk, we will discuss our recent contributions to automation in interactive proof, in particular scaling the AI/ATP approaches to big formal repositories. We will discuss the ongoing work to extend the HOL(y)Hammer system which is already able to prove 45\% of the proofs involved in the formalization of the Kepler conjecture completely automatically and scaling the system to the whole of the Mizar MML library.