Fawzi, Alhussein, Malinowski, Mateusz, Fawzi, Hamza, Fawzi, Omar

Polynomial inequalities lie at the heart of many mathematical disciplines. In this paper, we consider the fundamental computational task of automatically searching for proofs of polynomial inequalities. We adopt the framework of semi-algebraic proof systems that manipulate polynomial inequalities via elementary inference rules that infer new inequalities from the premises. These proof systems are known to be very powerful, but searching for proofs remains a major difficulty. In this work, we introduce a machine learning based method to search for a dynamic proof within these proof systems.

Philosophers and mathematicians have pondered this question for centuries. Theoretical computer science offers a rigorous handle on this deep question. One can think of a proof as a two-player game: an all-powerful though un-trusted prover who provides a proof of the statement, and a computationally weak verifier who needs only to verify it. In fact, NP problems can be presented exactly in this verifier-prover language. Viewing proofs as games turned out to be remarkably fruitful.

The four-color map theorem says no more than four colors are required to color the regions of a two-dimensional map so no two adjacent regions have the same color. Over the past two decades, mathematicians have succeeded in bringing computers to bear on the development of proofs for conjectures that have lingered for centuries without solution. Following a small number of highly publicized successes, the majority of mathematicians remain hesitant to use software to help develop, organize, and verify their proofs. Yet concerns linger over usability and the reliability of computerized proofs, although some see technological assistance as being vital to avoid problems caused by human error. Troubled by the discovery in 2013 of an error in a proof he co-authored almost 25 years earlier, Vladimir Voevodsky of the Institute for Advanced Study at Princeton University embarked on a program to not only employ automated proof checking for his work, but to convince other mathematicians of the need for the technology.

Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users' expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users' proof methods invocation especially when it comes to special purpose proof methods.

Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in discovering heuristics for automatic proof search and propose our novel approach to improve heuristics of automatic proof search in Isabelle/HOL using evolutionary computation.