Mathlib

【geek-terminalニュース】Terence TaoのMath 2.0とAI数学計算資源論の最新情報

📝 本日のニュース概要以前お伝えしたAI生成数学原稿とTerence Tao周辺議論の続報です。今回はOpenAI数学原稿そのものではなく、Tao氏のCaltech講演スライド「Math 2.0」を中心に、AI数学を証明生成ではなく探索科...

【geek-terminalニュース】MathCode登場、数学AIは証明する知性なのか超高速な探索装置なのか

📝 本日のニュース概要 MathCodeは自然言語の数学問題をLean 4定理へ変換し、形式証明を試みる端末型AIコーディングエージェントです。永続Lean REPL、Mathlib補題探索、LSP診断修復、並列プランナーを軸に、数学AIの...