攻克形式化数学奥赛难题：基于 Lean 的神经定理证明器研究进展

在形式化数学领域，自动化定理证明技术正迎来新的突破。研究人员近日开发出一种针对 Lean 交互式定理证明器的神经定理证明器，旨在通过深度学习技术提升处理复杂数学逻辑推理的能力。

该系统展现出了卓越的学习能力，能够自主应对一系列极具挑战性的高中数学奥林匹克竞赛题目。其解决范围不仅涵盖了美国数学竞赛（AMC12）及美国数学邀请赛（AIME）的经典难题，甚至还成功处理了改编自国际数学奥林匹克（IMO）的两道高难度试题，展示了神经架构在处理高阶逻辑证明任务中的巨大潜力。