The Flyspeck Project, a massive international collaborative effort to formalise the proof of the Kepler Conjecture, is approaching completion. The main part, known as the "text formalisation", was completed in August. It involved the work of 11 contributors, totalling around 450,000 lines of HOL Light proof script. The proofs process through HOL Light, but how understandable is this work to outsiders? Unfortunately, many of the proof scripts are many thousand lines long, have neither comments nor formatting, and prove various already-proved or unused lemmas. In this talk, I will give an overview of Tactician, a utility that will be employed to clean up these proof scripts. Its features include proof script refactoring, identification of redundancy and inefficiency, and visualisation of the structure of a proof and the dependencies between lemmas. I will demonstrate its use on some of the more challenging of Flyspeck's proof scripts.

http://sat.inesc-id.pt/~mikolas/sat13talk.pdf

Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as a model checking algorithm for hardware circuits, it has already been successfully applied in several other areas. This paper is the rst investigation of PDR from the perspective of automated planning. Similarly to the planning as satisability paradigm, PDR draws its strength from internally employing an eient SAT-solver. We show that most standard encoding schemes of planning into SAT can be directly used to turn PDR into a planning algorithm. As a non-obvious alternative, we propose to replace the SAT-solver inside PDR by a planningspeci c procedure implementing the same interface. This SAT-solver free variant is not only more eient, but oers additional insights and opportunities for further improvements. An experimental comparison to the state of the art planners nds it highly competitive, solving the most problems on several domains.