PythonとLeanをつなぐNerodiaについて調べてみた
-- Views
September 27, 26
スライド概要
2026/9/26 鯱.py × Unagi.py コラボイベント in 豊橋 で発表した資料です。
イベントページ：https://shachi-py.connpass.com/event/403190/
ITエンジニア
関連スライド
Meta XR SDK(V66-74)でQuestアプリを開発
あうぜん
1.2M
各ページのテキスト
PythonとLeanをつなぐ Nerodiaについて調べてみた 2026/9/26 鯱.py × Unagi.py コラボイベント in 豊橋 発表者：imamuray ▲Nerodiaのロゴ, https://github.com/leanprover/nerodia より引用
発表の概要 ● ● ● ● ● Nerodiaとは？ Nerodiaのインスパイア元 PyO3 について Leanの紹介 Nerodiaを実際に動かしてみた まとめ
Nerodiaとは？ PyO3にインスパイアされたPythonとLeanをつなぐライブラリ ● まだ試験段階で、実用はまだ先 将来的にPythonとLeanを相互運用できる未来がくるかも？ Rust Python PyO3 Lean Nerodia 呼び出せる 相互に呼び出せる ● ● メモリ安全性 高速な処理 開発中？ 検証された信頼性 の高い処理
Nerodiaを調べようとした経緯 Leanの今年9月から来年年2月までのロードマップで以下のように書かれていた We will deliver a simple FFI from Python, followed by further languages. The foundation is Nerodia, our Lean/Python FFI inspired by PyO3:... （中略） Python is the priority: the AI ecosystem is dominated by Python, and it is unrealistic to expect those users to switch languages. link: https://lean-lang.org/fro/roadmap/y4-1/ ● ● ● Pythonから始めて、ほかの言語とLeanを連携させたい Nerodiaというライブラリを基盤にする AIはPythonが主流だから、Pythonの優先度が高い → Nerodiaについて調べてみよう！ ※FFI: Foreign Function Interface ある言語からほかの言語の関数などを呼び出す機構
PyO3 ― RustとPythonをつなぐライブラリ RustとPythonの相互運用を実現するためのライブラリ ● RustからPython呼び出せたり、逆にPythonからRust呼び出せたりできる うれしいこと ● Rustのメモリ安全性があり高速な処理をPythonから呼び出せる PyO3が使われている主なライブラリ ● ● ● pydantic-core: データ検証ライブラリpydanticの内部実装 polars: データフレームライブラリ ruff: pythonのlinter/formatter ○ 備考：ruffはPyO3を直接使っていないが、 PyO3に依存している maturinを使っている
Leanとは？ OSSの関数型言語＆証明支援系 ● 証明支援系(proof assistant)：数学の定理やプログラムの性質・仕様を記述し、そ れらの証明をコンピュータで検査するためのツール 2013年から開発が始まり、現在のバージョンはLean4 現在はLean Focused Research Organization（Lean FRO）とコミュニティによって開発 されている
Leanを使ってうれしいこと プログラムの性質の証明を書いて、動作の信頼性を高められる ● ● 一般的な言語で動作を確認するときは、具体的な入力に対するテストを書く ○ → 考慮漏れの可能性 Leanでは「この条件のとき必ずこうなる」を証明として書ける ○ 例「入力が整数ならばこの関数はエラーにならない」など ○ → 条件を満たすすべてのケースについて保証できる 暗号ライブラリやセキュリティ関連など、安全性が求められる分野でLeanが使われてい る ● ● AWSの認可ポリシー記述言語Cedar Microsoftの暗号ライブラリSymCrypt
最近、Leanの注目度が上がってる？ 9月に入って立て続けにAI×Leanの話題があった ● ● AnthropicがAIとLeanを使ってフェルマーの最 終定理の形式化をした OpenAIが数学の未解決問題をAIとLeanを 使って解いた 9/23にClaude Codeの創出者がXで形式検証 (Lean関連)のことをつぶやいて、ちょっと話題になっ た link: https://x.com/bcherny/status/2102543349102338309
やってみた NerodiaのREADMEにあった方法を試す。 実行環境：Ubuntu, Lean 4.34.1, Python 3.14.4 pythonから呼び出すときのモジュール名 pythonで表示するDoc String pythonでの関数名 Leanコードをビルド後、 Pythonパッケージにビルド Leanで書いた関数を Nerodiaを使って Pythonから呼び出すことができた
現状のNerodiaでできること ● Python側へ公開する型はまだ限られている ○ ○ ○ ✅整数型、文字列型の変換： Int → int, Nat → int, String → str ❌リストの変換はできない： List Int → list[int] 例 ■ ✅def sumAsString (a b : Nat) : String := toString (a + b) ■ ❌def append (xs ys : List α) : List α := xs ++ ys ● ● NerodiaがListに非対応なのでビルドできない 逆にPythonに公開する型だけ気をつければ、関数内部はLeanで自由に書ける getChar は文字列のn番目の文字を取得する関数 nが文字列の長さを超えるときは空文字列を返す ok が「nは文字列の長さ以下である」証明
まとめ Nerodiaはまだ開発中 ● ロードマップ的には来年2月頃にもう少し使いやすくなっているかも？ Nerodiaのようなライブラリが発展すれば、PythonからLeanの資産を使える ● ● Leanによって検証された信頼性の高い処理を扱える 将来的にはPyO3とRustのように、Pythonで使えるライブラリにLeanが使われるよ うになるかも？
参考資料 PyO3 ● 解説記事 ○ ○ ● PythonとRustの融合：PyO3/maturinを使ったPythonバインディングの作成入門 | gihyo.jp https://gihyo.jp/article/2023/07/monthly-python-2307 GitHubリポジトリ ○ https://github.com/pyo3/pyo3 Lean, Nerodia ● Lean FROのロードマップ ○ ○ ● The Lean FRO Year 4 - Part 1 Roadmap https://lean-lang.org/fro/roadmap/y4-1/ NerodiaのGitHubリポジトリ ○ https://github.com/leanprover/nerodia