stanford-oval/wikipedia huggingface dataset:
Lean (証明アシスタント)
歴史 > 2021年: Lean 4

2021年、Lean 4の最初のマイルストーンリリースが発表された。C++ではなく Lean 自身によって再実装され、「Lean は定理証明支援系であると同時に、汎用プログラミング言語でもある」と標榜するようになった。
Lean 4 より以前のバージョンでは、次のような問題点が認識されていたが、Lean 4 では大幅に改善された。
Lean 3 での経験から、定理証明を上手く行うためにはメタプログラミングフレームワークを備え、高い拡張性を有することが重要であると認識されていた。しかし Lean 3 のシステムの多くの部分が、C++ で書かれた Lean 3 のソースコードを変更しない限り、ユーザには変更できなかった。
Lean 3 メタプログラミングは仮想マシン解釈のオーバーヘッドにより非効率だった。これにより Lean 3 での自動証明は、C++ や OCaml のような効率的なコンパイラを持つ言語で実装された同様の自動証明とは競合できなかった。
Lean 4 は完全に拡張可能であり、パーサ、エラボレータ、タクティク、決定手続き(decision procedure)、プリティプリンタ、コードジェネレータを変更・拡張することができる。また Lean 4 は対話的証明のためにカスタマイズされた衛生的なマクロ(hygienic macro)を持つ。Lean の構文をユーザが改変する際に C++ コードに触れる必要はなくなった。
さらに Lean 4 ではメモリ管理手続きが改善されたほか、テーブル解決に基づく新しい型クラス解決アルゴリズムが使用され、パフォーマンスが改善された。また、Lean 4 は functional but in-place と呼ばれる新しいプログラミングパラダイムに基づくようになった。
Lean 4 には Lean 3 との後方互換性はない。Lean3 で開発されていた主要なライブラリとして、2017年ごろから開発が行われていたmathlib が挙げられるが、コミュニティにより Lean4 への書き直しが行われた。これには100万行以上のコードを書き換える必要があったが、この移行作業は2023年7月に完了した。
歴史 > 2023年: Lean FRO設立

2023年7月、Lean Focused Research Organization (FRO) が設立された。形式数学革命のために、証明のUI改善、スケーラビリティの改善、証明の自動化といった問題に取り組むとしている。また2023年9月、最初のLean 4 の公式リリースが発表された。
Leanの型システム > 無矛盾性

非形式的な数学において一般的に基礎理論として採用されているのは ZFC 集合論と呼ばれる理論であるが、Lean で採用されている基礎理論は Calculus of Inductive Constructions  (省略して CIC と呼ばれる) であって、これとは異なる。
Lean の型システムの無矛盾性については、Lean 3 の時代の結果として、「 ZFC_{\omega }が無矛盾であることと、  Lean_{\omega } が無矛盾であることが同値であること」が知られている。ただし  ZFC_{\omega } とは、「ZFC に、任意の有限個の到達不能基数が存在するという仮定を足したもの」を指し、   Lean_{\omega } とは「Lean 3の型システムに、任意の有限個の universe があるという仮定を足したもの」を指すものとする。 これは、ZFC の中で Lean 3 のモデルが構築でき、Lean 3 の中で ZFC が構築できるためである。
Lean 4 については、入れ子帰納型 (nested inductive type) や構造体のη変換 (η for structures) が導入されたことが型システムに大きな影響を及ぼしており、Lean 3 に対する無矛盾性の証明はそのまま適用できなくなった。
Leanの型システム > 型付けの一意性

Lean では項の型は一意である。つまり、項 e の型が α であり同時に β であるとき、α と β は（どこかの型宇宙において）等しい。
なお、これは「型とは、集合のようなもの」という、型に対する素朴な理解とは矛盾することに注意が必要である。集合の場合は、 U\subseteq V かつ  x\in U であるならば、 x\in V が成り立つ。しかし、Lean では型 U の項を他の型の項であると直接見なすことはできない。
Leanの型システム > Coqとの差異

旧Coq (現在のRocq) は、Lean と同じくCalculus of Inductive Constructions (CIC) を採用しているという点で、Lean とよく似ているが、以下のような点で異なる。
Lean では定義は宇宙多相(universe polymorphic) であることができる。つまり、一つの定義ですべての宇宙レベルを賄うことができる。しかし、Coq では定義は不定宇宙(indefinite universe)に棲んでいる。つまり、それぞれの定義は特定の宇宙に棲んでいるが、その宇宙レベルはグローバルに可変になっている。
Coq では余帰納型(coinductive type)がサポートされているが、v4.16.0 の時点で Lean 4 は coinductive type をサポートしていない。
Lean では証明無関係(proof irrelevance)を definitional equality としてサポートしているが、Coq では propositional equality としてこれを主張する公理が用意されている。
Lean の機能 > 対話的実行

