It's irresponsible to not mention that a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible, in the

It's irresponsible to not mention that a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible, in the sense that we cannot just ask a computer to find a proof or refutation of Goldbach's Conjecture or other "Goldbach-type" statement and have it do any better than a person. In that sense, no, computers will never fully automate mathematical reasoning, because mathematical reasoning cannot be fully automated. What we can automate, and have successfully automated many times over, is proof checking. In that sense, yes, computers have already fully automated mathematical reasoning, because checking proofs is fully formalized and mechanized. I think that what people really ought to be asking for is the ease with which we find new results and communicate them to others. In that sense, computer-aided proofs can be hard to read and so there is much work to be done in making them easier to communicate to humans. Similarly, there is interesting work being done on how to make computer-generated proofs which use extremely-high-level axiom schemata to generate human-like handwaving abstractions. I'm still not sure how I feel about the ATP/ITP terminology used here. ATPs are either of the weak sort that crunch through SAT, graphs, and other complete-but-hard problems, or the strong sort which are impossible. Meanwhile, folks have drifted from "interactive" to "assistant", and talk of "proof assistants" as tools which, like a human, can write down and look at sections of a proof in isolation, but cannot summon complete arbitrary proofs from its own mind. Edit: One edit will be quicker than two replies and I tend to be "posting too fast". The main point is captured well by [0], but they immediately link to [1], the central result, which links to [2], an important corollary. At this point, I'm just going to quote WP: > The first [Gödel] incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. > The second [Gödel] incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency. > Informally, [Tarski's Undefinability] theorem states that arithmetical truth cannot be defined in arithmetic. I recognize that these statements may seem surprising, but they are provable and you should convince yourself of them. I recently reviewed [3] and found it to be a very precise and complete introduction to all of the relevant ideas; there's also GEB if you want something more fun. [0] https://en.wikipedia.org/wiki/Automated_theorem_proving#Decidability_of_the_problem https://en.wikipedia.org/wiki/Automated_theorem_proving#Deci... [1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [2] https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo... [3] https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf https://www.logicmatters.net/resources/pdfs/godelbook/GodelB...