不満があっても、「言ってもどうせ何も変わりはしない」という諦めがあればあえて不満を口に出すことはないでしょう。願望があっても、「どうせ叶わぬ夢だし、言ったところで虚しくなるだけ」と断念しているなら語ることはないでしょう。
僕は今から不満と願望を書き記します。それは、諦め・断念していた事が、にわかに現実味を帯びてきたからです。不満と願望は、悪態と文句のように受け取られるかも知れませんが、僕の蓄積されたストレスの捌け口というわけではなくて（いや、多少は「蓄積されたストレスの捌け口」だけど）、前向きな予測〈希望的観測〉なんです。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\have}{\Keyword{have } }
\newcommand{\need}{\Keyword{need } }
\newcommand{\letsShow}{\Keyword{lets show } }
\newcommand{\conclude}{\Keyword{conclude } }
\newcommand{\par}{\Keyword{par } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\achieved}{\Keyword{achieved } }
\newcommand{\next}{\Keyword{next } }
`$
内容：
シリーズ・ハブ記事：
現状の証明支援系とタクティク証明
Lean 4のチュートリアル https://leanprover.github.io/theorem_proving_in_lean4/tactics.html からの例題です（わずかに変更しています）。
variable (p q : Prop) theorem sample (hp : p) (hq : q) : p ∧ q ∧ p := by apply And.intro -- (1) exact hp -- (2) apply And.intro -- (3) exact hq -- (4) exact hp -- (5)
これは次のような意味です； p, q が命題〈proposition〉のとき、p と q を仮定すれば、p ∧ q ∧ p を結論できるでしょう。その証明が (1) から (5) までの5ステップで書いてあります（2個のハイフンはコメント開始記号です）。
まず、「こんなこと当たり前だろう。わざわざ証明するようなことかよ、バカバカしい」という感想がありそうです。実際、当たり前なんですが、限られた手順だけを使って仮定から結論を導く練習だと割り切ってください。
限られた手順はタクティクと呼ばれるコマンドで表現されます。番号が付いた5ステップは、タクティク言語によるコマンドラインの並びです。証明（この場合はコマンドラインの並び）を書く場合*1、インフォビューという画面領域に、証明状態が表示され、コマンドを投入するたびに何が起きるかを目視で確認できます。
つまり、証明を書く側は、インフォビューによるフィードバック付きの対話的インタープリタを利用できるわけです。しかし、できあがった証明はコマンドの並びであり、読む側もインフォビュー付きインタープリタを使わない限りは証明状態の状態遷移を追うことができません。もちろん、プロ棋士は将棋盤なしでも将棋が出来るとか、ソロバンの名人はソロバンなしでも計算出来るのと同様な意味で、インタープリタなしで状態遷移を再現できる人はいます。が、そんな特殊なスキルをみんなに要求するの？
「チャットAIで形式証明も自然言語混じりで書ける（はず）」で引用したニプコウ〈Tobias Nipkow〉の言葉を再度引用すると：
引用：（[tactic] は檜山が挿入）
a [tactic] proof is a more or less structured sequence of commands that manipulate an implicit proof state. Thus the proof text is only suitable for the machine; for a human, the proof only comes alive when he can see the state changes caused by the stepwise execution of the commands. Such proofs are like uncommented assembly language programs.
[タクティクによる]証明は、暗黙の証明状態を操作する若干構造化された一連のコマンド並びです。したがって、証明テキストは機械にだけ適したものです。人間にとっては、コマンドのステップごとの実行によって引き起こされる状態遷移を目視で確認できる環境においてのみ、証明が理解可能です。このような証明は、コメントのないアセンブリ言語プログラムのようなものです。
それにも関わらずタクティク証明が主流なのには理由があります。その理由を説明する前に、タクティク証明を人間可読にする方法を紹介します。
人間可読証明
前節のタクティク証明を「自然言語ヒント／キュー前提の形式証明の書き方」で導入・解説した構文／フォーマットで書いてみます。先に、幾つかの注意事項：
- 命題を表す小文字の変数 p, q を大文字にします。つまらない変更ですが、意外と“分かりやすさ”や“受け入れやすさ”に影響します。
- もとの証明にあった命題のラベル（正確には命題の証拠に付けられたラベル）hp, hq は不要なので省略します。自然言語の曖昧な指示語が使えるなら、ラベルはかなり省略できます。
- $`\par/\:\endBlock`$で十分なのですが、分かりやすさのために $`\par/\:\next \:/ \endBlock\par`$ という冗長な書き方をしています。
- $`\achieved`$もなくてもいいものですが、分かりやすさのために使っています。
- もとのタクティク証明に比べて非常に長くなってますが、“ソースコードの短さ”と“人間にとっての分かりやすさ”はトレードオフの関係にあります。冗長さが分かりやすさに寄与するのです。
- Lean 4の場合、$`P \land Q \land P`$ は $`P \land (Q \land P)`$ の省略と定義されています。単に、Lean 4の約束はそうだ、というだけのことです。
- ブロック構造のインデントは律儀にはやってません。
$`\letsShow \text{sample} : P,\, Q \to P \land Q \land P\\
\need P \land (Q \land P)\\
\uparrow \text{論理ANDを分解する -- (1)}\\
\need P,\, Q \land P\\
\par\\
\quad \letsShow P,\, Q \to P\\
\quad \need P\\
\quad \uparrow \text{仮定にある -- (2)}\\
\quad \Box\\
\quad \conclude P,\, Q \to P\\
\next\\
\quad \letsShow P,\, Q \to Q \land P\\
\quad \uparrow \text{論理ANDを分解する -- (3)}\\
\quad \need Q,\, P\\
\quad \par\\
\qquad \letsShow P,\, Q \to Q\\
\qquad \need Q\\
\qquad \uparrow \text{仮定にある -- (4)}\\
\qquad \Box\\
\qquad \conclude P,\, Q \to Q\\
\quad \next\\
\qquad \letsShow P,\, Q \to P\\
\qquad \need P\\
\qquad \uparrow \text{仮定にある -- (5)}\\
\qquad \Box\\
\qquad \conclude P,\, Q \to P\\
\quad \endBlock \par \\
\quad \achieved P,\, Q \to Q \land P\\
\endBlock \par \\
\achieved P,\, Q \to P \land (Q \land P)\\
\conclude
`$
フォワード方向（仮定から結論への方向）の証明に書き換えると：
$`\letsShow \text{sample} : P,\, Q \to P \land Q \land P\\
\bullet P, \, Q \land P \text{ を証明してから、論理ANDで組み合わせる}\\
\par\\
\quad \letsShow P,\, Q \to P\\
\quad \downarrow \text{仮定を再掲}\\
\quad \have P,\, Q\\
\quad \downarrow \text{仮定から}\\
\quad \have P\\
\quad \conclude P,\, Q \to P\\
\next\\
\quad \letsShow P,\, Q \to Q\land P\\
\quad \downarrow \text{仮定を再掲}\\
\quad \have P,\, Q\\
\quad \downarrow \text{順序は関係ないから}\\
\quad \have Q,\, P\\
\quad \downarrow \text{論理ANDの導入規則から}\\
\quad \have Q \land P\\
\quad \conclude P,\, Q \to Q\land P\\
\endBlock\\
\achieved P,\, Q \to P\land (Q \land P)\\
\conclude
`$
これでだいぶ分かりやすくなったと思います。しかし、一番分かりやすいのはテキスト表現ではなくて絵図〈picture | diagram〉表現です。今の証明は次のストリング図で表現できます*2。
水色のノードの意味は次のとおりです。
- copy : (P, Q) → (P, Q), (P, Q) -- ワイヤーの束のコピー、2本から4本に
- proj1 : (P, Q) → P -- 左のワイヤーだけを取る（右のワイヤーを切り落とす）第一射影
- swap : (P, Q) → (Q, P) -- 左右のワイヤーを入れ替えるスワップ
- AND : (Q, P) → Q∧P -- 論理AND導入
- AND : (P, Q∧P) → P∧(Q∧P) -- 論理AND導入
一目瞭然とはこのことです。人類がテキスト言語から絵図言語に乗り換えられないのは、文字・活字・組版文化の歴史的惰性だと思いますが、このような歴史的惰性を変化させるのは5年10年では無理でしょう（「「コミュニケーションの多次元化」という革命に立ち会っているのだと思う」参照）。絵図的には簡単なことを、テキストに引き写しては難読化させるという不毛な作業を、まだしばらくは続けることになりそうです*3。
なぜタクティク証明が主流なのか
タクティク証明の源流は1979年のEdinburgh LCF〈Logic for Computable Functions〉だと言われています。しかし、それよりも早い1973年には、人間可読な宣言的記述方式のMizarが登場しています。人間可読な形式よりタクティクが好まれた理由は何でしょうか？ 真面目に調査したわけでも確たる証拠があるわけでもありませんが、おそらく：
- REPL〈Read-Eval-Print Loop〉方式のインタープリタと相性が良かった。ひとつのコマンドに対する応答がすぐ返るので、長いソースコードを非対話的に書くより楽。
- バックワード・リーズニングが機械的アルゴリズムとして実装しやすかった。（Prologなどの論理型言語も、バックワード・リーズニングを実装しています。）
- タクティク・インタープリタ上で走るプログラムを書くことにより、自動証明が可能となる。
- 証明ソースコードが短くなる。
これらの理由は現在の証明ソフトウェアにも通用します。総論として言えば：
- 人間の都合よりは機械〈ソフトウェア〉の都合を優先させている。人間側の学習と労力のコストは軽視されている。
- 証明を書く側が楽になる手段は（多少は）提供されているが、証明をソフトウェアなしで読むことは考慮されてない。
ユーザーインターフェースも貧弱です。
- Title: Coqoon: An IDE for interactive proof development in Coq
- Authors: Alexander Faithfull, Jesper Bengtson, Enrico Tassi, and Carst Tankink
- Date: 2016
- URL: https://hal.inria.fr/hal-01242295/document
引用：
User interfaces for interactive proof assistants have always lagged behind those for mainstream programming languages.
対話型証明支援系のユーザーインターフェースは、主流のプログラミング言語のユーザーインターフェイスに常に遅れをとっています。
なぜこんな事態になっているかと言えば、証明ソフトウェアの設計・実装が最高難度のチャレンジだからでしょう。本体の証明エンジンを作るのがとんでもなく難しいので「使い勝手」だの「人間可読性」とか言ってられない、手が回らないという事情かと。設計者・開発者がそう思っているわけではなくても、証明ソフトウェア・コミュニティの文化として「ユーザー側に負担がかかるのは致し方ない」という発想が組み込まれているようです。
Mizar方式にするだけではダメ
「Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか」より引用：
ここ数年のウェンツェルの主張を追ってみると、Isabelleの世界を広げようと尽力しているのが分かります。証明支援系の利用が広がらないネックは、「難読な証明記述言語と貧弱なユーザーインターフェースだ」との認識のもと、Isar（Isabelleの宣言的証明記述言語）とIsabelle/jEditにより障壁を取り除く戦略のようです。
ウェンツェル〈Makarius Wenzel〉は、Isabelleの主要な開発者であり、Isabelleの機能拡張を精力的に主導しています。ウェンツェルの言う「難読な証明記述言語と貧弱なユーザーインターフェースがネックだ」とは前節で指摘した内容そのものです。彼は、Mizar風の非タクティク言語Isabelle/Isarとフロントエンド・フレームワークPIDEにより、「ユーザー側に負担がかかるのは致し方ない」を打破しようとしています。
ウェンツェルの活動には拍手喝采をおくりますが、Isabelle/Isar＋PIDEなら誰でも使えるのか？ というと、答は「否」です。
「証明検証系Mizarのジレンマと証明系の村」より引用：
ウェンツェルは、Isabelle/Isar（言語）とIsabelle/PIDE（フロントエンド・ソフトウェア）が教育に有効だろうと主張しているし、その方向で頑張ってもいるようです。しかし、「ちょっと無理なんじゃないか」と僕は思います。Isabelleは（そしてもちろんCoqも）無駄に難しいからです。タクティク言語の難読さは論外ですが、高水準なIsarにしても、その意味モデルや論理的概念が難しいので、教育に使うための事前の教育で息切れするでしょう。
Isabelle/Isar＋PIDEがタクティク証明やコマンド・インタープリタより相対的に容易なのは確かですが、問題は「相対的に」ではなくて、「絶対的な」学習負担・操作負担なんです。僕には、「教育に使うための事前の教育」が元が取れる努力だとは思えないのですよね。コスパ悪すぎる。
使いものにならない？
以上に述べたような事情で、5年10年のレンジで見れば、証明ソフトウェアが普及することはないだろうと思っていました。一般の人（特別な資質と情熱の持ち主ではない！）が、教育目的や、ソフトウェア検証の目的で証明ソフトウェアを使うのは無理だ、と。
しかし、最近の幾つかの記事で指摘したように、にわかに事情が変わってきました。
自然言語の解釈と会話ができるAIの登場により、証明ソフトウェアの難点が解消される見込みが出てきました。この変化は、キャラクタUIからグラフィカルUIへの変化と少し似ています。ウィンドウシステムの登場により、ターミナル／コンソールのシェルに対して呪文のようなコマンドを打ち込んでは操作していたコンピュータが、直感的なマウス操作でもいじれるようになりました。
あるいは、プログラミングにおける高級言語の登場にも似てるかも知れません。機械語／アセンブラ言語は効率的ですが、人間向きとは言えません。機械語／アセンブラ言語しかなかったら、プログラミングは（一部の好き者以外には）難しくつらいものだったでしょう。
とは言いながら、コマンドシェルを好む人はいるし（僕も好きです）、GUIよりコマンドが効率的なときはあります。もちろんアセンブラ言語の使い手は今でも存在するし、リスペクトの対象です。自然言語に包まれた甘口の証明記述言語が普及しても、カチカチの形式言語の用途が消滅することはないでしょう。
「自然言語証明から形式証明を抽出できる（はず）」の最後に書いたように、証明の自動生成もけっこう期待できそう。証明自動生成においては「AIが間違えたり嘘を言ったりしないか？」という懸念は不要です。人間でもAIでも、証明ソフトウェアでチェックされるので、間違い・嘘はすぐに検出されます。
2年後くらいには、甘口の証明記述言語と良好な（できればピクトリアルな）ユーザーインターフェースが使えるようになっていると期待〈希望〉してます。そうなれば、「証明ソフトウェアは使いものにならない」という前言は撤回します。
*1:書くときに、Lean 4の言語サーバーと、VSCodeのようなクライアントが必要です。
*2:逆に、ストリング図をテキストに書き写す方法は「ストリング図のテキスト化」「ストリング図のテキスト化は何が大変か？」「ストリング図のテキスト化： ボックス＆ポート方式」にあります。
*3:自然言語AI技術も、テキスト言語にもとづいているので、“一目瞭然な絵図の世界”への転換には役立ちません。ただし、画像解釈・生成／動画〈ムービー〉解釈・生成の技術が進展すれば、非テキスト言語の世界が拓ける端緒になるかも知れません。
