日曜日に， コンピュータを用いて正しい証明を行う定理証明支援系 Lean の勉強会 （数学系のための Lean 勉強会） にオンラインで参加してきました． 楽しかったです．

X/Twitter で見つけて，悩んだのですが，エイヤと参加してしまいました． 私は趣味で休日 Isabelle（Lean とは異なりますが，定理証明支援系です）を書いたりしていましたが， 最近モチベーションと体力が維持できず数ヶ月以上離れてしまったのと， 独学だと行き詰まりを感じていたので，願ったり叶ったりでした．

定理証明支援系とは

定理証明支援系というのは， コンピュータ上で証明を行うためのソフトウェアです． 定理証明支援系では， apply などのコマンド (tactics) を使って， 用意された推論規則を何度も適用することで， 厳密な証明を行います． 用意された推論規則というのは例えば， 「新たな仮定の導入」や「（新たに導入した仮定を含む）定理の適用」だったり， 「論理積（かつ，\(\land\)）を用いた命題を分解して， それぞれの場合について個別に証明できるようにする」とかです．

定理証明支援系を用いることの利点は色々あると思いますが， 例えば以下のようなものがあると思います．

  1. 証明の正しさをコンピュータが保証してくれる．

    定理証明支援系では， 基本的には「正しさ」が保証された推論規則しか使えません． 変なことを書くとコンピュータに怒られます． 例えば，間違っている部分の下側に赤い波線が出てきます． 人間が手で書く証明はどこかで間違える可能性が非常に高い ので， これはとても有用です．

    ここで， 定理証明支援系が証明の際に用いる推論規則の正しさは， 「型理論」という数学的な根拠に基づいており 1， その無矛盾性が ZFC 上（通常の数学）で証明されています． もし定理証明支援系の推論規則で何も仮定せず矛盾が導けるなら， 「通常の数学」の世界も矛盾すると言うことです．

    もちろん定理証明支援系の実装にバグがいたりする可能性は否定できませんし， そもそも「通常の数学」が正しいのかの保証も人類にはできない （ゲーデルの不完全定理） ので， 定理証明支援系での証明に成功したからと言って 「絶対に正しい」と言い切ることはできませんが， 少なくとも紙での証明よりは遥かに厳密で正しい証明ができます．

  2. ある程度は証明が自動的にできる．

    定理証明支援系によっては，ある程度は「自動証明」ができます． これは次にどの推論規則を適用するかをある程度自動的に探してくれる比較的単純なものから， すでに証明されている定理を検索してきて上手く適用したり， SMT Solver というものを裏で走らせて定理全体が恒真であることを自動的に証明（しようと）するより強力なものまで， 色々あります．

    そもそも「全ての定理を自動的に証明する」 ようなアルゴリズムは存在しない（ことが証明されている）ので， 基本的にはボタンを押すだけで全部自動的にできると言うわけではなく， 出力結果を見ながら次にどうするかを逐一考えることになりますが， 自明度の高い定理では自動証明を繰り返すだけで証明が全て完了したりすることも多いです． 特に，場合分けが面倒なだけで証明自体は自明なものなどでは， 紙に手で書くよりも遥かに楽になります．

  3. 証明の再利用がしやすい．

    紙での証明において，過去の証明を活用しようとすると， 様々な壁が立ちはだかることが多いと思います． 具体的には，「せっかく証明を書いた紙を失くす（捨てちゃったりとか）」とか， 「何を仮定してその定理を示したのか， かなり良く見ないと分からない（本人も忘れている）ために， 現在示したい定理においてそれが補題として使えるのか分からない」とか． 個人レベルで色々証明を溜め込むのではなく， 広く世界で共有しようとするともっと大変です．

    定理証明支援系では， 厳密な証明をデジタルな形で共有した上で， それらをすぐに自分の証明にも活用することができます． デジタルな形でバージョン管理などもされながら共有されているので， 紛失したりすることは（ほぼ）ありません． また定理中で用いている仮定を満たしているかなどについて， その定理を適用するタイミングでコンピュータが自動的に確かめてくれるために， 補助定理の証明の中身を詳しく追いかけたりせずに自分が証明したい定理に集中できます．

