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: