AI数学家“亚里士多德”利用强化学习、蒙特卡洛树搜索及Lean形式化证明系统，在6小时内成功破解困扰30年的埃尔德什问题#124简版。这一突破不仅展现了专业AI Agent在复杂数学推理上的强大能力，超越了通用大模型的局限性，更预示着数学研究将进入人机协作的“vibe proving”时代，并将加速形式化方法在商业和科学发现领域的广泛应用，重塑人类认知与探索的边界。

一项由斯坦福大学、UC伯克利和MIT合作的开创性研究揭示，顶尖大语言模型在解决奥数级不等式证明问题时，尽管常能得出正确答案，但其内部逻辑推理过程却充满漏洞。研究团队通过创建IneqMath数据集和LLM-as-Judge评估系统，量化了这种“可信度错觉”，并指出模型规模的增大或延长思考时间并不能有效提升其逻辑严谨性，但自我反思和引入外部定理线索等策略显示出改善潜能，为AI的可靠性与信任问题带来了深远启示。

香港科技大学团队发布的MATP-BENCH基准测试显示，当前多模态大模型（MLLMs）在理解图文结合的数学问题并将其形式化方面表现尚可（45%成功率），但在构建完整、可验证的形式化证明时，其成功率骤降至仅4%，暴露出模型在严谨逻辑推理和辅助线构造等深层能力上的显著不足，这指明了AI在迈向真正智能道路上的关键瓶颈。