Something remarkable happened this week. A human-AI collaboration formally verified Maryna Viazovska’s Fields Medal-winning proof of optimal sphere packing in 8 and 24 dimensions. Math, Inc.’s AI agent Gauss autoformalized the 24-dimensional proof — over 200,000 lines of Lean code — in just two weeks, with no pre-existing blueprint to work from.… Read More “The Age of the Navigator: Why AI in Mathematics Changes Everything — and Nothing”