AI のおかげで Lean…

jrf> AI のおかげで Lean などの定理証明器が話題。昔、私が使っていたころ、(今は無理だけど)すべてを定理証明器で証明するようになるべきではないか…みたいなことを言ったら、別分野(電気系)の教官にすごい反感を持った目でニラまれた。そのころ SPICE とかで論理を自動実装するみたいな触れ込みで現れながら、そこまでうまくいかない…実装経験がものをいうみたいな状況だったというのもあるのだろうけど。…そこから現代、AI が回路実装をサポートする時代になって、すべてを証明する…が不可能でなくなる時代が見えてきた。さすがに私もこんな時代がこんなに早く来るとは思っていなかった。