最近では， LLM（大規模言語モデル）と組み合わせて証明の更なる自動化を試みるような研究もあるようです． 定理証明支援系は基本的には「自明度の高い定理」を「厳密に」行うためのソフトウェアだと思っていて， 今我々（人間）が定理証明支援系を用いて証明するのと同じくらいの能力を LLM が持った（持っている）としても， より高度で抽象的な数学に挑戦するような数学者たちが脅かされることは全くないと思いますが， いわゆる Copilot として有効活用できるような未来はありうると思います．

と言うわけで，定理証明支援系は素晴らしいソフトウェアなのですが， 如何せん私を含む初学者には扱いが難しいと言うのが正直なところです．

証明の正しさが機械的に保証できると言うのは， 裏を返すと機械的に正しさを保証できるような証明をきちんと記述する必要があると言うことでもあり， それぞれの定理証明支援系が様々な工夫を行なってこの手間を軽減しようとはしているものの， 紙の上で曖昧さを残しながら証明を行うのと比べると大変なことが多いです． これは特に抽象度の高い数学分野になってくると如実に現れると思います． そう言った事情もあり， ソフトウェア分野における証明（ソフトウェア検証など）においては良く見かけるものの， 正直なところあまり一般的に良く使われると言う印象はありません．

またアカデミア発のプロダクトにありがちですが， 日本語で親切な説明が沢山あるかと言われると， 私の知る限りではあまりないです． そもそもユーザが少ないので仕方のないことだと思います．

と言うわけで，今回参加した勉強会はとても貴重でありがたいものでした．

勉強会について

私はこのような勉強会に参加するのが初めてだったのですが， とても楽しく参加できました． 主催者やその他参加者の方々に感謝したいです．

これは「数学系のための」勉強会で， 数学の研究者や学生を対象としているので， 「数学科出身でないのに参加しても大丈夫か． 研究者でも学生でもないし （一応研究開発業務に従事していますが，理論的研究からは遠いです）」 とかなり悩みましたが， 参加して良かったです．

勉強会は， 最初に簡単に Lean の使い方などについて説明していただいた後に， 用意していただいた教材を各自進めて， 後で解説するといった流れでした（後半の発展的内容については解説が後に配られました）． 体力不足で後半集中力を切らしていたので， 個人的にはこの進め方はとても助かりました． ひたすら怒涛の勢いで解説… のような感じだとおそらく途中でギブアップしてしまったと思います． 集中力，もう少しなんとかしたいですが， 瞼がヒクヒクしだしたので諦めました．

私はオンラインで参加しましたが， 今回教室を貸し出していただいたのは 「すうがくぶんか」という社会人のための数学教室 なようでした． 私はこの教室について知らなかったのですが， 理化学研究所の佐野岳人先生とかも講義されているみたいです． 例えば， 佐野先生の位相空間論の全 12 回の講義 (10/7–12/23) が 58,500 円で聴講できるようです． 6 万円は正直今の私には少し厳しいのですが…， とても気になりますね． もう少し稼げるようになったらこういったものも参加してみたいです． その頃には時間的，体力的余裕が全くなくなっているかも知れませんが． とはいえ，大した趣味もないし， 社会のためにも（？）出来れば稼いだお金はこういったところに還元したいとは思っています．

今回の一件で味を占めてしまい， X/Twitter で色々探していたら， すうがく徒の集い と言うものも見つけてしまいました． 発表リストを見た感じ， 自分には全く理解できなさそう（残念ながら要求知識を全く満たしていません）ですが， どうしようかな…

まとめ

定理証明支援系 Lean の勉強会に参加してきました． 最高でした！また参加したいです．

  1. ZFC の公理を用いて証明を行うことができるものもあります． ↩