[xamuel]

>Till the point when computers will create thousands of proofs a man will have trouble to understand.

I'm skeptical this will ever happen. If we create a computer X that comes up with such proofs, and we create X in such a way that we fully trust X's truthfulness, then we can trivially understand every theorem X asserts: the explanation for every such theorem is, "The theorem is asserted by X."

To put it another way, suppose I have an algorithm A which I know churns out true theorems with proofs. Suppose I run A for awhile and it churns out a theorem with a gigantic proof. The fact that the proof is gigantic is totally irrelevant. I can completely ignore said proof and accept the theorem because I know that A outputs true theorems. That knowledge itself obsoletes the very proofs A churns out.

This line of reasoning can be made quite formal and rigorous. See the following slides for a deeper step into it, with a link to a paper if you want to go deeper still: https://semitrivial.github.io/MeasuringIntelligence2019.pdf

[nshm]

Thank you for the link, very exciting research. I definitely agree that there are separate activities to formulate the theorem and to prove already described one. The former requires some kind of creation and imagination and might not be automated soon, the latter is probably just a directed search like AlphaGo and can be automated in a near future.

But the implementation of such automated prover means that proofs will die since human will only propose the theorems and machine will prove them maybe in some huge computation. That might be more effective overall and will probably open some new knowledge areas but at the same time humans gonna loose the need and ability to prove the statements.