プログラミング言語としての Lean は、関数などの式を部分的に実行して評価することが容易にできるように設計されている。#eval というコマンドが存在し，関数などをその場で評価することができる。いわば、Jupyter Notebook のような対話的な実行環境が最初から利用可能であるということができる。
def frac (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * frac n

-- エディタ上でコードを開いているとき
-- `#eval` の上にマウスオーバーすると 120 と表示される
#eval frac 5
Lean の機能 > フィールド記法

Lean はオブジェクト指向言語ではなく、オブジェクトやクラスに相当する概念は存在しないが、関数適用を「まるでフィールドにアクセスするかのように」書くことができる記法が用意されている。これは Nim 言語における Uniform Function Call Syntax に似ている。
structure Point (α : Type) : Type where
  x : α
  y : α

-- アクセサ
#check (Point.x : {α : Type} → (Point α) → α)
#check (Point.y : {α : Type} → (Point α) → α)

def origin : Point Int := { x := 0, y := 0 }

-- 通常の関数適用の書き方
#guard Point.x origin = 0

-- フィールド記法。`.x` を付けるだけで値にアクセスできる
#guard origin.x = 0
Lean の機能 > 正格評価

同じく純粋関数型言語である Haskell とは異なり、Lean は正格評価である。つまり、関数を評価する前に関数に渡された引数をすべて評価する。
/-- 条件 `cond` が true なら最初の引数を，
false なら2番目の引数を返す関数 -/
def selectFst (cond : Bool) (fst snd : Nat) :=
  if cond then
    fst
  else
    snd

/-- 与えられた自然数をそのまま返す関数.
実行されると infoview に表示が出る. -/
def trace (n : Nat) : Nat :=
  dbg_trace "trace is called"
  n

/-
trace is called
10
-/
#eval selectFst true 10 (trace 20)
Lean の機能 > 帰納型

Leanでは帰納型を定義することができる。帰納型とは、「その型の項を得る関数（コンストラクタ）」を有限通り指定することで定まる型であり、Leanでは「その型の上の関数/述語を得る方法（再帰原理）」が同時に生成されることで帰納法が可能であることが保証される。
帰納型の最も簡単な例は、列挙型である。列挙型とはある定められた有限通りの値しか取らない型のことで、たとえばBoolはLeanの標準ライブラリで列挙型として定義されている。列挙型は、「コンストラクタが引数を取らない」という特別なケースの帰納型である。
inductive Bool where
  | false
  | true
コンストラクタは引数をとっても構わない。特にこれから定義しようとしている自分自身を引数に取ることも許されるので、再帰的なデータ型を定義することができる。再帰的な帰納型の最も簡単な例は、自然数である。自然数はLeanの標準ライブラリでは次のように定義されている。
inductive Nat : Type where
  | zero : Nat
  | succ : Nat →  Nat
この定義はペアノの公理に基づいており、すべての自然数はゼロもしくは他の自然数の後者であると述べている。ペアノの公理には「コンストラクタが単射」「コンストラクタの像が重ならないこと」「帰納法の原理」も含まれるが、それらの成立はLeanによって自動的に保証される。

自然数の加算はパターン・マッチングを使用して、再帰的に定義できる。
def Nat.add (n m : Nat) : Nat :=
  match n with
  | zero => m
  | succ n => succ (add n m)
Lean の機能 > 証明

Lean ではカリーハワード同型対応を利用して証明を行う。ある命題 P の証明 h は，型 P を持つような項 h : P と同一視される。したがって、Lean を仲介することによって「証明する」ということは、「正確にある型を持つような項を作る」ということに言い換えられる。
これは Lean で簡単な命題の証明項を実際に構成した例である。
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := 
  fun h => { left := h.right, right := h.left }
Lean の機能として、タクティクによって証明項を構成することができる。by キーワードによってタクティクモードに入ることができる。タクティクモードの中では、「現在利用できる仮定や命題」「今示すべきこと」が常に infoview に表示され、対話的に証明を書くことができる。
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
  -- P ∧ Q と仮定する
  intro h
  
  -- Q ∧ P を示すには Q と P をそれぞれ示せばよい
  constructor

  -- Q を示す
  case left =>
    exact h.right

  -- P を示す
  case right =>
    exact h.left
Lean の機能 > 依存型

Lean は依存型を持つ。つまり、関数 f : A → B があったときに、f による t : A の返り値 f t の型が t に依存していてもよい。このとき f の型を f : (t : A) → B のように表記する。これにより、命題に正しく型を付けることが可能である。
theorem one_add : ∀ n, n + 1 ≥ 1 := by simp_arith

/-
one_add 1 : 1 + 1 ≥ 1
-/
#check one_add 1

/-
one_add 3 : 3 + 1 ≥ 1
-/
#check one_add 3
依存型がなければ命題（これは一種の型である）が項に依存することができないので、表現することができる命題の範囲がとても狭まってしまう。定理証明支援系をプログラミング言語として実現するうえで、依存型があることはとても重要な役割を果たす。

また、依存型はより柔軟にプログラムに型を付けることを可能にし、型で表現できるソフトウェアの仕様の範囲を広げる。以下は「長さが n であるようなリスト」を Subtype として表現する型である。
def Vect (α : Type) (n : Nat) : Type := {l : List α // l.length = n }
Lean の機能 > 拡張可能性

Lean は強力なメタプログラミング機能を持っており、新しい記法の定義や証明の自動化が行えるようになっている。以下は、notation コマンドで記法を定義する例である。
def modulo (k n m : Int) : Prop := k ∣ (n - m)

-- modulo を二項関係らしく書けるようにする
notation:55 x:55 " ≃ " y:55 " mod " k:55 => modulo k x y

#check (1 ≃ 6 mod 5)
declare_syntax_cat コマンドや macro_rules コマンドを使うことで、さらに複雑な構文も定義することができる。
/-- 2項演算の集合 -/
inductive Op where
  /-- 加法 -/
  | add
  /-- 乗法 -/
  | mul
deriving BEq

/-- 数式 -/
inductive Expr where
  /-- 数値リテラル -/
  | val (n : Nat)
  /-- 演算子の適用 -/
  | app (op : Op) (left right : Expr)
deriving BEq

namespace Expr
  /- ## Expr の項を定義するための見やすい構文を用意する -/

  /-- `Expr` のための構文カテゴリ -/
  declare_syntax_cat expr

  /-- `Expr` を見やすく定義するための構文 -/
  syntax "expr!{" expr "}" : term

  syntax:max num : expr
  syntax:30 expr:30 " + " expr:31 : expr
  syntax:35 expr:35 " * " expr:36 : expr
  syntax:max "(" expr ")" : expr

  macro_rules
    | `(expr!{$n:num}) => `(Expr.val $n)
    | `(expr!{$l:expr + $r:expr}) => `(Expr.app Op.add expr!{$l} expr!{$r})
    | `(expr!{$l:expr * $r:expr}) => `(Expr.app Op.mul expr!{$l} expr!{$r})
    | `(expr!{($e:expr)}) => `(expr!{$e})

  -- 構文が正しく動作しているかテスト
  #guard
    let expected := Expr.app Op.add (app Op.mul (val 1) (val 2)) (val 3)
    let actual := expr!{1 * 2 + 3}
    expected == actual
end Expr
Lean の機能 > 自動証明

Lean は対話的に証明を書くことをサポートするだけでなく、タクティクによる自動証明機能も提供する。以下は複雑な命題に見えるが、たった一つのタクティクで証明が終了する例である。
example (a₁ a₂ a₃ : Nat) : 3 ∣ a₁ + 10 * a₂ + 100 * a₃ ↔ 3 ∣ a₁ + a₂ + a₃ := by
  omega
また次は、直観主義論理（排中律を仮定しない論理）における証明を自動で行ってくれるタクティクの例である。
import Mathlib.Tactic.ITauto

/-- 排中律の二重否定 -/
example (P : Prop) : ¬¬ (P ∨ ¬ P) := by
  intro h
  apply h
  have : ¬ P := by
    intro hp
    have : P ∨ ¬ P := by left; assumption
    contradiction
  right
  assumption

example (P : Prop) : ¬¬ (P ∨ ¬ P) := by
  itauto
Lean の特徴

Agda や Coq, Isabelle などの他の定理証明支援系と比べると Lean にはどのような特徴があるだろうか。この中で Isabelle は依存型がなく、依拠している基礎が異なるという著しい差異がある。Agda と Coq と比較すると、基礎はほぼ同じであるが、Lean には以下のような特徴がある。
Lean の特徴 > テーブル化型クラス解決(Tabled Typeclass Resolution)

型クラスは、プログラミングと定理証明の両方において、アドホック多相性  を実現してくれる。しかし、Lean の急成長中の数学ライブラリ Mathlib の中で、型クラスが広く使われるにつれ既存の型クラス解決手続きの理論的限界が進歩の妨げになるようになった。既存の型クラス解決手続きの主要な理論的限界とは、次のようなものである：
ダイアモンドが存在する場合、指数関数的に実行時間が伸びてしまう
サイクルが存在する場合に発散が生じる
Lean 4 では、この２つの問題を解決する新しいアルゴリズムであるテーブル化型クラス解決が実装されている。このアルゴリズムは Prolog に対して1998年に  提案された型クラス解決アルゴリズムに基づく。
Lean の特徴 > 拡張された do 記法

Lean は純粋関数型言語であるため、手続き型言語では暗黙に扱われる副作用を、モナドという再利用可能な抽象的要素で再定義することで扱っている。この再定義によって、副作用をより厳密に制御したり、派生的な副作用を導入したりすることを可能にしている。モナドは Haskell の最もよく知られた抽象化機能であり、そのユビキタスな糖衣構文である do 記法と常に結びついている。
Lean では、メタプログラミングフレームワークによる高い拡張可能性を生かして、do 構文が Haskell と比べて拡張されている。具体的には以下のような記法を最初からサポートしている。
可変な変数を let mut で宣言できるようにする Rust ライクな記法
早期リターン(early return)
for ループ、break や continue といった制御フロー
たとえば、以下は Lean 4 で実装したエラトステネスの篩である。
private def eratosthenesAux (n : Nat) : Array Bool := Id.run do
  let mut isPrime := Array.mkArray (n + 1) true

  isPrime := isPrime.set! 0 false
  isPrime := isPrime.set! 1 false

  for p in [2 : n + 1] do
    if not isPrime[p]! then
      continue

    if p ^ 2 > n then
      break

    let mut q := p * p
    while q <= n do
      isPrime := isPrime.set! q false
      q := q + p

  return isPrime

/-- エラトステネスの篩 -/
def eratosthenes (n : Nat) : Array Nat :=
  eratosthenesAux n
    |>.zipIdx
    |>.filterMap fun ⟨isPrime, i⟩ =>
      if isPrime then some i else none

#guard eratosthenes 10 = #[2, 3, 5, 7]

#guard (eratosthenes 100).size = 25
Lean の特徴 > Functional but in-place

ほとんどの関数型言語は、メモリ管理を自動で行うためにガベージ・コレクタを利用している。一方で、各値の正確な参照カウントを保持することで、破壊的更新などの最適化が可能になる。Lean は、純粋な関数型言語でありながら参照カウントを利用してメモリ管理を行う。参照カウントがちょうど１の値（つまり共有されていない値）を更新するとき、自動的に破壊的更新が行われる。このことを指して、Lean のプログラミングパラダイムのことを functional but in-place (FBIP) と呼ぶ。特に、Lean で配列のようなデータ構造を扱うとき、FBIP によりコードの純粋性を保ちながら効率的なコードを生成することが可能である。
これにより Lean のコンパイラが生成するコードは効率的になり、 他の静的型付け言語と比較しても遜色のないものになった。
実際に Lean が値の破壊的変更を行っていることは、次のようなコードで確認することができる。
-- Lean のオブジェクトのメモリ上でのアドレスを取得する関数
-- 参照透過性を壊すため，unsafe である
#eval ptrAddrUnsafe #[1, 2, 3]

/-- フィボナッチ数列を計算する -/
def fibonacci (n : Nat) : Array Nat := Id.run do
  -- 可変な配列 `fib` を宣言している
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    -- ここで配列 `fib` のメモリアドレスを表示させている
    dbg_trace unsafe ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

-- 値がコピーされていれば異なるメモリアドレスが表示されるはずだが...?
#eval fibonacci 15
Lean の特徴 > 衛生的でありながら強力なメタプログラミングフレームワーク

ITP（対話的定理証明支援系）において、構文を拡張可能にすることは複雑な数学的対象をわかりやすく表現するのに重要であるのみならず、ライブラリ開発においても再利用可能な抽象化を行うために役立つ。このように表現力の高いマクロシステムを持つことは ITP にとって極めて重要なのだが、Lean 3 のものを含め既存の ITP のマクロシステムには問題があった。
問題点は主に以下の２点である：
マクロの抽象化が弱く、しばしば冗長な定義をせざるをえなかった。
タクティクを定義する際などに、マクロ展開において名前の偶発的な衝突が起こってバグを生み出していた。
Lean 4 はこれらの問題を Scheme ファミリーに着想を得た新しいマクロシステムを開発することにより同時に解決した。新しいマクロシステムは、複数のマクロ抽象化レベルを単一で統一的なシステムで実装することを可能にし、高い表現力と安全性を両立した。
たとえば、以下は Coq のライブラリ math-comp における和のΣ記号の定義である。見てわかるように少しずつ異なる同様の定義が 12 回繰り返されている。
Reserved Notation "\sum_ i F"
  (at level 41, F at level 41, i at level 0,
           right associativity,
           format "'[' \sum_ i '/  '  F ']'").
Reserved Notation "\sum_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \sum_ ( i  <-  r  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \sum_ ( i  <-  r ) '/  '  F ']'").
Reserved Notation "\sum_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \sum_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \sum_ ( m  <=  i  <  n ) '/  '  F ']'").
Reserved Notation "\sum_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \sum_ ( i  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\sum_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\sum_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \sum_ ( i  <  n  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \sum_ ( i  <  n ) '/  '  F ']'").
Reserved Notation "\sum_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \sum_ ( i  'in'  A  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \sum_ ( i  'in'  A ) '/  '  F ']'").
ほぼ同じことが Lean の数学ライブラリ mathlib4 では次のように表現されている。明らかに繰り返しが少なく、簡潔な書き方になっていることがわかるだろう。
syntax bigOpBinder := term:max ((" : " term) <|> binderPred)?

