AI駆動で学ぶ Lean 4 入門

Lean 4で数学の証明を機械検証する——その体験を、AI（Claude）との協働による失敗もハルシネーションも包み隠さず記録した一冊です。 本書は単なる文法書ではありません。「知識ゼロから、AIをメンターとして使い倒し、未知の証明を自力で切り拓く」ための実践的サバイバルガイドです。 【本書で得られる4つのスキル】 エラー読解と「型」のメンタルモデル：初心者が必ず絶望するエラーの根本原因を理解する AI駆動証明の技術：AIに嘘をつかせない「3点セット」のプロンプト術 Mathlib探索プロトコル：10万の定理の海から目的の武器を掘り当てる手法 sorry駆動開発：仮の足場を使って進めるトップダウン型の証明構築術 環境構築から始め、型クラスやMathlibの沼を抜け、最終章では線形代数の「次元定理」を完全証明します。 対象読者：線形代数の基礎知識（ベクトル空間・線形写像）を持つ方。Lean 4およびプログラミングの経験は一切不要です。