Comment by 2b3a51

Andrew Wiles was also careful about communicating progress on his Fermat's Theorem proof during the years in his attic. So yes I take the point.

I read the Mastodon thread as more about the 'flattening' and 'rawness' of the proofs these systems and their operators are producing. I mean what is the cultural significance of a lean proof that is half a million lines long or something? And what tools can be extracted for further work from such a construction?

The late William Thurston wrote about the culture of mathematics in that sense.