Astra 两小时攻下两个十年悬而未决的猜想
研究者称 Astra 两小时内给出两个 2016 年最佳臂识别猜想的算法与证明框架，Fable 5.1 复核无问题，并用 Lean 4 形式化通过内核检查。
Astra developed the key ideas for two decade-old conjectures in just two hours. 😱 @OpenAI @sama @gdb On Sept 6, Xiangxin @NickZhou523786, Jiaxi, and I asked GPT-6-Astra to tackle Chen @wjmzbmr1 & Li’s 2016 best-arm identification conjectures. It produced the key algorithm and proof framework for resolving both in the independent, unit-variance Gaussian setting. Claude Fable 5.1 cross-checked the proofs and found no issues. After preliminary human review, we formalized the main results in Lean 4, also with GPT-6-Astra, passing the kernel check on Sept 8. On Sept 10, CodeBuddy + hy4-preview discovered that another team had posted a concurrent solution on arXiv (https://arxiv.org/abs/2609.10529v1) the day before (Sept 9). Our proof takes a different route, and we also provide Lean formalization code. Manuscript + code: https://github.com/zhouxiangxin1998/GapEntropy The way we do research may be changing faster than we expected. Also thanks @thsottiaux for the reset :)