We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems, including problems from the AMC12 and AIME competitions, as well as two problems adapted from the IMO.
这个标题的传播点在于“Solving (some)”的克制表达和“formal math olympiad problems”的反差感：既强调成果，又不夸大范围，容易吸引对 AI、数学和形式化证明都感兴趣的读者。它适合改写成更大众化的表达，比如“AI 开始解奥赛题了，但只是在形式化证明框架里”，借势突出“机器证明数学”的新鲜感。需要注意的是，标题本身并没有承诺“全面攻克”，所以传播时最好保留这种限定，避免夸张。
文章最值得提炼的观点是：神经定理证明器已经能在 Lean 这样的形式化系统中，解决一部分具有挑战性的高中奥赛题，包括 AMC12、AIME 以及两道改编自 IMO 的题目。它传达的不是“AI 已经像人一样做数学”，而是“在严格形式化表达下，模型已经能对一部分题目给出可验证的证明”。从摘要看，关键价值点在于把“可生成答案”推进到“可机器验证的证明”，但具体覆盖率、失败案例和泛化边界，摘要没有提供，不能据此下结论。
可以做成“AI 离数学家还有多远”的解读短文，重点讲清楚“会解题”和“会形式化证明”是两回事，适合面向泛科技读者。也可以做成视频或播客选题，把 Lean、神经定理证明器、奥赛题这三个概念拆开，解释为什么这个成果在 AI 研究里重要。社媒帖则适合用“AI 开始碰奥赛题了，但它真正厉害的地方不是算出来，而是能被形式系统检查”这种角度，顺带引出“形式化数学会不会成为下一波 AI 研究热点”。