Lean4の証明をAlectryonで美しく可視化する

概要

この記事では、定理証明支援系Lean4で記述した証明を、ドキュメント生成ツールAlectryonを使って、人間が読みやすい美しいPDFやHTML形式に「可視化」する方法を解説します。

Lean4のコードに適切な形式でコメントを記述することで、証明のロジックと解説を統合した高品質なドキュメントを生成できます。

前提とする環境

本記事では、必要なツールチェイン（Lean4, TeXLive, Alectryon等）がすべて含まれたPodman/Dockerコンテナ環境を使用します。以下のリポジトリで提供されている環境を想定しています。

• lean4

この環境には、PDFを生成するためのDockerfileやスクリプト一式が含まれており、すぐに証明の可視化を試すことができます。

lean4/environments/lean4/Dockerfile

# 必要なパッケージのインストール
RUN apt-get update && apt-get install -y \
    curl \
    git \
    build-essential \
    cmake \
    python3 \
    python3-pip \
    # ... (中略) ...
    # PDF/HTML生成に必要なツール
    texlive-full \
    texlive-lang-japanese \
    latexmk \
    pandoc \
    && rm -rf /var/lib/apt/lists/*

# ... (中略) ...

# Python パッケージのインストール
RUN pip install --upgrade pip && \
    pip install pygments alectryon[lean4]

上記Dockerfileのように、コンテナにはPDFの元となるLaTeXの処理系であるTeXLiveや、ドキュメント変換ツールのpandoc、そしてAlectryon本体が初めからインストールされています。

可視化のためのLean4コードの書き方

Alectryonは、Lean4コード内の特定の形式のコメントを解釈してドキュメントを生成します。

• ファイル全体の解説: /-! ... -/ で囲まれたブロックコメント
• 定理や定義の解説: /-- ... -/ で囲まれたブロックコメント
• セクション見出し: /-! # 見出しレベル1 -/ のように、#でレベルを指定

コード例

以下は、可視化対象のLean4コード (examples/math_proofs/MathProofs.lean) の一部です。

examples/math_proofs/MathProofs.lean

/-! 
# 数学的証明のサンプル

このファイルには、PDF出力用の数学的証明の例が含まれています。
基本的な代数と解析の定理を証明します。

## 目次
1. 自然数の基本性質
2. 実数の性質
3. 指数関数の性質
4. 組み合わせ論的証明
-/

namespace MathProofs

/-! ## 1. 自然数の基本性質 -/ 

/-- **定理 1.1**: すべての自然数 n について、n + 0 = n が成り立つ。 -/
theorem nat_add_zero (n : ℕ) : n + 0 = n := by
  rw [Nat.add_zero]

/-- **定理 1.2**: 加法の交換律が成り立つ。 -/ 
theorem nat_add_comm (m n : ℕ) : m + n = n + m := by
  rw [Nat.add_comm]

-- (以下略)

このように、Leanコード内にMarkdown形式で解説を記述していくことで、コードとドキュメントを一体で管理できます。

PDF/HTMLの生成方法

提供されている環境には、Alectryonによるドキュメント生成を簡単に行うためのシェルスクリプト (generate-pdf.sh / generate-pdf.cmd) が含まれています。

実行コマンド

コンテナ環境内から、以下のコマンドを実行することでPDFおよびHTMLドキュメントが生成されます。

# ./generate-pdf.sh <対象のLeanファイル> [出力先ディレクトリ]
./environments/lean4/generate-pdf.sh examples/math_proofs/MathProofs.lean ./output

スクリプトの内部処理

このスクリプトは、主に以下の処理を自動で行います。

1. Alectryonの実行 (HTML生成): Lean4コードを解析し、まずはHTML形式のドキュメントを生成します。
2. Alectryonの実行 (LaTeX生成): 次に、PDFの元となるLaTeX (.tex) ファイルを生成します。
3. LaTeXの拡張: 生成された.texファイルに、日本語表示や定理環境、ヘッダー/フッターなどの設定を追加した新しいLaTeXファイル (_enhanced.tex) を作成します。
4. PDFへのコンパイル: pdflatexコマンドを複数回実行し、LaTeXファイルから最終的なPDFドキュメントを生成します。

以下は、generate-pdf.cmd内の処理の一部です。

lean4/environments/lean4/generate-pdf.cmd

REM 1. HTMLバージョンを生成
echo %BLUE%[INFO]%NC% HTMLバージョンを生成しています...
alectryon --frontend lean4 "%LEAN_FILE%" --output-directory "%OUTPUT_DIR%" --output "%BASE_NAME%.html"

REM 2. LaTeXバージョンを生成
echo %BLUE%[INFO]%NC% LaTeXバージョンを生成しています...
alectryon --frontend lean4 "%LEAN_FILE%" --backend latex --output-directory "%OUTPUT_DIR%" --output "%BASE_NAME%.tex"

REM 3. PDFを生成
echo %BLUE%[INFO]%NC% PDFを生成しています...
cd /d "%OUTPUT_DIR%"

REM 拡張LaTeXファイルを作成
call :create_enhanced_latex "%BASE_NAME%.tex" "%BASE_NAME%_enhanced.tex"

REM PDFLaTeXでコンパイル
pdflatex -interaction=nonstopmode "%BASE_NAME%_enhanced.tex" >nul 2>&1

生成されるドキュメント

このプロセスにより、出力先ディレクトリ（例：./output）には以下のファイルが生成されます。

• MathProofs.html: ブラウザで閲覧可能なHTML版
• MathProofs.tex: 中間生成物のLaTeXソースファイル
• MathProofs.pdf: 最終成果物であるPDFドキュメント

生成されたPDFでは、Lean4のコード、定理、証明、そして解説コメントが、論文のようにフォーマットされた美しいレイアウトで表示されます。

まとめ

本記事では、Alectryonを用いてLean4の証明を高品質なドキュメントとして可視化する方法を紹介しました。

コード内にドキュメントを記述する「リテラルプログラミング」のアプローチを取ることで、証明の正しさをLean4に保証させつつ、その意図や背景を人間が理解しやすい形で残すことができます。

今回利用した環境のように、Docker/Podmanでツールチェインを固めることで、誰でも簡単に証明の可視化を試すことができます。ぜひご自身のLean4プロジェクトでも活用してみてください。