태그: #alphaproof
GPU·LLM·MLOps·쿠버네티스, 그리고 마음가짐에 관한 글 · 2 편
초인간 게임 AI 2026 — Stockfish 17 / Leela Chess Zero / KataGo / AlphaZero / MuZero / Cicero / Pluribus / AlphaStar / 将棋 dlshogi 심층 가이드
2026년 초인간 게임 AI를 한 글로 정리한다. Stockfish 17(체스 최강), Leela Chess Zero(신경망), Komodo Dragon 3, AlphaZero에서 MuZero로 이어진 DeepMind 계열, Maia(인간 같은 체스), KataGo와 Leela Zero(바둑), AlphaGo(이세돌), Pluribus(6명 포커), Cicero(Diplomacy + 언어),
2026-05-16 · 39 분 읽기 #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
2026-05-16 · 37 분 읽기 #lean-4#lean#mathlib#rocq#coq