태그: #isabelle-hol
GPU·LLM·MLOps·쿠버네티스, 그리고 마음가짐에 관한 글 · 1 편
Lean 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