近日，Axiom 宣布已完成对整个 Stacks Project 的 Lean 形式化。Stacks Project 是现代代数几何领域的重要开源参考文献，系统整理了概形、层、上同调等核心理论，是当代数学研究的基础性资源。此次发布将这一长期积...

继OpenAI在周六宣布其模型获得金牌后，Google也宣布其Gemini Deep Think模型在国际数学奥林匹克竞赛（IMO）中解决了六道题目中的五道，并获得了赛事官方认证的金牌标准。这一突破标志着Google在人工智能领域的重大进...

近日，开发者ndrwnaguib在GitHub上发布了一个引人注目的开源项目，旨在使用Lean4定理证明器对伯特兰·罗素教授的经典著作《数学原理》第一卷进行形式化验证。该项目严格遵循罗素原著中的证明过程，仅在必要时添加形式...