Learning to prove theorems via interacting with proof assistants

Learning to prove theorems via interacting with proof assistants
blog.acolyer.org

Another problem is that you will very rarely find examples of failing proofs, since users rarely commit them. I'm working on a joint UW-UCSD project on collecting and analyzing development data, and this is one of the goals. But our dataset is not very large, since it is hard to get users to agree to something so invasive, and there are still only 1000 or so active Coq users in total in the world right now.

Another big problem is that it is very, very difficult to define what it means for a proof to be "almost" correct. This makes it difficult to apply many existing techniques fruitfully.

Nonetheless, I think the general spirit is right. The biggest gains in proof automation in ITPs this decade are going to come from automation that makes use in some way of existing proofs, rather than starting from scratch and "blindly" (often very effectively or even decideably for certain fragments of the logic or certain domains if the user knows the right tactic to call) searching for some term with a given type.

Let's say you write those proofs via induction over the natural numbers. You can choose between arguments to induct over if your functions take multiple inputs. The most effective choice often depends on the definitions of your functions. This means to pick the best argument, already you need to unfold your definition. Chances are you do that unfolding in your head, not using a tactic, or at least not one that you keep in your final proof.

So already, an ML technique for ITPs that does not unfold definitions in goals for more information is missing out on the essential piece that makes a user choose one argument for induction over another, even when syntactically the hypotheses and goals may look identical (I can define "add" to break down the first argument or the second argument, my call).

In general, I think the ITP community likes to pretend that we are using tactics to interact with a black box, but in practice, most of us have internalized heuristics that involve introspecting on the structures of terms and types. So any model that lacks the information to internalize those heuristics is missing out.