Lean は証明の正しさを確認するためだけのツールって思ってませんか？

Lean は証明の正しさを確認するためだけのツール …って思ってませんか？ 2026年7月 AI for math

最近、AI が話題ですね

最近、AI が話題ですね数学の証明も任せられるようになった人間より賢いね

最近、AI が話題ですねでも AI が賢過ぎてチェックが難しい「AI がこう書いてるから大丈夫やろ」そんなわけないよね

最近、AI が話題ですねそこで Lean が注目を浴びている Lean は AI を信じちゃったりしないのでより客観的に検証できる

でもちょっと待って

でもちょっと待って Lean は確かに証明の検証に有用でも実像があまり広まってないのでは？

でもちょっと待って Lean は数学の証明の検証に役立つ… だけじゃない Lean の可能性をもっと見てほしい …という話をしたい

自己紹介趣味で Lean の本を書いている一般人 Lean by Example や「ゼロから～」の著者

自己紹介【宣伝】ラムダノートが潰れないよう応援してくれると嬉しい

自己紹介本業はソフトウェア開発【宣伝】 Proxima Technology という会社にいます数学科卒を積極的に雇ってる会社です

自己紹介本業はソフトウェア開発【宣伝】もし興味があれば会社のHP等から連絡ください

そもそも Lean で証明ができるのはなぜ？プログラミング言語なのに証明も書けるって、冷静に考えると謎では

そもそも Lean で証明ができるのはなぜ？いろんな誤解を見てきました

誤解1 論理式のゲーデル数を計算してる？

誤解1 論理式のゲーデル数を計算してる？そんなことをしたら計算が大変そう

誤解2 ZFC に基づいてるんでしょ？

誤解2 ZFC に基づいてるんでしょ？すごくたくさんある誤解「数学の基礎と言えばZFC」だから？

誤解3 HoTT ってやつでしょ？

誤解3 HoTT ってやつでしょ？めっちゃ惜しいホモトピー型理論（HoTT）は、 Lean 2 まではサポートされていた

誤解3 HoTT ってやつでしょ？ HoTT を使うと自動証明が遅くなるからという理由で捨てられた、らしい

正解カリー・ハワード同型対応を使い依存型の中で述語論理をやっている

正解カリー・ハワード同型対応を使い依存型の中で述語論理をやっている依存型については説明をしない（ぜひ拙著を読んでほしい）

正解カリー・ハワード同型対応を使い依存型の中で述語論理をやっているカリーハワード同型対応というのは、「証明はプログラムだ」という同一視のこと

正解カリー・ハワード同型対応を使い依存型の中で述語論理をやっている・命題は型・証明はその項・帰納法は再帰などなど…。

正解カリー・ハワード同型対応を使い依存型の中で述語論理をやっている特に、命題 P を証明するのは h : P という項を構成するのと同じ

正解カリー・ハワード同型対応を使い依存型の中で述語論理をやっているよってプログラムの型チェックがすなわち証明のチェックになる

正解カリー・ハワード同型対応を使い依存型の中で述語論理をやっている「普段プログラム書いてて同型みを感じない」という感想も観測するけどそれは多分書いてる言語のせい動的言語をメインで書いていませんか？

…だから何なんだろう

…だから何なんだろう Lean が「プログラミング言語でもある」のはカリーハワード同型対応を使ってるから

…だから何なんだろう Lean がプログラミング言語でもあるということは Lean で書いたプログラムをLean 内で検証できる

…だから何なんだろう Lean は do 構文が Haskell より強力で for ループとか while
ループも書き放題命令的プログラムの検証も Lean 内でできる（専用フレームワークがある）

…だから何なんだろう Lean では数学の証明しか書かないとしても自動証明は Lean 内のプログラムとして書くので Lean がプログラミング言語でもあることは関係がある

カリーハワード対応の帰結まとめ・Lean 自身がプログラミング言語・プログラムとその証明を一緒に書ける・自動証明とも関連が深い

カリーハワード対応の帰結まとめそもそもプログラムと証明の関連が深いと言っている時点でおもしろいと思う計算も論理もおもしろい対象だから一緒に楽しめておトク（個人の感想です）

数学は今後どうなるのか

数学は今後どうなるのか私の個人的な感想や妄想が混じりますすみません

数学は今後どうなるのか私は学部生のころ代数学をやって、修士で計算機科学に移った

数学は今後どうなるのか数学系の教室は理学部にあるが計算機系の教室は工学部にありめっちゃ歩かないといけない改めて調べたら約500mでした

数学は今後どうなるのかぼく「遠いなあ」ﾃｸﾃｸ…

数学は今後どうなるのかぼく「遠いなあ」ぼく「数学と計算機って両方やる人いないの？」

数学は今後どうなるのかぼく「遠いなあ」ぼく「数学と計算機って両方やる人いないの？」ぼく「でも数学と計算機って近い分野では？」

数学は今後どうなるのか計算機科学が数学にズブズブなのは周知の通りプログラマの採用でも数学科卒は「できそう」って思われたりする

数学は今後どうなるのか数学でも計算的な観点は重要で数学的問題の動機に計算的な需要があったりするしかし、こっちはあまり意識されていない気がする

数学は今後どうなるのかたとえばユークリッドの互除法について x, y が互いに素なら a*x+b*y=1 となる a,b の存在がわかって嬉しい！
という話がどの数論の教科書にも載っている

数学は今後どうなるのかしかし、互除法は高速でもある速さに言及している数学系の本はあまりないがそこスルーするべきところか…？ﾓﾔﾓﾔ

数学は今後どうなるのかあと、数学だと・「存在する」と・「具体的に計算できる」を明示的に区別しない気がするそれは大事な区別では？

数学は今後どうなるのかたとえば高校数学では「正方形の対角線の長さは存在するので√2 は存在する」という話を習うが実際にどうやれば平方根が計算できるかは習わない

数学は今後どうなるのかぼく「数学と計算機の間の橋が必要だ」

数学は今後どうなるのかぼく「数学と計算機の間の橋が必要だ」当時は Lean を知らなかったが、今では Lean が橋になれるのでは？と思っている

数学は今後どうなるのか Lean で数学を学んだネイティブ世代が増えたら、数学の語られ方やコミュニティは変わるのでは？

知らんけど

ご清聴ありがとうございました

Lean は証明の正しさを確認するためだけのツールって思ってませんか？

Lean は証明の正しさを確認するためだけのツールって思ってませんか？

More Decks by 井上亜星

Other Decks in Programming

Featured

Transcript