Scribble at 2026-04-28 16:25:27 Last modified: 2026-04-28 16:28:11

或る意味で妙な表現だが "formalized mathematics" という分野があって（形式化とは無縁の数学があるのだろうか）、昨今は「コンピュータ数学」とか「実験数学」などとも呼ばれることがあるように、コンピュータを使ったアプローチが主流となっている。そこでは、半世紀以上も前から "theorem prover" とか "proof checker" とか "proof assistant" あるいは "automated reasoner" などと呼ばれるものが研究されていて、要するに数学における証明をコンピュータで自動化することを目指している。これは、現実の数学研究において自分自身が研究している理論の自己検証という用途や、自己検証（昔なら「検算」などとも言った）を終えて発表された理論の第三者による追試、いまではたいていジャーナルの査読者が行ったり、arXiv のようなプレ・プリントをホストするサーバに公開された場合は不特定の人々が検証したりする用途に使える。

こうした theorem prover というのは、実際には色々な設計方針で開発されているシステムが色々とあり、もちろん theorem prover そのものを研究対象にしている数学者もいて、専門の雑誌やアンソロジーが毎年のように発行されている。それだけの成果の積み重ねはあるのだが、日本の科学哲学のプロパーで専門に研究している人は皆無と言ってよいだろう（そもそも、それ以前に数学の哲学をガチで研究して業績を残した日本の研究者などいないわけだが・・・まぁ京都付近の人々は西田幾太郎がどうの下村寅太郎がどうしたと、しょーもないナショナリズムで戦前の些末な成果を過大評価するのが習い性だ）。ただし、ここで紹介するMizar については、珍しく日本も国際的なスケールから見て研究拠点の一つとなっていて、「日本 Mizar 学会」という組織まであるのは敬服に値する。丁寧にリソースを探すと、長野大学のサイトには日本語のチュートリアルが残っているので、恐らくは HTTPS も使われていないし、そのうち消える可能性が高いため、興味がある方はいまのうちにダウンロードしておくことをお勧めする。