探讨AI在数学推理领域的进展，涵盖任务分类、主流模型及挑战，附带详实阅读清单。

近日，港大的研究显示OpenAI o1在国际奥数题测试中表现出色，揭示其真正的数学推理能力。通过严格的AB测试，该模型显示出优于死记硬背的实战能力，具体分析了其在搜索和解决类型问题上的表现，结果令人信服。

最新基准FormalMATH测试显示，即使顶级AI模型在数学证明上的表现也不尽如人意。