syntax bigOpBinderParenthesized := " (" bigOpBinder ")"

syntax bigOpBinderCollection := bigOpBinderParenthesized+

syntax bigOpBinders := bigOpBinderCollection <|> (ppSpace bigOpBinder)

syntax (name := bigsum) "∑ " bigOpBinders ("with " term)? ", " term:67 : term
これは Lean では syntax  および declare_syntax_cat というコマンドが用意されていることと関係がある。Lean ではユーザが構文カテゴリを定義し、パーサの拡張を抽象化された高水準言語で行うことができる。これは Lean 3 までの静的なマクロでは不可能だった。
利用

Kevin Buzzard は、数学者や数学科の学部生の間で Lean のような定理証明支援系を普及させることを目指す Xena プロジェクトを主導している。Xena プロジェクトの目標の1つは、インペリアル・カレッジ・ロンドンの学部生の数学カリキュラムにあるすべての定理と証明をLeanで書き直すことである。
2020年12月、数学者の Peter Scholze は自身の liquid vector space に関する定理を Lean で形式化することは可能かという挑戦状を Lean コミュニティに持ち込んだ。この挑戦は Liquid Tensor Experiment と呼ばれ、2022年7月に完了が宣言された。
フィールズ賞受賞者の Terence Tao は、2023年10月のSNSへの投稿で、自身の論文を Lean 4 で形式化する過程で小さな（しかし非自明な）ミスを見つけることができたと明かしている。
数学理論の形式化や自動証明に対する応用だけでなく，ソフトウェアの正しさの検証やセキュリティの方面でも Lean を使用した研究がなされている。AWS は、Cedar 言語の正しさとセキュリティ特性を保証するのに Lean を使用した。
Lean の構文の例
Lean 4 の型クラス解決アルゴリズムは、実行時間を指数的に改善した.
Lean 4 のベンチマークにおける実行時間を Haskell, OCaml, Standard ML, Swift と比較した表．
永遠の0

