>>10813673You're argument that "Math can be automated easily because it's not even tangible" is stupid.
The efforts to automate things such as construction, manufacturing, mining and agriculture have all been successful. You just don't see miners panning for gold or farmers tilling fields by hand anymore.
People who tried applying machine learning to Coq failed to discover anything new. People who tried to design programs that produce conjectures have also failed to make any progress.
Empirically, it would seem that mathematicians are going to be the last to be automated. It seems that the factor that limits the viability of using computers to prove theorems is the cleverness of the programs we can write for them, and this is a problem that's up there with the Riemann hypothesis and 3n+1 conjecture
