OpenAI的Astra模型一口气放出10个数学证明，还带Lean验证和推理过程，数学爱好者可以围观了。
OpenAI研究员Sebastien Bubeck表示，Astra是OpenAI下一个主要模型，已独立证明多个数学难题。OpenAI将发布10个Astra证明，每个都附带完整Lean证书和思维链（CoT）推演。结果包括对von Neumann代数中Connes刚性猜想的反驳，以及高维球堆积、电路复杂度、多色图中单色三角形的更好界限。这一进展让独立研究者对AI驱动的科学发现感到兴奋。
do you all feel that liftoff? being an independent researcher make me feel extremely excited for the...
do you all feel that liftoff? being an independent researcher make me feel extremely excited for the future of ai-powered scientific discovery Sebastien Bubeck @SebastienBubeck yes, nonsofic groups exist: this statement is one of many new beautiful results proved by Astra, our next major model. We're releasing 10 such Astra proofs, complete with lean certificates and CoT walkthroughs for each of them. The results are wide-ranging, from von Neumann algebras (disproof of Connes' Rigidity Conjecture) to better bounds for high dimensional sphere packing, for circuit complexity, for monochromatic triangles in multicolored graphs, and more. More thoughts here: openai.com/index/ten-adva… 🔗 View Quoted Tweet 💬 1 🔄 0 ❤️ 4 👀 1226 📊 1 ⚡