『永遠の0』（えいえんのゼロ）は、百田尚樹による日本の小説、またそれを原作とした漫画・映画・テレビドラマ。小説本はオリコン本ランキングで史上初となる400万部を突破した。
概要

放送作家として『探偵!ナイトスクープ』などを手がける百田の作家デビュー作であり、執筆にあたっては第二次世界大戦(大東亜戦争)で出征した著者の父親や親族が影響を与えている。
2006年には当初原稿を持ち込んだ多くの出版社には認められず、縁あってサブカルチャー系の太田出版から書き下ろしで発表された。
2009年に講談社文庫から文庫化。
2010年から2012年にかけて須本壮一（本そういち）による作画で漫画版が刊行された。
2012年10月から徐々に話題を呼び、『オリコン“本”ランキング文庫部門』で歴代13作目のミリオンヒット作となった。
2013年8月付けで、湊かなえ著『告白』（2010年・双葉社）の254.4万部を超えて文庫部門1位を記録し、同年12月には文庫版の販売部数300万部を突破。歴代のタイトルで300万部超えは、オリコンの書籍全部門を通し、コミック部門の『ONE PIECE』（51巻から70巻までの計20作で獲得）に続いて史上2例目となる。2013年12月に映画が公開された。
2015年にはテレビドラマが放送された。2015年7月31日に映画版がノーカットで地上波初放送された。
2016年8月15日、オーディオブックを配信サービス「FeBe」より配信。
ストーリー

