It wouldn’t just guess the next line of the proof, it’d guess the next conjecture. It could translate our math papers into proofs that compile, then write libraries that reduce code duplication. I expect canonical solutions to our confusions to fall out of a good enough such library.
I would expect such libraries to be a million lines of unenlightening trivialities. And the “libraries to reduce code duplication”, to mostly contain theorems that were proved in multiple places.
It wouldn’t just guess the next line of the proof, it’d guess the next conjecture. It could translate our math papers into proofs that compile, then write libraries that reduce code duplication. I expect canonical solutions to our confusions to fall out of a good enough such library.
I would expect such libraries to be a million lines of unenlightening trivialities. And the “libraries to reduce code duplication”, to mostly contain theorems that were proved in multiple places.