Coq、Agda、Idris、Lean などの証明支援系は、型付きラムダ計算と帰納的構成計算に基いています。ベースに強力な型システムを持ったプログラミング言語があり、型システムの型チェッカーを利用して証明チェックも行います。証明記述と証明チェックは、ラムダ計算のなかに埋め込まれていると言えます。
したがって、最も素朴で素直な証明記述構文・フォーマットはラムダ項です。人間が、証明をラムダ項で記述すれば、特別な道具なしにラムダ式パーサー／型チェッカーに証明を渡せます。この方法を、証明の直接記述〈direct description〉と呼びましょう。直接記述で書かれた“証明を表すラムダ項”を証明項〈proof term〉または証明オブジェクト〈proof object〉と呼びます。
証明が長くなってくると、証明の直接記述は困難になると言われています。以下は、素因数分解の一意性（たぶん）の証明項の例です。
このテの証明項は、「どうだ、読みにくいだろう」という文脈で提示されますが、改行もインデントもなく、キーワードやシンタックスシュガーも一切使わない生々しいデータを出すのはフェアではない気がします。しかしそれでも、読みにくいのは確か。
直接記述の代替手段として考案された*2のがタクティクによる記述です。しかし、「証明支援系がダメだった理由と、AIでブーストする理由」で述べたように、タクティクはタクティク・インタープリタの仮想機械語で、これまた人間が読めるシロモノではありません。
つまり結局、直接記述もタクティク記述も人間可読ではないのです。この事態に対して我々ができることは：
- 人間が読めるシロモノではない機械可読証明を、根性と時間を投入して頑張って読み書きする。
- ラムダ計算／型理論ベースを捨てて、一階述語論理／高階述語論理などをベースにした証明ソフトウェアに乗り換える。
- ラムダ計算／型理論ベースは維持して、シンタックスシュガーやコンパイル〈トランスパイル〉技術で難読性を緩和する。
一番は身も蓋もない解決策だし、「根性と時間」を持ち出す時点で解決策とも呼べません。二番は考慮に値する案ですが、現在主流で広く利用可能な証明ソフトウェアがラムダ計算／型理論ベースであるという現実的な事情から採用が難しいでしょう。となると、三番しか残っていません。
今でも、より読み書きしやすい表層構文をコンパイル（あるいはマクロ展開）することは行われています。しかし、それで劇的に可読性が向上するかというと、「多少甘口にしたところで所詮は機械向け言語」というそしりは否めないところです。
なにやってもうまくいかない状況で、機械が人間言語〈自然言語〉を理解できる（かも）という知らせは朗報です。証明の自然言語記述という第三の方法が出現します。以下の一連の記事は、この状況変化に触発されて書いたものです。
100%自然言語だと曖昧性に悩まされるので、“いい感じ”のハイブリッド言語が望まれます。ハイブリッド言語を、自然言語混じり形式言語〈formal-natural mixed language〉または半形式言語〈semi-formal language〉と呼びましょう。
いずれは自然言語混じり形式言語を証明ソフトウェアが解釈してくれるでしょうが、ごく近い未来では次の翻訳を行うコンパイラが必要です。
- 自然言語混じり形式言語 → 証明ソフトウェアのネイティブ言語
次の翻訳もあり得ます。
- 自然言語混じり形式言語 → 完全な自然言語
完全な自然言語にすることに意味があるのか？ ちょっと疑問を感じますが、記号的表現があるだけでイヤ！ という人にはありがたいかも知れません。
僕が欲しい翻訳〈変換〉は：
- 自然言語混じり形式言語 → グラフィカルな表現
グラフィカル〈ピクトリアル〉な表現が最も分かりやすいと思うからです。「証明支援系がダメだった理由と、AIでブーストする理由 // 人間可読証明」を読んでもらえれば、テキスト表現にすることが、構造の多次元性を潰して難読化することだと理解できると思います。文字・組版技術やコンピュータ・プログラミング言語技術の制約が、人間の直感的理解を阻害しているのです。
ただし、きれいで見やすいグラフィカルな表現の生成は難しいです。Graphvizのdot言語のような高水準グラフィックス記述言語への変換は容易でしょうが、望ましい外観・レイアウトが得られるとは思えません。ストリング図の、満足すべき自動レイアウト・アルゴリズムは存在しないようです（僕が知らないだけかも知れませんが）。
自然言語混じり形式言語をソース言語として採用できれば、それはブレークスルーとなるでしょう。自然言語混じり形式言語からの多方向翻訳により、色々な目的に沿った記述・表現形式が得られますから。
シリーズ・ハブ記事：
