2024年，年轻的数学家Sidharth Hariharan在洛桑见到了菲尔兹奖得主Maryna Viazovska。两人随后启动了一个极具野心的项目：将Viazovska在2016年证明的“8维球体填充定理”，用Lean定理证明器完整地形式化。 所谓“形式化”，简而言之，就是把数学论文中的每一个推理步骤，翻译成计算机可以逐行验证的逻辑代码。这是一项极其耗费心血的工程——论文中看似简短的一行推理，往往需要后台写出几百行代码来填补逻辑跳跃。 Hariharan的团队花了整整两年时间搭建框架、撰写蓝图、定义…