RESEARCH / 04
OpenAIが数学の新成果722編を公開 — 未公開の内部フロンティアモデル、Lean形式化とともにGitHubで
OpenAIが2026年10月6日に公開した数学研究成果コレクション（372ファミリー・722編、GitHubリポジトリopenai/math）を一次情報から整理する。約4,000問への出題、Lean形式化の提供範囲、検証上の注意点、リポジトリ構成を解説。
TAG / TOPIC
Lean
「Lean」に関するAIニュースと解説記事の一覧です。
03 STORIES
LATEST STORIES
Leanの新着記事
RESEARCH / 04
Anthropic、Claudeがフェルマーの最終定理の完全な計算機検証付き証明を11日間で生成と発表 — Leanで1,300万行、2.95万の補題
AnthropicがClaudeによるフェルマーの最終定理の形式化を発表。11日間・ほぼ自律・Leanで1,300万行・30,300定理を証明し最終証明に29,500を使用。Prove2MeとClaude Codeベースのマルチエージェント構成、約60億出力トークン、Mathlibの5倍超で史上最大のLean証明。Buzzard氏の査読とGitHub公開を一次情報に基づき整理。
RESEARCH / 04
Terence Taoら、Lean検証数学の登録所「Palomar」を公開 — AI生成証明の急増に対応する新インフラ
Terence Taoら9名は2026年8月18日、Leanで検証された数学の登録所「Palomar Registry」を公開したと発表した。ICARMとLean Focused Research Organizationが共同で立ち上げ、Lean FROのcomparator、Mathlibのformalization.yaml、文書生成のVersoを中核技術とする。2026年に入りAI支援の証明・形式化が急増し、未検証の主張が拡散する課題に対応し、検証の最低基準と検索可能な持続的記録を提供する。登録は新規性や重要性の認定ではない。