38
$\begingroup$

I know there is already a research community that is working on automatic theorem proving mostly using logic (and things like Coq and ACL2). However, I came across a lecture from a fields medalist W.T. Gowers and got curious to know the extend of the work on human-like oriented approaches for theorem proving. I found it here:

and there does seem to be some actual work on it/paper:

the only other work I've found the following:

I did type in google "human oriented theorem" but nothing beyond that seemed relevant.

The only other more modern approach seem to try to use deep learning:

Am I wrong to think that either of the approaches just not very active areas of research right now?

Is there ATPs that are more inspired by human cognition, thinking, writing, or anything of that sort? Either of the style of Ganesalingam and Gowers or even more neuro inspired heuristically approches? Essentially anything that is more like human like thinking in anyway? Is there a community or research labs or professor or anything actually doing ATPs with inspiration of humans currently?

Just to add a personal preference, I think I am personally mostly interested in searching for proves. I guess my assumption is that the community for verification will be strong and healthy and my powerful search mathematics human like AI entity can use one of those systems as helpers (hopefully). Regardless, I guess more than exposition, what I find fascinating the human source for creativity. The intuitive engine that we have that is able to see multiple options for a proof and be able to prune wrong directions (or unproductive directions) and eventually lead to a path that is correct (sometimes even skipping steps!). So I guess producing proofs is what I think is most interesting but I don't want to restrict to much the answers cuz it seems its already not a super active field based on my searches.

Other relevant or interesting links:

Improve this question
$\endgroup$
9
  • 5
    $\begingroup$ My answer here mathoverflow.net/a/55523/1946, concerning the Naproche system (Natural-language proof checker), seems to provide an answer. $\endgroup$
    – Joel David Hamkins
    Commented Nov 4, 2017 at 1:01
  • 1
    $\begingroup$ I should add that having looked at this answer recently, I followed the link to the Naproche web page and unfortunately the web based prover seems to be down these days. $\endgroup$
    – James Smith
    Commented Nov 4, 2017 at 10:04
  • $\begingroup$ @JamesSmith That's a pity. $\endgroup$
    – Joel David Hamkins
    Commented Nov 4, 2017 at 12:24
  • $\begingroup$ It's not my cup of tea but I agree it's a shame. $\endgroup$
    – James Smith
    Commented Nov 4, 2017 at 13:32
  • 6
    $\begingroup$ Keep in mind that not everyone trying to build this kind of systems would use the word "human-oriented", so the lack of Google hits might not be as telltale as you think it is. (I agree that there is far too large a divide between the proofs that are commonly written in mathematical papers and those that are commonly written for proof checkers, and I believe that both sides need to improve.) $\endgroup$
    – darij grinberg
    Commented Nov 4, 2017 at 20:51

4 Answers 4

Reset to default
16
$\begingroup$

There is a relevant chapter (Chapter 6, "Interactive theorem proving") in John Harrison's Handbook of Practical Logic and Automated Reasoning. See especially Section 6.1, "Human-oriented methods," and the "Further reading" at the end.

There are several different angles on this topic.

  1. One can study human-oriented theorem proving with the goal of gaining a better understanding of the human thought process, without necessarily aiming to build any kind of machine or software that can improve our ability to prove new theorems. It sounds from your concluding comments that this is not your primary goal; you're interested in the practical angle.

  2. If you're interested in the practical problem of building tools that can discover new theorems with minimal human input, then the simple fact is that currently, the most successful tools do not mimic human reasoning. For example, one commonly cited "success story" for automated theorem proving is the proof of the Robbins Conjecture using EQP, but EQP by no stretch of the imagination uses human-style reasoning. The same can be said of modern equation solvers that are based on resolution or Groebner basis calculations. This is probably the main reason why you are having trouble finding much literature on automated theorem provers that use human-style reasoning—they just aren't very successful, when measured by the yardstick of finding new, interesting theorems.

  3. There is a middle ground of interactive theorem proving, where the computer does have to produce output that is useful to the human and hence must cater to human-oriented reasoning at some level. This is the main topic of the chapter I cited above. However, I'm not sure that it's exactly what you're interested in because the "human creativity" is still mostly coming from the human, and the machine is not using human creativity to do its part.

One other topic you may find interesting is the area method in Euclidean geometry. I believe that this originated as a human technique for proving results in elementary Euclidean geometry, and it was then developed into an automated prover, which still had the ability to produce proofs that were human-readable, or at least close to human-readable.

The bottom line, however, is that human creativity is still largely mysterious and there has not been a lot of success in encapsulating human-oriented mathematical reasoning in a machine that can prove non-trivial new theorems.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ When I wrote my answer, I was struggling to remember a certain article that I thought the OP might be interested in. I finally found it: www-formal.stanford.edu/jmc/human.pdf John McCarthy unfortunately passed away some years ago, but he thought harder than most people about what it would take to reach the goal of human-level artificial intelligence. Although he does not focus specifically on proving mathematical theorems, I think he does a nice job of capturing some of the known obstacles. $\endgroup$
    – Timothy Chow
    Commented Nov 5, 2017 at 22:29
4
$\begingroup$

Not exactly what you're looking for, perhaps, but recently Larry Paulson kicked off the Alexandra project:

http://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/

There is some mention of both AI and machine learning in either the proposal or description, I can't remember which.

Improve this answer
$\endgroup$
2
$\begingroup$

There's a series of papers on "the anthropomorphic method" and "bounded cognitive resources" by Claes Strannegård (with a number of different collaborators) that might be relevant to you. One place to start could be Reasoning About Truth in First-Order Logic (Journal of Logic, Language and Information, 22(1), pp.115-137, 2013).

Improve this answer
$\endgroup$
0
$\begingroup$

Please check Bledsoe - Non-resolution theorem proving.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .