AUTOLEAN

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

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