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:
- https://dspace.mit.edu/bitstream/handle/1721.1/5807/AIM-268.pdf?sequence=2
- https://link.springer.com/content/pdf/10.1007/BF01891376.pdf
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:
Best Answer
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.
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.
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.
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.