本文整理了2026年9月16日以太坊基金会Protocol团队在Reddit上的AMA内容，梳理了以太坊下一阶段的技术路线。核心主线是抗量子迁移正影响未来几年的技术优先级，目标在2029年底前实现抗量子的L1，涉及账户签名、共识层BLS替代和KZG调整。Frames让交易验证可编程，成为账户抽象的关键。ZK-EVM进入实际生产，实时证明性能风险显著降低，但工程条件与状态增长仍是瓶颈。隐私推进有序但内置隐私池尚无共识。形式化验证工具链逐步完善。货币政策与ETH发行调整仍需社区更大范围共识。
孙宇晨宣布设立以自己名字命名的数学奖。他以诺贝尔的生平类比，说明自己财富源自数学（区块链建立在椭圆曲线等密码学之上），设奖是还债。奖项规则：奖跟题走，不跟人走，人与AI均可获奖，以机器形式化验证为唯一发钱标准，题单由他定价且锁死不可更改。他引用Dario Amodei的'数据中心天才之国'理念，强调奖励'悬空但严丝合缝'的纯粹推理。奖池已打入区块链，公开可查验，其公益重心将转向此奖。
文章回应25位菲尔兹奖得主关于AI将损害数学的宣言。作者以AlphaGo‘第37手’为例：AI出现后职业围棋水平不降反升，因为开源引擎让每位棋手拥有超人类导师。作者认为菲尔兹奖得主担心的核心问题真实存在——AI正在把解题的成果与过程分离，但他们忽略了更深层的变化：验证成本的历史性反转。过去猜测便宜而验证昂贵，如今借助Lean等证明助手和形式化证书，验证变得廉价可复制。数学的制度体系（同行评审、长学徒制）都是围绕验证稀缺建立的。AI不会摧毁数学，反而会让数百万人得以参与，让‘十亿数学家’绽放。
文章介绍了OpenAI于8月1日公布的数学与理论计算机科学领域十项新进展，涵盖高维球堆积、编码理论、Connes刚性猜想、算术电路复杂度、多色Ramsey数等长期开放问题，既有新上下界也有反例。这些结果由内部版Astra模型生成，总成本仅约2000美元，随后由人类研究者配合整理成论文，并用Lean形式化证明系统验证。作者认为AI在科研中的角色正从读论文、辅助推导走向搜索开放问题、提出新证明、形式化验证与人类审查的闭环。
文章分析了 AI 如何同时推动形式化验证的需求与供给曲线移动。在需求端，AI 代码生成增加了对可信验证的需求，以解决审查瓶颈和意图确认问题；在供给端，AI 自动化了证明生成和规格编写，降低了成本。文章指出，密码学、区块链等高风险领域将率先受益，验证正从高端服务转变为软件基础设施。
文章回顾了人工智能与数学证明的深厚渊源，从1950年代的Logic Theorist到哥德尔不完备性定理，探讨了形式化数学的演进。重点介绍了现代AI数学的基础设施LEAN（包括其核心人物Leonardo de Moura、从v3到v4的演进及mathlib库），以及DeepMind、Harmonic、Axiom Math等科技巨头和初创公司在AI自动定理证明领域的布局。文章指出，AI正在通过神经网络与形式化验证的结合，重新回归逻辑推理的起点。
文章介绍了一种基于函数式事件溯源（Functional Event Sourcing）的库，旨在让业务逻辑 Bug 在结构上不可能发生。作者通过定义可组合的状态机，在类型层统一描述状态转换，自动生成决策逻辑和演化逻辑，从而避免两者不一致。此外，该库还能自动生成 Mermaid 流程图，并利用 SMT 求解器验证业务不变性，大幅提升代码的健壮性和可维护性。
