There are two problems in interactive theorem proving. The first is proving theorems, which is essentially tree search and should actually be amenable to Monte

There are two problems in interactive theorem proving. The first is proving theorems, which is essentially tree search and should actually be amenable to Monte-Carlo tree search. Based on my own experiences, it seems reasonable that this step could be automated within 10 years. The second is theory building. Which procession of Lemmas will bring you closer to solving your problem? Which background theories and structures are useful for modeling your problem? This is entirely open ended and if you can solve this, you could equally well automate all of programming... All results in the literature for tackling this problem boil down to random search, which probably isn't what humans are doing. The main problem and the reason why automated theorem proving has so far failed in formalizing interesting mathematics is that these two problems are not separate. There are reasoning principles in higher-order logic which require you to invent new Lemmas on the fly. For instance, in order to perform induction you typically need to generalize the goal statement to obtain a more useful inductive hypothesis. This can be arbitrarily complicated. I'm sure that this is another problem which will eventually be solved (same as AGI?), but if you can solve it at even a fraction of the efficiency of a normal human then you have just made programming obsolete. It is a simple matter of encoding some refinement calculus in Coq and then synthesising programs by giving examples and constraints... One last remark, before somebody accuses me of being excessively negative: There are some subproblems for which we have solutions that work amazingly well. For instance, if you are looking at purely equational reasoning, then a computer with a good implementation of paramodulation or unfailing Knuth-Bendix completion is better than any human. Boolean propositional logic is another example where computers are much better. Finally, there are classes of sums/integrals/recurrences/differential equations where again, computers are better. There are more problems like this, but I'll stop here. The point is that we only know how to solve specific problems. Nobody has ever made any progress in developing a program which automatically explores a theory and finds solutions to new problems. Saying that we will solve this problem within 10 years is the same as saying that we will solve teleportation in 10 years. There is zero real progress in the problem, so what data are you extrapolating from?