Venture(US:VEMLY) 3 6 Ke·2025-09-12 09:01Core Insights - Christian Szegedy, former co-founder of xAI and chief scientist at Morph Labs, has launched a new company called Math Inc., focused on creating verifiable superintelligence through automated formalization technology [1] - Math Inc. has developed an autonomous formalization agent named Gauss, which has successfully formalized the Prime Number Theorem in just three weeks, a task that previously took 18 months for a team of experts [2][3] Group 1: Gauss and Its Capabilities - Gauss is the first autonomous formalization agent designed to assist mathematicians in formal verification tasks, achieving significant milestones in a short time frame [2] - The agent autonomously operates for over 10 hours, completing approximately 95% of formalization and proof tasks, with human involvement required only for the remaining portion [6] - Gauss generated around 25,000 lines of Lean code, including over 1,000 theorems and definitions, marking a significant achievement in formal proof history [4] Group 2: Historical Context and Challenges - The process of converting human mathematical achievements into verifiable machine code has historically been costly and complex, often requiring specialized talent [3] - Previous efforts in formalizing the Prime Number Theorem took 18 months, highlighting the efficiency of Gauss in comparison [3] - The project faced challenges in scaling the Lean verification environment to support thousands of concurrent agents, which was addressed through collaboration with Morph Labs [6] Group 3: Academic Reception and Future Prospects - Gauss has received positive feedback from the academic community, with experts recognizing its potential to revolutionize formal verification and mathematical collaboration [7] - Math Inc. aims to enhance Gauss's capabilities and autonomy in future versions, with plans to significantly reduce the time required for large formalization projects [7] - The company is currently engaging with mathematicians for beta testing, indicating a proactive approach to integrating Gauss into practical applications [7] Group 4: Background of Christian Szegedy - Christian Szegedy has a notable background, having previously worked at Google and contributed to significant advancements in deep learning, including the development of Batch Normalization [8][10] - His experience in AI and formal verification positions Math Inc. as a promising player in the field of verifiable superintelligence [8][9]