Navier-Stokes, Sphere Packing, and Lean: How AI Entered Big Mathematics

This Habr article explores the current state of artificial intelligence integration into fundamental mathematics. The primary focus is OpenAI's claim regarding the solution to one of the 'Millennium Prize Problems' involving the Navier-Stokes equations. The author notes that the situation remains ambiguous: the proposed proof requires rigorous verification by the expert community, and disputes have arisen regarding authorship. The article examines the methods by which modern computer systems attempt to comprehend complex scientific concepts and the role of formal proof languages like Lean. It discusses both the potential breakthroughs AI could bring to theoretical physics and mathematics, as well as the existing limitations of algorithms when dealing with abstract logical structures. The piece emphasizes that despite ambitious claims from developers, the path to fully automated theorem proving remains complex and requires an interdisciplinary approach.