司法試験浪人の佐伯健太郎と、出版社（新聞社）に勤める姉の佐伯慶子は、亡くなった祖母・松乃の四十九日からしばらくしたころ、祖父・賢一郎から彼が自分達の実の祖父ではないことを知らされる。第二次世界大戦後、松乃は二人の母・清子を連れて賢一郎と再婚しており、実の祖父は終戦間際に特攻で戦死した海軍航空兵だと判明する。
それから6年後、司法試験浪人が長く続き人生の目標を見失っていた健太郎は、フリーライターとなった慶子から、新聞社主宰の終戦60周年記念プロジェクトのアシスタントを頼まれる。プロジェクトを進める新聞記者の高山隆二は神風特攻隊のことをテロリストだと語るが、祖父の話もありその考えに釈然としない慶子は、このプロジェクトに際して特攻隊員だった実の祖父について調べようと決めた。姉弟はわずかな情報を元にその足取りを追い始める。
厚生労働省や方々の戦友会に連絡を取ったところ、実祖父の名が宮部久蔵であり、関係者9人が存命であることが知れた。その内の一人、戦闘機搭乗員としてラバウル航空隊で一緒だったという人物・長谷川梅男を訪ねるが、元海軍少尉の長谷川は久蔵について「海軍航空隊一の臆病者」「何よりも命を惜しむ男だった」「海軍軍人の風上にも置けない奴と思った。」と姉弟に蔑みの言葉をぶつけた。
健太郎は元戦友から聞く祖父の話に困惑し、次第に調査を続ける気をなくしていたが、母から健太郎と同じ26歳で亡くなった父・久蔵がどんな青年だったのか知りたいと改めて頼まれ、さらに手がかりとなる海軍従軍者達を訪ね歩く。だが、生前の久蔵を知る者達の語ることは「生きるということを教えてもらった」と感謝を述べる者もいれば、「航空隊員として軽蔑されていた」などとそれぞれに全く違っており、調べるほどにその人物像は謎に包まれていた。
戸惑いつつも二人は、国のために命を捧げるのが当然だったといわれる戦時下の日本と、そこに生きた人々の真実について調べてゆく。
凄腕の零戦乗りで、卑怯者と誹られても「娘に会うまでは死なない」と松乃との約束を守り続けていた久蔵は、どのような生涯を送り特攻を選んだのか。実は久蔵は、特攻出撃の際、自機が整備不良であることに気づき、これに搭乗すれば生還できるという理由から、その機を前途有為な学生パイロットの一人に譲る。そのパイロットこそ、二人の祖父・賢一郎であった。終戦から60年を経て、各々の壮絶な生き方と封じられていた事実を明らかにする。
登場人物 > その他の登場人物

藤木 秀一
登場人物 > アメリカ軍の登場人物

空母タイコンデロガの艦長
エピローグに登場。近接信管を始めとする激しい対空砲火をくぐり抜けて来た宮部に敬意を表し、水葬に付す。実は彼の息子は真珠湾で戦死しており、その態度は非常に立派なものだった。
空母タイコンデロガの砲手
プロローグとエピローグに登場。タイコンデロガの五インチ高角砲の砲手。宮部の操縦技術に恐怖する。
トニー・ベイリー
第五章に登場。アメリカ軍の戦闘機パイロット。宮部の乗る零戦に撃墜され、脱出するも、そのパラシュートを宮部に銃撃される。しかし、低高度での出来事だったため、勢いがつく前に海に落下し、生還する。
書誌情報 > 単行本

『永遠の0』太田出版、2006年8月23日、448頁。ISBN 4-7783-1026-8。
書誌情報 > 文庫本

『永遠の0』講談社〈講談社文庫〉、2009年7月15日、590頁。 ISBN 978-4-06-276413-1。
児玉清による13ページの解説を収録。
漫画

双葉社『漫画アクション』誌上で2010年1月から2012年2月まで連載された。作画は須本壮一（本そういち）。アクションコミックスから全5巻が出版されている。
『永遠の0』 第1巻、双葉社、2010年7月28日。ISBN 978-4-575-83796-4。https://www.futabasha.co.jp/book/97845758379640000000?type=1。
『永遠の0』 第2巻、双葉社、2010年11月27日。ISBN 978-4-575-83839-8。https://www.futabasha.co.jp/book/97845758383980000000?type=1。
『永遠の0』 第3巻、双葉社、2011年7月28日。ISBN 978-4-575-83934-0。https://www.futabasha.co.jp/book/97845758393400000000?type=1。
『永遠の0』 第4巻、双葉社、2011年11月28日。ISBN 978-4-575-83994-4。https://www.futabasha.co.jp/book/97845758399440000000?type=1。
『永遠の0』 第5巻、双葉社、2012年4月28日。ISBN 978-4-575-84065-0。https://www.futabasha.co.jp/book/97845758406500000000?type=1。
映画

| 永遠の0 |
| --- | --- |
 THE ETERNAL ZERO
