Overview
- Two leading AI labs have posted claimed solutions across disciplines, including a Navier–Stokes submission and papers that say the Exponential Time Hypothesis is false.
- Both OpenAI and Anthropic provided Lean formal proof files so machines can check formal steps but several researchers have reported mismatches between the written manuscripts and the Lean code.
- Advisory group AGMAI and many scholars have urged immediate, broad access to the materials and funding for independent audits instead of restricted, vendor-controlled review.
- Teams of human experts at universities and institutes have begun line-by-line audits and are producing readable expositions and trimmed proofs to make the AI outputs usable for ordinary researchers.
- If the claims hold, large swaths of theory that depend on ETH and related assumptions will need re-evaluation, and the field faces new labor and funding demands to verify and translate AI-generated work into human knowledge.