「チャットAIで形式証明も自然言語混じりで書ける（はず）」において、形式証明のなかに自然言語によるヒント／キューが書けたら証明記述作業が格段に楽になる、と書きました。この方法を少し推し進めれば、書籍や論文の自然言語証明から形式証明を生成できるようになるでしょう。
内容：
シリーズ・ハブ記事：
自然言語だけの形式証明
「チャットAIで形式証明も自然言語混じりで書ける（はず）」の事例を再掲します。繰り返し説明はしませんが、自然言語〈日本語〉によるヒント／キューを含む形式証明です。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\for}{\Keyword{for } }
\newcommand{\letsShow}{\Keyword{lets show } }
\newcommand{\conclude}{\Keyword{conclude } }
\newcommand{\assume}{\Keyword{assume } }
\newcommand{\consider}{\Keyword{consider } }
\newcommand{\st}{\Keyword{ st } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\Imp}{ \Rightarrow }`$
$`\for a, b, c \in {\bf N}\\
\letsShow \exists z\in {\bf N}. a + z = b,\; \exists z\in {\bf N}. b + z = c \to\\
\quad \exists z\in {\bf N}. a + z = c\\
\downarrow \text{仮定を再掲}\\
\exists z\in {\bf N}. a + z = b,\; \exists z\in {\bf N}. b + z = c\\
\bullet \text{この2つの存在命題について考えよう}\\
\consider x\in {\bf N} \st a + x = b,\; y \in {\bf N} \st b + y = c\\
\quad \downarrow \text{上の条件の等式から}\\
\quad a + (x + y) = c\\
\quad \downarrow \text{上の } x + y \text{ を } z \text{ として存在限量子で束縛する}\\
\quad \exists z \in {\bf N}. a + z = c\\
\endBlock\\
\bullet \text{以上により}\\
\conclude \exists z\in {\bf N}. a + z = b,\; \exists z\in {\bf N}. b + z = c \to\\
\quad \exists z\in {\bf N}. a + z = c
`$
この事例では、全体の構造や流れは人工的なキーワード（緑色）で示しています。しかし、全体の構造や流れも自然言語で書けます。例えば、証明開始の合図と締めの言葉は次のように書けます。
これから「∃z∈N. a + z = b 、∃z∈N. b + z = c ならば ∃z∈N. a + z = c」を示そう。
‥‥
‥‥
「∃z∈N. a + z = b 、∃z∈N. b + z = c ならば ∃z∈N. a + z = c」が結論できた。
まったく好き勝手な言い回しでは困りますが、統制・制限された自然言語〈controlled natural language〉を使えば、証明開始と終了をソフトウェアが検出することは可能でしょう。
他の部分も自然言語で書いてみます
a, b, c を任意の自然数とする。
これから「∃z∈N. a + z = b 、∃z∈N. b + z = c ならば ∃z∈N. a + z = c」を示そう。
仮定を再掲する。
∃z∈N. a + z = b 、∃z∈N. b + z = c
この2つの存在命題について考えよう。
x は a + x = b である自然数、y は b + y = c である自然数とする。
これらは存在命題から存在が保証される。
上の x, y に関する条件の等式から
a + (x + y) = c
は言える。
上の x + y を z として存在限量子で束縛すると
∃z∈N. a + z = c
が言える。
以上により
「∃z∈N. a + z = b 、∃z∈N. b + z = c ならば ∃z∈N. a + z = c」が結論できた。
既存の証明から形式証明の抽出
十分に明確な日本語で書いてあれば、自然言語証明から形式証明を抽出できるでしょう。うまくいかない場合もあるでしょうが、そのときは日本語のほうを修正・校正することによって抽出可能にすることができます。
既存の書籍や論文の自然言語証明を人間が手で形式証明に変換するのは、労力的に現実的ではありません。しかし、日本語の修正・校正ならば、ずっと楽な作業です。100%自然言語ではなくて、構造や流れを明示するマークアップを挿入するのも手〈ひとつの手段〉です。
このような方法で、書籍や論文から形式証明を抽出して蓄積すれば、それなりの規模の証明コーパスが構築できます。その証明コーパスから学習した大規模言語モデルは、けっこう賢くなるんじゃないのかな*1。
「チャットAIで形式証明も自然言語混じりで書ける（はず）」において、
実感としては、石頭で物分かりが悪いソフトウェアが証明を理解する支援を人間がしているようです。ソフトウェアは“証明支援される系”です。
と書きましたが、トレーニングされた賢いバックエンドに、良好なUIが備われば、ほんとうに人間を支援してくれる証明ソフトウェアが実現できるでしょう。
*1:チェスや将棋のように、ある観点からは人間を凌駕するかも知れません。