監督:  山崎貴
脚本:  山崎貴 林民夫
原作:  百田尚樹『永遠の0』（太田出版）
製作:  市川南 畠中達郎
出演者:  岡田准一 三浦春馬 井上真央 濱田岳 新井浩文 染谷将太 三浦貴大 上田竜也 吹石一恵 田中泯 山本學 風吹ジュン 平幹二朗 橋爪功 夏八木勲
音楽:  佐藤直紀
主題歌:  サザンオールスターズ「蛍」
撮影:  柴崎幸三
編集:  宮島竜治
制作会社:  ROBOT
製作会社:  「永遠の0」製作委員会
配給:  東宝
公開:  2013年12月21日
上映時間:  144分
製作国:   日本
言語:  日本語
興行収入:  87.6億円
テンプレートを表示
主演は岡田准一。第38回日本アカデミー賞最優秀作品賞受賞作品。
2013年12月21日から全国430スクリーンで公開され、初日2日間の観客動員数は約42万9000人、興行収入約5億4200万円。その後興行成績で8週連続第1位となった。幅広い客層を集めてロングランが続き、観客動員数は700万人、累計興行収入86億円を突破、歴代の邦画実写映画で6位にランクインする大ヒットを記録し、文化通信社調べによる2014年邦画興行収入第1位を記録した。
原作はこれまでにも映画・ドラマ化の話が上がっていたものの、いずれも脚本上の問題等から実現には至らなかったが、山崎貴・林民夫による企画内容を受け著者である百田尚樹が快諾し、初の映像化となった。
2014年に第16回イタリア ウディネ・ファーイースト映画祭でグランプリを受賞。日本作品の受賞は2009年の『おくりびと』以来の快挙となった。
映画 > 製作

撮影にあたり、作中に登場する旧日本海軍の零戦二一型の原寸大模型が制作されたほか、唯一現存するオリジナルエンジンで飛行可能な零戦からエンジン音が収録された。制作された零戦は、撮影終了後ゆかりの地である大分県宇佐市によって買い取られ、構想中の宇佐市平和ミュージアム（仮称）に展示される。撮影には徹底した軍事訓練と零戦搭乗経験者による指導を要し、奄美大島や鹿児島、茨城などを中心に、膨大な空撮を含む3ヶ月にわたるロケが敢行された。
山崎貴監督作品としては、初めて民放テレビ局が製作に関与していない作品となっている。また、主人公・宮部の配役には監督が元共演者である堤真一を通してその求道的な姿勢を聞き及んでいたことがきっかけとなり、岡田准一の出演が決まった。
映画 > キャスト

宮部 久蔵 - 岡田准一（V6）
佐伯 健太郎 - 三浦春馬
大石 松乃 - 井上真央
佐伯 慶子 - 吹石一恵
佐伯 清子 - 風吹ジュン（幼少期：栗本有規）
大石 賢一郎 - 夏八木勲（青年期：染谷将太）
井崎 源治郎- 橋爪功（青年期：濱田岳）
武田 貴則- 山本學（青年期：三浦貴大）
景浦 介山- 田中泯（青年期：新井浩文）
長谷川 梅男- 平幹二朗
小山 - 上田竜也（KAT-TUN）
伊藤 - 青木健
香川 - 遠藤雄弥
寺西 - 栩原楽人
映画 > スタッフ

原作：百田尚樹『永遠の0』（太田出版）
監督・VFX：山崎貴
脚本：山崎貴、林民夫
音楽：佐藤直紀
VFXディレクター：渋谷紀世子
プレビズアドバイザー：栃林秀
撮影：柴崎幸三
美術：上條安里
照明：上田なりゆき
録音：藤本賢一
編集：宮島竜治
音響効果：岡瀬晶彦
装飾：龍田哲児
スクリプター：甲斐哲子
助監督：山本透
企画：アミューズ
制作プロダクション：ROBOT
VFXプロダクション：白組
制作協力：東宝映画、阿部秀司事務所
配給：東宝
製作：「永遠の0」製作委員会（東宝、アミューズ、アミューズソフトエンタテインメント、電通、ROBOT 、白組、阿部秀司事務所、ジェイ・ストーム、太田出版、講談社、双葉社、朝日新聞、日本経済新聞社、KDDI、TOKYOFM、日本出版販売、GYAO、中日新聞社、西日本新聞社）
映画 > 主題歌

「蛍」
映画 > Blu-ray / DVD

2014年7月23日発売。2014年、TSUTAYAが発表したレンタルDVD／ブルーレイ年間ランキングで第3位を獲得。
映画 > Blu-ray / DVD > 永遠の0 Blu-ray / DVD 通常版

1枚組 - 本編DISC（本編144分、予告・特報・テレビスポット集）
映画 > Blu-ray / DVD > 永遠の0 Blu-ray / DVD 豪華版

2枚組 - 本編DISC、特典DISC 140分（製作メイキング集、劇場公開時特番、舞台挨拶集）
封入特典：限定コンテンツ用ARカード
初回生産限定特典：ブックレット 154ページ（撮影日誌、場面写真・メイキング写真集、美術設定集、インタビュー他）、特製アウターケース付きデジパック仕様
映画 > テレビ放送

| 回数 | テレビ局 | 番組名（放送枠名） | 放送日 | 放送時間 | 放送分数 | 視聴率 | 備考 |
| --- | --- | --- | --- | --- | --- | --- | --- |
| 1 | 日本テレビ | 金曜ロードSHOW! | 2015年7月31日 | 19:58 - 22:54 | 178分 | 13.2% | 本編ノーカットで地上波初放送された 。 本編開始前に、主演の岡田准一のコメント映像などがあったため、本編は20:01からスタートとなった。 |

