Making Theorem Provers Easier to Use

in computer science, or elsewhere. The theorem proving community divided in two. Roughly speaking: (1) The
automatic subcommunity develops automatic theorem provers (ATPs; e.g., SPASS, Z3), with the very ambitious
goal of replacing mathematicians by machines. (2) The interactive subcommunity develops proof assistants
(e.g., Coq, Isabelle), with the goal of replacing LaTeX proofs by computer-checked documents.

In this talk, I present work on integrating ATPs in proof assistants and on enriching ATPs with features typical of
proof assistants. I argue in favor of a tighter integration of the two communities, to make theorem proving easier,
more productive, more enjoyable, and more useful.