AI在IMO中表现出银牌水平

hbghlyj

在Hacker News上讨论了DeepMind开发的AI在解决国际数学奥林匹克（IMO）问题方面的表现。
该AI系统能够独立解决多个IMO问题，并使用Lean定理证明助手生成了形式化的证明。
然而，社区对问题的形式化过程提出了质疑，担心在将自然语言问题转化为形式语言时，是否无意中提供了答案，从而影响了AI的独立性。
一位参与该项目的用户澄清，AI确实是自主找到了解决方案，并提供了完整的Lean证明。
LeanDojo: Theorem Proving in Lean Using LLMs