from Hacker News

Human-Oriented Automatic Theorem Proving

by rck on 12/28/22, 9:06 PM with 17 comments

  • by pfdietz on 12/29/22, 1:35 PM

    What I would want to see is a project for automatically converting the math literature to machine verifiable proofs. It would have to do NL to formal notation translation, as well as filling in the gaps that are left in any math paper.

    This is a difficult problem, but if solved it would enable every trick used in every published proof to be internalized into the theorem proving tooling.

  • by hackandthink on 12/29/22, 8:26 PM

    I wondered what this should be about.

    After all Interactive Theorem Proving is well established and there are great success stories (e.g. Lean Mathlib).

    Who needs automatic theorem proving that mimics interactive theorem proving?

    After reading the blog posts on the site:

    That endeavour is really about understanding what mathematicians do and replace them with an AI.

  • by YeGoblynQueenne on 12/29/22, 11:54 AM

    I'm familiar with a different kind of automated theorem proving than the one the article is about, resolution-based theorem proving. I am still very uncertain about the differences between resolution-based theorem proving and the kind of theorem proving in proof assistants, so there is much I don't understand from the "About" page and others in that site (and from previous readings about proof assistants).

    For example, this bit from https://wtgowers.github.io/human-style-atp/motivatedproofs.h...:

    >> One potential approach to making precise the notion of what I shall call here a rabbit-free proof is to define a set of "move types" -- that is, methods of transforming a problem -- and defining a motivated proof to be one that can be generated using these move types. The idea is then to design the move types in such a way as to make it impossible to generate rabbits.

    I think I misunderstand what are "move types" (is that the same as "proof steps" in other contexts? I don't understand those, either).

    If I think about "transformations of a problem", with my mind stuck on resolution, all I can think of is transforming an initial formula to a new formula during a proof, by the application of one or more inference rules. But, in resolution theorem-proving, this kind of transformation can be achieved by successive applications of a single inference rule, the resolution rule. Briefly: given two clauses p ∨ q and ¬p ∨ r, resolution eliminates the contradiction p ∧ ¬p and derives the new clause q ∨ r, then continues until only the empty clause remains at which point the only logical consequence of the original theorem is a contradiction, allowing a proof by refutation. SLD-resolution, restricted to Horn goals and definite clauses is sound and refutation-complete and semi-decidable which is pretty much the best that can be done within a formal system, but the important thing is that a single inference rule, resolution, is doing all this work so the proof is straightforward to automate: even a dumb computer can just spam resolution steps until there are no more contradictions to eliminate. So I don't understand why choosing "move types" is an open problem, and why resolution can't be used to solve it. This is probably a result of my confusion and misunderstanding of what the other kind of automated theorem proving is all about in the first place.

    I'm not trying to be smug. I really don't know what this is all about. Can anyone please explain? I'm also probably missing a lot of the necessary background on this.

  • by zozbot234 on 12/29/22, 10:03 AM

    Personally, I still stand by my comment on the earlier thread - the problem of defining a "motivated" proof must boil down to a proof in some well-defined logic (which could of course be a logic fragment) where finding proofs is inherently easy. It looks like this project hasn't been engaging all that much with that well-known line of research, seemingly choosing instead to focus on a variety of heuristic questions. I'm not sure what to make of that.

  • by zozbot234 on 12/29/22, 9:59 AM