（上記ツイートは3年前くらいのもの）

半年くらい藻搔いた結果の答え合わせとして．

新しいことをしようとしている際は， 出来るだけ早々な一般化は避け， 多少冗長になるとしてもコアの機能のみを素直に利用して外部依存は減らした方が， 結果的には近道になる（場合がある）ことがわかった．

背景

Isabelle は ``定理証明支援系’’ なるもので， 「証明の正しさ」をコンピュータが機械的に保証するためのツールである．

人間はどうしても間違えるし， 正しかったとしても曖昧さが残る1．

しかし，定理証明支援系を使って証明できれば， 自分の証明が絶対に正しいことを第三者も含めて確信できる2．

ただ， 「証明の正しさ」をコンピュータが機械的に保証するということは， 逆にいうと，コンピュータが機械的に正しさが保証できるようなレベルまで証明を書き下してやらないといけないので， かなり大変だったりする．

最近 (2026年3月現在) は 「生成 AI が特に定理証明支援系 Lean を用いた形式証明を自動的に行う」 といった研究がかなり話題になっているようで， もしかしたらすでに or 近い将来生成 AI で完全自動化できるのかもしれないが， 今の所は普通のコードと違ってチャッピーがサラッと書いてくれるという感じでは全然ない．

というかチャッピーはあんまり使い物にならなかった3．

本題

Isabelle/HOL (HOL はライブラリみたいなもの) を用いて自ら提案する型システム4の健全性の証明を行った．

最終的には 5,000 行程度と，超大規模というつもりはないが， 小規模というにはかなりの規模のものになった．

正直に言って，かなり苦戦した．

折角なので， 今回の Isabelle/HOL での形式化などを通して， 今回得た自分なりの学びをまとめておく．

あくまで個人的な知見であって， 万人に適用可能ではないとは思うが．

学び

まずは動くものを拾ってきて， それを可能な限り簡単化するところから始める．

まずは普通の Simply Typed Lambda Calculus (単純型付きラムダ計算) の健全性の証明のコードを拾ってきた．

意外と，値呼びのものがなく，かなり書き直すことにはなった（最終的なコード）．

合流性の証明等，今回の目的には不要な部分が大量にあったので， 今回の本筋に影響しない補題を削除することが最初の仕事になった．

→ コードに対する目視だけでやるのはあまりに大変だったので， 定理の依存関係を可視化するツールを作った．

https://github.com/sano-jin/isabelle-deps

予め動くものを用意できていると， うまくいかないときの原因の絞り込みがしやすい．

というか，そうでもしないと，できない．

解く前から定義・問題を一般化しない．

つい一般化したくなるが，堪える．

一般化した方が解きやすければ，一般化しても良い． （が，そのようなことはほとんどなかった）

解けてから， 使っていない前提条件は省いておく， くらいのことはしておく． 逆にそれ以上の一般化に無理に時間を使わない （結局ほぼ改善できない，ということが何度もあった）．

多少冗長になったとしても，外部依存は出来るだけ減らして，コアの機能のみを用いる．

コア機能以外を利用していると， うまくいかない際の問題の特定が難しくなる．

具体的には， 例えば， Nominal Isabelle というライブラリを利用しようとしていたのだが， 諸般の事情により断念した．

Nominal Isabelle は美しいライブラリ5で， 是非使いたいものだが．．．

うまくいかない際は，問題の切り分けを地道に行う．

特に，ChatGPT の言うことは信用しない．

  • 「2 turns 以上使ってはいけない」みたいにするのが良いのかもしれない．
  • つい「あともうちょっと，あともうちょっと．．．」という感じで何度も使いたくなるが．．．
  • 精神力が試される．．．

心を無にして，原因と無関係と思しきコードを削除し続けて，最小コード例を作る．

どうしてもうまくいかないときは，一旦寝て，外に出て頭の中で解いてみる．

そもそも大筋が悪いことが結構ある．

もっとテクニカルな知見も色々とあるにはあるが， ハイレベルな話としては概ねこんな感じ．

ポエム

上記はどれもまぁ当たり前というか， 泥臭くてあまり美しくはなく， 個人的には正直かなり残念ではある．．．

特に，今回は Nominal Isabelle を捨てて de Bruijn Index でゴリ押ししたのだが， これはかなり無念だった．

とはいえ，エンジニアリングの本質は意外とこんなものなのかもしれないなと少し思った．

本物の数学者（？）も，実は意外とこんな感じなのかもなとも思った．

最終結果は美しく一般化された理論かもしれないが， その裏には泥臭い試行があるのかな，と．

知らんけど．

などと言いつつ，私は未熟な人間なので？， つい解く前から一般化したり格好良い武器（外部ライブラリ等）を使いたくなったりしてしまう．

以上

  1. というのは私に関しては半分以上言い訳で， 本質的問題としては私の能力の低さに起因するところがある． ↩

  2. 宇宙線の影響や定理証明支援系自体のバグなどによって， 間違った命題を「証明」できてしまう可能性は原理的にはゼロではないかもしれないが， 現実的にはゼロと言って良いはず． ↩

  3. しかし生成 AI の進歩は凄まじいので，正直もう， これからどうなるのかではなくて， 今どうなのかすら全然分からない． 恐怖を感じている． ↩

  4. この論文 の Section 3. ↩

  5. Nominal Rewriting に関する研究について断片的に触れた際には， 浅学なため全く理解できず，難解で遠い世界だなぁという印象を抱いていた． しかしながら，実際に Nominal Isabelle を用いて綺麗に証明ができることを確認し， その応用の美しさに非常に強い印象を受けた． 当該研究成果がどの程度この仕組みに寄与しているのか全然知らないので， 恐らくは全然見当違いのことを言っているのだろうけど． ↩