視聴率はビデオリサーチ調べ、関東地区・世帯・リアルタイム。
テレビドラマ

| テレビ東京開局50周年特別企画 永遠の0 |
| --- | --- |
ジャンル:  テレビドラマ
原作:  百田尚樹
脚本:  櫻井武晴
監督:  佐々木章光
出演者:  向井理
製作
プロデューサー:  岡部紳二（CP）、阿部真士、佐々木章光、森一弘、近見哲平、石田義一
制作:  テレビ東京、テレパック

放送
放送国・地域:  日本
 公式サイト

第1夜
放送期間: 2015年2月11日
放送時間: 水曜20:54 - 23:18
放送分: 144分
回数: 1

第2夜
放送期間: 2015年2月14日
放送時間: 土曜20:58 - 23:14
放送分: 136分
回数: 1

第3夜
放送期間: 2015年2月15日
放送時間: 日曜20:54 - 23:24
放送分: 150分
回数: 1
テンプレートを表示
テレビ東京開局50周年特別企画として、2015年2月11日 20:54 - 23:18、14日 20:58 - 23:14、15日 20:54 - 23:24の3夜にわたって放送された。視聴率は第1夜が9.0%、第2夜が7.5%、第3夜が9.9%（ビデオリサーチ、関東地区調べ）でいずれも2ケタには届かなかったものの、テレビ東京の高橋雄一社長は「非常によく作られていたし、こうした骨太のドラマをやりきったという点では評価している」と前向きなコメントを出した。
テレビドラマ > キャスト

宮部久蔵 - 向井理
宮部松乃 - 多部未華子/上月左知子（現代）
佐伯健太郎 - 桐谷健太
佐伯慶子 - 広末涼子
長谷川梅男 - 中尾明慶（戦時）/笹野高史（現代）
伊藤寛次 - 千原せいじ（戦時）/津嘉山正種（現代）
井崎源次郎 - 満島真之介（戦時）/近藤正臣（現代）
永井清孝 - 賀来賢人（戦時）/小林克也（現代）
谷川正夫 - 金井勇太（戦時）/石橋蓮司（現代）
武田貴則 - 工藤阿須加（戦時）/山本圭（現代）
景浦介山 - 尾上松也（戦時）/柄本明（現代）
村田保彦 - 渡辺大（戦時）/竜雷太（現代）
小山實 - 石黒英雄
東野二飛曹 - 澤部佑
遠藤一飛曹 - 阿部亮平
酒井一飛曹 - 橋爪遼
大久保整備兵 - 高畑裕太
岡崎二飛曹 - 池田大
今野二飛曹 - 岡﨑育之介
吉田大尉 - 奥野瑛太
斎藤中尉 - 永嶋柊吾
内田飛曹長 - 須田邦裕
司令官（大佐） - 木下隆行
中尉 - 緋田康人
六藤学 - 大和田健介
藤木秀一 - 原田泰造
高山隆司 - 山口馬木也
佐伯清子 - 高畑淳子/渡邉このみ（幼少時）
大石賢一郎 - 中村蒼/伊東四朗（現代）
テレビドラマ > スタッフ

原作：百田尚樹『永遠の0』（太田出版）
脚本：櫻井武晴
監督：佐々木章光
音楽：栗山和樹
主題歌：MISIA「桜ひとひら」（アリオラジャパン）
ヴォカリーズ：幸田浩子（東京二期会）
空撮CGスーパーバイザー：栃林秀
VFX：田中貴志、伊藤あかり、松元遼
資料映像協力：クリエーションファイブ
操演：島尻忠次（ローカスト）
零戦製作：馬場憲治、千住彰、田口敏則
零戦操縦指導：東裕一
殺陣：宇仁貫三、鎌田栄治
スタント：難波和宏
取材協力：水交会、筑波海軍航空隊記念館、戦場体験放映保存の会
資料提供：時代考証学会
ラジコンプロップ協力：日本遠隔制御、斎藤製作所、模型人
医療指導：山本昌督、松島由貴子
軍服監修：渡辺穰
軍事所作指導：越康広、長谷部浩幸
ロケ協力：日本航空学園、千葉県フィルムコミッション、小山町フィルムコミッション、いばらきフィルムコミッション、プロジェクト茨城、栃木県フィルムコミッション、鹿沼市フィルムコミッション、高萩フィルムコミッション、水郷佐原観光協会、福生ロケーションサービス、南伊豆町、富士吉田市、南日本放送　ほか
撮影協力：防衛省、陸上自衛隊、海上自衛隊、航空自衛隊、鹿屋市
VFX・CG：マリンポスト、キュー・テック、Artistree Media
選曲：辻田昇司
音響効果：岩熊展史、水本大介
MA：河野弘貴、兒玉邦宏
技術協力：ビデオフォーカス
照明協力：Kカンパニー
鉄製小道具：大澤製作所
装飾：京映アーツ
スタジオ：東映東京撮影所
制作統括：井澤昌平（テレビ東京）
チーフプロデューサー：岡部紳二（テレビ東京）
プロデューサー：阿部真士（テレビ東京）、佐々木章光、森一弘、近見哲平、石田義一
制作：テレビ東京、テレパック
テレビドラマ > 放送局・放送時間

