菲尔兹奖成果首次被AI完整形式化，Gauss20万行代码改写数学史？

Core Insights - Math, Inc. has achieved a significant milestone in the field of mathematics by formalizing the proof of the optimal sphere packing theorem in 8-dimensional and 24-dimensional spaces using their AI, Gauss [1][3][10] - The formalization of this theorem marks a revolutionary moment in the collaboration between AI and human mathematicians, showcasing the rapid advancements in AI-assisted mathematical research [6][21][22] Company Overview - Math, Inc. was founded by Christian Szegedy, a former co-founder of xAI and chief scientist at Morph Labs, focusing on developing AI technologies for formal verification in mathematics [3][15] - Gauss, the AI developed by Math, Inc., is designed to assist mathematicians in formal verification tasks, combining natural language reasoning with formal reasoning capabilities [15][16] Achievements - The formal proof of the optimal sphere packing theorem in 8 dimensions was completed in just two weeks, while the 24-dimensional proof involved over 200,000 lines of code [18][23] - Gauss previously completed the formalization of the Prime Number Theorem in just three weeks, a task that took human mathematicians 18 months [3][16] Collaboration and Impact - The collaboration between Math, Inc. and human mathematicians has led to significant advancements, including the identification and correction of errors in existing proofs [16][21] - The formalization of these mathematical results is expected to accelerate research processes and deepen the understanding of the interconnectedness of mathematical knowledge [23][24] Future Directions - Math, Inc. plans to continue collaborating with the sphere packing project and other formal mathematical libraries to ensure the long-term usability and maintainability of the code generated by Gauss [24]