Source: The Next Web
A mathematician funded to spend five years formalizing Andrew Wiles's proof of Fermat's Last Theorem watched Claude complete the task in less than two weeks. The speed gap raises immediate questions about whether institutions should continue funding years-long solo efforts to translate human proofs into machine-verifiable code when LLMs can now do this work at scale. This directly threatens a funding model built on the assumption that formalization requires sustained expert labor, not a weekend of API calls.