Agda で算術の基本定理を証明する
この記事では、関数型プログラミング言語であり証明支援系でもある Agda を用いて、算術の基本定理（任意の整数は素数の積に一意に分解できる）を形式化し証明する方法を解説する。ラムダ計算の枠組みで構成された Agda の型システムを活用しながら、帰納法や補題を用いた厳密な証明の実装例が示されている。
背景メモ
• この記事は「算術の基本定理」（任意の自然数が素数の積として一意に表せること）を、依存型定理証明支援系 **Agda** を使って形式的に証明する内容。
• Agda は関数型言語 Haskell に似た構文を持つプログラミング言語だが、通常のプログラミングに加えて数学の定理を「型」として記述し、その証明をプログラムとして書くことができる。バージョン 2.7.0.1 を想定。
• 記事では、Agda の標準ライブラリではなく、筆者が教育用に整備したライブラリ **「Little Typer」**（LF スタイルの推論規則を模したもの）を使用。このライブラリは標準ライブラリより名前的に簡潔で、Agda 入門者にも追いやすい構成になっている。
• 算術の基本定理は整数論の根幹であり、その完全な機械検証（証明の全ステップをコンピュータにチェックさせること）は、定理証明コミュニティにおける古典的な演習問題かつ達成目標。
• 本記事はコード全文を含む literate Agda ファイル（.lagda）形式で書かれており、読者は実際に Agda でロードして実行・検証できる。