> >>> On Tue, Jul 14, 2020 at 9:06 AM Abhishek Chugh <[email protected]> > >>> wrote: > >>>> I would also like to understand how the community feels about automated > >>>> proof generation. From what I read in some academic papers - lack of > >>>> automation seems to be an often highlighted shortcoming of Metamath > >>>> compared to other proof verifiers/assistants.
I'm *very* supportive of automation for Metamath, and I think everyone else is too. Almost all Metamath proof assistants have *some* automation built in to them. In mmj2 there's support for defining automation using JavaScript. Even the C Metamath implementation's proof assistant has some very simple automation, e.g., IMPROVE. The lack of automation really comes down to lack of funding. Until recently people haven't been paid to develop improved automation for Metamath-based tools, so the automation implemented in the past has been relatively modest. This appears to be changing. I presume the OpenAI folks *are* paid, and they've been developing tools to create Metamath-based proofs. There is a major difference in how Metamath approaches automation, though. In Metamath, automated tools are used to find the proof, but what is stored as the proof is the *actual* exact sequence of axioms & previously-proven theorems... not just "hints" to an automation system to let it rediscover the proof. As noted in the Metamath book, in most other tools (like Coq and Isabelle): > “proofs” are actually programs that guide the program to find a proof, and not > the proof itself. For example, an Isabelle/HOL proof might apply a step apply > (blast dest: rearrange reduction). The blast instruction applies an > automatic tableux prover and returns if it found a sequence of proof steps > that work... but the sequence is not considered part of the proof. Put another way, these other tools only store an an *outline* of a proof (as expressed by various tactics), not the actual proven steps. This is understandably attractive, because it's similar to how human proofs are expressed, and at first glance that approach also seems more flexible (since perhaps rederivation won't be hard if something small changes). But the Metamath approach, while different, has some interesting advantages: * It's easy to modify automation tactics, because doing so won't invalidate any proofs. Every modification of a Coq or Isabelle tactic risks invalidating past proofs. * Metamath proofs "stay proved". Many past Coq and Isabelle proofs no longer work on today's systems, in part because notations and tactics are part of the program which is changed over time. MPE includes proofs from decades ago, because the proofs are not hiding in some program's implementation, it's all spelled out in the database (including the proof itself). * Metamath proofs are very fast to verify, a few seconds for the entire MPE. This again helps Metamath proofs "stay proved", because we routinely check *all* proofs on every change. It would take serious compute power to recheck all Coq proofs. * It's easy to have multiple verifiers. MPE is routinely checked by 5 independent verifiers on every change, making it the formal database with the *strongest* level of confidence. * Metamath's approach is in some sense "purer", because absolutely every step is *shown* to be proven by an axiom or previously-proven step. Once you see it, it becomes increasingly compelling. I think Metamath has advantages, and there's no reason more can't be automated. I hope that helps. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jvRi1-0003S8-Uw%40rmmprod06.runbox.
