いいねぇ。非常に良い。これはものすごく，「証明がはかどる」気がしてきた。
この実験により，ChatGPTを使って「厳密な数学の議論」ができる可能性が拓けた。
例えば，
Write the proof of the Meyer-Vietris sequence in Coq's code.
とやると，以下のコードが表示される。
("見たまま"表記で記事書くんじゃなかった。次回からはてな表記にしよう・・・)
Coqコードを生成することにすれば，有名な定理は名前だけ指定すれば「検証可能な」証明が出てくるということだ。
とすると，あとはマイナーな補題や命題をどう扱うか。この辺りからCoqに対する具体的な知識が必要になってくるかもしれない。これは，適当な本の1章を使ってまるまる実験するなどしてみたい。こりゃワクワクするねー。
バキバキのProof Engineerにとってはこんな証明支援には「腑抜けがっ」と言いたいところかもしれないが，証明支援系の使い勝手を劇的に変えてくれる可能性がある点だけは大目に見ていただきたいところ。
