What's amusing to me in this context is, summarizing emails and such has for a while been a supposed use case for AI—the LLM serving as the "synthesist" to explain long texts accessibly. But with this math question, a human "synthesist" would be needed to approximately understand the math discovered and programmatically verified by the LLM. So the roles reverse.