[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.