生成式人工智能会产生幻觉，这引发了一个科学界无法承受的“真理问题”。计算机科学家图多尔·阿希姆认为，一个已有400年历史的想法可以解决这一问题：莱布尼茨曾梦想构建一个逻辑框架，在这个框架中，错误根本不可能发生。了解他关于数学超级智能的构想——该构想将使人工智能建立在形式化验证的基础上，从而将不可靠的聊天机器人转变为科学发现的严谨伙伴。

通往数学超级智能之路

Mathematics has driven progress for thousands of years, but today, human verification can't keep up with the accelerating pace of AI-generated proofs. Legendary problems like the Poincaré conjecture took years for global teams to validate, while modern AI can now solve Olympiad-level challenges in hours. A 400-year-old vision of formalized logic, now realized through tools like Lean and Mathlib, promises certainty and trust in mathematical results. This shift lets humanity focus on creativity and exploration, while AI handles precision and proof verification.

AI And Formal Math Will End The Human Bottleneck In Discovery

For 4,000 years, math has relied on human trust and peer review, but the explosion of AI-generated proofs now overwhelms expert capacity to verify them. Legendary problems like the Poincaré conjecture already required years of collective scrutiny. A new era is emerging, where computers use formal languages like Lean to check proofs with absolute certainty. This shift could enable AI to collaborate reliably with humans, replacing tedious checking with creative exploration.