Scribble at 2024-04-06 12:11:44 Last modified: 2024-04-06 12:17:26
Terence Tao @tao@mathstodon.xyz / The most recent issue of the Bulletin of the American Mathematical Society, available at https://www.ams.org/journals/bull/2024-61-02/ , is largely devoted to the topic "will machines change mathematics?", with a wide variety of viewpoints from mathematicians (I understand that the following issue will also contain contributions from other disciplines that can inform the sociology of mathematics.) I found the articles to be an interesting read (though it does make my own forthcoming Notices article at https://terrytao.files.wordpress.com/2024/03/machine-assisted-proof-notices.pdf somewhat redundant, as much of what I write is covered by the union of these articles). It is also notable that many of these articles were submitted nearly a year ago and are thus somewhat overtaken by events - this space is developing quickly!
マストドンも、なんだかメディアの記事ばかりが投稿されるなぁと、巡回先から外そうかと思っていたのだけれど、こうして実際に Tao のような人物の投稿があると見逃せないという気分が残る。
computer-aided (or computer-assisted) proof については、もちろん automated thorem prover (or solver) を幾つか試したことはあるけれど、正直なところ科学哲学の研究でこれらを使わないといけないほどのケースってないんだよね。だから、純粋にこの話題そのものに興味があるわけでもなければ、別に科学哲学者だからといって Prolog や LISP を勉強して扱えるようにならないといけないってわけでもない。
それどころか計算についても、たとえば僕の修士論文で掲載した簡単な確率論の式の展開などと比べてすら、それよりも長くて込み入った計算を科学哲学の論文で見たことなんか殆どない。量子論を語っていても、本当にこの人たちってヒルベルト空間どころか線形代数とかテンソルとか理解してるのかなと思わざるを得ないような人が幾らでもいるわけで、もちろんそういうところに議論の本質があるわけではないというのも確かなのだろう。ただ、そうは言っても基本的な知識として押さえておいてもいいよっていう分野だとは思う。
そして、これは科学哲学だけではなくシステム開発の分野でも言えることだ。特に、コンピュータを使った証明に関連する基礎的な知識として、たとえばカリー＝ハワードの同型対応なんていう概念を聞いたこともないなんてのがプログラマを名乗ってるのは、いくら東アジアの辺境国家とは言っても酷すぎるという気がする。とにかく、この国の IT やウェブの技術者は情報科学やデジタル通信理論の素養がなさすぎて呆れる。なんだかんだ言っても、いまどきはイノベーションって学識があってのことだからね。家のガレージでパソコンの通販やってりゃ素晴らしいシステムを思いついたり上場企業の経営者になれると思ったら大間違いだ。