vibeformalizing
シンプルに自分の数学とコーディング能力の欠如かもしれないけど，紙とペンによる証明で通るとわかっていたとしても実際に形式証明に落とし込む際には全然うまくいかないことはあって，「迂遠だけどもこうすればコードに出来そう」みたいな別ルートを考えるのはノウハウが別に必要だと思う． おそらくAI/LLM側は多分Mathlibなりあらゆる分野の"形式証明の"書き方を蓄積した結果，現実的に可能なコードに落とし込む提案をするのが自分よりも遥かに上手い，という肌感がある．その別提案と元の主張・議論の流れとを吟味する作業が私の脳に外注され続けている． Lean ⊣⊢ "普通の数学"という図式が果たして本当に成り立つか否かや無矛盾性などの議論は一旦保留するにせよ、形式証明を書くことを通常のソフトウェア開発だと思ってテスト駆動開発の観点を導入してみる。するとここでいうテストは当に数学側からタダで降ってくるし、更にそれは100%論理的に妥当→
という意味で、逆にこれほどまでにAI/LLMに向いている領域もないのではないか．．．つまりハーネス自体を我々人間側が適宜調整する必要は特になくて、究極的には、ゴールさえ置いておけば後は野となれということが出来る世界が来たらいいねーみたいなことを、話した。
純粋に数学をやっている人と定理証明支援系について話して簡単なデモンストレーションをしたら「無限的な構造を持つ概念や単純には（コンピュータプログラムとして）実行不可能に見える概念の定義や証明を計算機上でコードとして書けるのは不思議だ」と言われて逆に新鮮だった
「定理証明支援系はつまるところ究極には、巨大な項書換え系のもう少しリッチな感じで、実際にその定義を実行するといったことは二の次なのですよ」みたいな適当な説明をしたけども、全然知らない人にとってはTPの動作原理や能力についてそもそもよくわかっていない可能性もあるのかと思った
個人的に、人間にとっての定理証明支援系は、数学者の便利かつ高級な電卓・Better TeXのようなものになると良いかなと思っているのだけども、普及の鍵は「大きな定理を示した！」という事実よりも、普通に紙とペンの数学の議論がある程度自然にTPで書けるということを粘り強く強調することなのか．．．
AI・コーディングエージェントが寄越してくる形式証明の一番の問題は、彼ら（私は彼らに一定の人格を認めています）の認識能力が人間のそれより遥かに上なので、全部愚直に書くみたいなことを平気でしてくるという問題があり、シンプルに！ということが全然出来てない
Hilbertの第24問題ではないけども、2027年ごろにはAI/LLMはある程度難題を証明出来ると思うが、最終的に寄越してくる形式証明のシンプルさが肝心になるのではという気がする．．．というのを今AIが寄越してきた証明を必死に解体する作業に追われながら思っている