OmniTools 5月23日消息，Google DeepMind提出AlphaProof Nexus系统，将大型语言模型（LLM）与Lean形式化验证工具深度集成。该系统支持LLM在生成数学证明过程中实时读取Lean编译错误并动态修正，同时可调用更强工具辅助解决子问题。
该机制要求模型每一步推理均转化为可编译、可验证的代码，使其角色从“令人信服的叙述者”转向“候选方案生成器”。在353个Erdős问题和492个开放猜想的测试中，系统成功解决9个Erdős问题，并证明44个序列猜想。
研究凸显形式化验证在识别AI逻辑缺陷、构建“人类提问—模型探索—验证器把关”新型协作范式中的关键价值。