its seeming resemblance to how human mathematical progress happens
Well, one important-to-me disanalogy is that they used the Lean proof-assistant as ground truth for an LLM’s purported proof being valid or not. Whereas human mathematical progress obviously does not require proof-assistants—humans were doing math long before proof-assistants existed. (More on this in §1 of my post “Sharp Left Turn” discourse: An opinionated review.)
I’ll bow out of that argument. Time will tell!
Well, one important-to-me disanalogy is that they used the Lean proof-assistant as ground truth for an LLM’s purported proof being valid or not. Whereas human mathematical progress obviously does not require proof-assistants—humans were doing math long before proof-assistants existed. (More on this in §1 of my post “Sharp Left Turn” discourse: An opinionated review.)