本書は情報理論の入門書である．情報量の基本的な性質から始めて，データ圧縮と通信の限界を定める符号化定理を示し，統計学・計算理論・ポートフォリオ理論などとの接点までを扱う．読むのに要るのは学部で学ぶ確率・解析・線形代数までで，Lean の知識は要らない．
内容は Cover & Thomas の『Elements of Information Theory』第2版を下敷きにしている．本書は原著に代わるものではないので，情報系の学部生には原著かその翻訳を読むことを勧める．
本書は文章も形式化もすべて Anthropic の言語モデル Claude が書いた．まず，原著そのものは入力として与えず，Claude が学習で得た知識から原著の定理を書き出させ，それをLean 4 で形式化させた．次に，形式化された定理をもとに本文を書かせた．
定理を先に形式化してから本文を書いているので，主要な結果には「形式化」の枠を添えてある．枠に挙げた Lean の宣言は，未証明の仮定を残さずに機械検証された定理であり，枠の付いた結果の正しさは機械が保証している．宣言名はリンクになっていて，本のアイコンはその定理の解説ページへ，GitHub のマークはソースへ飛ぶ．形式化と本文のソースはすべてGitHub のリポジトリで公開している．
本文の証明は，前提知識が少なくて済むことと読みやすさを優先して組み立てたので，Lean がたどる証明の道筋とは必ずしも一致しない．機械検証が保証するのは定理の正しさであり，本文の証明の手順はその対象ではない．
情報理論入門（Lean による形式証明つき）・GitHub