| 放送対象地域 | 放送局 | 系列 | 放送日・放送時間 (JST) | 備考 |
| --- | --- | --- | --- | --- |
| 関東広域圏 | テレビ東京 | テレビ東京系列 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 制作局 |
| 北海道 | テレビ北海道 | テレビ東京系列 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 愛知県 | テレビ愛知 | テレビ東京系列 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 大阪府 | テレビ大阪 | テレビ東京系列 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 岡山県・香川県 | テレビせとうち | テレビ東京系列 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 福岡県 | TVQ九州放送 | テレビ東京系列 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 岐阜県 | 岐阜放送 | 独立放送局 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 滋賀県 | びわ湖放送 | 独立放送局 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 奈良県 | 奈良テレビ | 独立放送局 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 和歌山県 | テレビ和歌山 | 独立放送局 | 第1話：2015年2月11日 20:54 - 23:18 第2話：2015年2月14日 20:58 - 23:14 第3話：2015年2月15日 20:54 - 23:24 | 同時ネット |
| 鹿児島県 | 南日本放送 | TBS系列 | 第1話：2015年3月11日 19:30 - 21:54 第2話：2015年3月18日 19:30 - 21:51 第3話：2015年3月25日 19:20 -21:51 | 遅れネット |
上記以外に、テレビ東京系列のない地域において、系列外遅れネットを行った局が複数あった。
オーディオブック

2016年8月15日にオーディオブック配信サービス「FeBe」（現・audiobook.jp）から配信開始。配信にあわせ久蔵の妻・松乃役の小芝風花が原作者百田尚樹と対談し、『SCHOOL OF LOCK!』 終戦記念日特別番組に生出演するTOKYO FMとのコラボ企画が行われた。
オーディオブック > キャスト

宮部久蔵 - 櫻井孝宏
佐伯健太郎 - 江口拓也
佐伯慶子 - 豊口めぐみ
大石松乃 - 小芝風花
米水軍兵士 - 杉村憲司
長谷川梅男 - 秋元羊介
伊藤寛次 - 小上裕道
永井清孝 - 金光宣明
井崎源次郎 - 浜田賢二
岡部昌男 - 樫井笙人
武田貴則 - 楠見尚己
谷川正夫 - 園部啓一
景浦介山 - 辻親八
大西保彦 - 側見民雄
大石賢一郎 - 坂巻学
高山隆司 - 松本忍
藤木秀一 - 山本善寿
江村誠一 - 堀総士郎
佐伯清子 - 根本圭子
寺西 - 稲垣拓哉
江村鈴子 - 尾田木美衣
島田加江 - 古城望
祖父 - 糸博
受賞歴 > 小説

大和ネクスト銀行が調査したシニア層（50歳から79歳）が選ぶ、2014年読んでよかった小説ランキング 第1位
受賞歴 > 映画

第16回イタリア ウディネ・ファーイースト映画祭
ゴールデン・マルベリー賞
第33回藤本賞
藤本賞：市川南・畠中達郎・プロデュースチーム
第39回報知映画賞
主演男優賞：岡田准一
第27回日刊スポーツ映画大賞・石原裕次郎賞
作品賞
監督賞：山崎貴（『STAND BY ME ドラえもん』と合わせて受賞）
主演男優賞：岡田准一（『蜩ノ記』と合わせて受賞）
第38回日本アカデミー賞
最優秀作品賞
最優秀監督賞（山崎貴）
優秀脚本賞（山崎貴/林民夫）
最優秀主演男優賞（岡田准一）
最優秀撮影賞（柴崎幸三）
最優秀照明賞（上田なりゆき）
最優秀美術賞（上條安里）
最優秀録音賞（藤本賢一）
最優秀編集賞（宮島竜治）
優秀助演男優賞（三浦春馬）
優秀音楽賞（佐藤直紀）
第69回毎日映画コンクール
録音賞（藤本賢一）
受賞歴 > テレビドラマ

東京ドラマアウォード2015
単発ドラマ部門・優秀賞
2015年日本民間放送連盟賞
テレビドラマ種目 優秀賞
本作に対する反響

出版当時の読者層はわずかな60代以上の男性が占めていたが、口コミで次第に広がり2013年以降は特に10代・20代の読者も増加した。累計販売部数は2013年12月時点で約480万部 その後も映画化・ドラマ化の影響で販売を伸ばし、2014年7月時点では530万部に及ぶ。映画のヒットや作品の普及につれ少なからず反響が起こり、政治思想を問わず読者として安倍晋三をはじめ、政界、芸能界、法曹界、スポーツ界の著名人に取り上げられるとともに、その賛否も話題となった。批判としては「特攻を美化している」「戦争賛美」といったものであり、これについて著者である百田尚樹は自身のTwitter等で、「私は『永遠の0』で特攻を断固否定した」「戦争を肯定したことは一度もない」と述べ、テーマは「生きるということ」と「戦争を風化させないこと」と語っている。「『永遠の0』はつくづく可哀想な作品と思う。文学好きからはラノベとバカにされ、軍事オタクからはパクリと言われ、右翼からは軍の上層部批判（井上成美まで悪し様に書いた）と怒られ、左翼からは戦争賛美と非難され、宮崎駿監督からは捏造となじられ、自虐思想の人たちからは、作者がネトウヨ認定される。まさに全方向から集中砲火」とコメントした。
また、映画化以降特に第二次世界大戦に関連した作品が重なったこともあり、戦争の歴史に対する関心が高まった。2013年6月に宇佐海軍航空隊のあった大分県宇佐市に平和資料館が暫定オープンしたほか、同年12月に作中に登場する茨城県旧筑波海軍航空隊史跡が記念館としてオープンし、4ヵ月で全国から2万6000人が訪れた。福岡県筑前町立大刀洗平和記念館など、特攻隊ゆかりの地や資料館の訪問者も比較的若い世代を中心に大きく増加し、日本海軍の軍人・軍属の人事記録を管理する厚生労働省には、孫など親族から軍人履歴原表の開示を求める申請が増えている。