DeepMind 用 Gemini Argon 压缩数学问题图灵机状态数
Google DeepMind 团队用 Gemini Argon 压缩哥德巴赫猜想、黎曼猜想、ZF 一致性三个问题的图灵机状态数，并在 Lean 4 中完成端到端验证，代码已开源。
It has been a blast hunting cryptids with such a great team 👾 Alongside the Busy Beaver holdout proofs, we also open-sourced smaller 2-symbol Turing machines for three foundational math problems, verified end-to-end in Lean 4 from a blank tape to Mathlib (0 sorry): - Goldbach's Conjecture: 25 -> 21 states - Riemann Hypothesis: 120 -> 104 states - ZF Consistency: 393 -> 380 states Using Gemini Argon, we compressed the community baseline machines and proved both the state reductions and full mathematical semantics in the kernel: each machine halts if and only if the conjecture fails (or ZF is inconsistent). Best part of releasing this openly: within days of going live, a community contributor already built on our 104-state proof to push the Riemann machine down to 95 states. 🚀 Huge thanks to everyone across the @GoogleDeepMind team who contributed to this project: @tomzahavy, @robertarail, @dsantosmarco, @vivek_veeriah, @Dahoas1, @zuza777, @MoritzFirsching, Andrew Bolt, Satinder Singh, Hussain Masoom, and Petar Sirkovic, as well as the Busy Beaver community. Code: https://github.com/google-deepmind/cryptids
这条是引用着另一条写的：「DeepMind 用 Gemini 4 Argon 发现 20 个新 Busy Beaver Cryptid」