Comment by quantumwoke

Some observations:

1. It seems at least possible that some of the proof of NS was contained in the training data, making it less novel.

2. The formalisation of mathematics into lean has been an underappreciated force multiplier on discovery.