2026

11

  1. Formalizing US Tax Code (Using Lean)
  2. AlphaProof Code
  3. Anthropicの非公開AIモデルを使って18年間未解決だった量子コンピューターの難問が証明される

10

  1. OpenAIが数学・コンピュータサイエンス・物理学における調和解析・計算複雑性理論・量子場理論に関する3つの新たな発見を発表、指数時間仮説は誤りである

08

  1. Postmortem for Lean Kernel Soundness Bug #14576