タグ: #alphaproof
GPU・LLM・MLOps・Kubernetes、そしてマインドセット · 2 件
超人間ゲームAI 2026 — Stockfish 17 / Leela Chess Zero / KataGo / AlphaZero / MuZero / Cicero / Pluribus / AlphaStar / 将棋 dlshogi 深掘りガイド
2026年の超人間ゲームAIを一枚の地図にまとめる。Stockfish 17（チェス最強）、Leela Chess Zero（NNベース）、Komodo Dragon 3、AlphaZeroからMuZeroへ続くDeepMind系、Maia（人間らしいチェス）、KataGoとLeela Zero（囲碁）、AlphaGo（李世乭との対局）、Pluribus（6人ポーカー）、Cicero（Diplomacy + 言語）、AlphaStar（
2026-05-16 · 34 分で読めます #game-ai#chess-engine#stockfish#leela-chess-zero#lc0Lean 4 & 定理証明支援系 2026 — mathlib / Rocq (旧 Coq) / Agda / Isabelle / FStar / AlphaProof / AIMO 深掘りガイド
2026年、定理証明支援系(proof assistant)はもはや学界の秘密兵器ではない。Lean 4 は Leonardo de Moura が AWS に移って以来爆発的に成長し、mathlib は 100 万定理を超え、Terence Tao を含む一流数学者の日常の道具となった。Coq は 2024 年 3 月に Rocq へリブランドを完了し、Agda・Idris 2・Isabelle/HOL はそれぞれの位置を保つ。Mic
2026-05-16 · 35 分で読めます #lean-4#lean#mathlib#rocq#coq