Sophie Schmieg on Nostr: back when the four color theorem was first proven with a heavily computer aided case ...

back when the four color theorem was first proven with a heavily computer aided case by case analysis, there was some discussion around whether this proof even "counted". After all, no mathematician would be able to do the case by case analysis themselves, so arguably no one could follow the proof as is. At least some of the LLM problem seems very similar, it's not clear what the value of a proof is when the only way to understand it is as a set of statements in lean, without any actual mathematical insight.