---
title: PythonとLeanをつなぐNerodiaについて調べてみた
tags: 
author: [Yuki Imamura](https://docswell.com/user/imamuray)
site: [Docswell](https://www.docswell.com/)
thumbnail: https://bcdn.docswell.com/page/4JQYQNL57P.jpg?width=480
description: 2026/9/26 鯱.py × Unagi.py コラボイベント in 豊橋 で発表した資料です。 イベントページ：https://shachi-py.connpass.com/event/403190/
published: September 27, 26
canonical: https://docswell.com/s/imamuray/Z6NDYE-2026-09-27-001428
---
# Page. 1

![Page Image](https://bcdn.docswell.com/page/4JQYQNL57P.jpg)

PythonとLeanをつなぐ
Nerodiaについて調べてみた
2026/9/26 鯱.py × Unagi.py コラボイベント in 豊橋
発表者：imamuray
▲Nerodiaのロゴ, https://github.com/leanprover/nerodia より引用


# Page. 2

![Page Image](https://bcdn.docswell.com/page/K74WNGDVE1.jpg)

発表の概要
●
●
●
●
●
Nerodiaとは？
Nerodiaのインスパイア元 PyO3 について
Leanの紹介
Nerodiaを実際に動かしてみた
まとめ


# Page. 3

![Page Image](https://bcdn.docswell.com/page/LJ1Y5DZ4EG.jpg)

Nerodiaとは？
PyO3にインスパイアされたPythonとLeanをつなぐライブラリ
●
まだ試験段階で、実用はまだ先
将来的にPythonとLeanを相互運用できる未来がくるかも？
Rust
Python
PyO3
Lean
Nerodia
呼び出せる
相互に呼び出せる
●
●
メモリ安全性
高速な処理
開発中？
検証された信頼性
の高い処理


# Page. 4

![Page Image](https://bcdn.docswell.com/page/GJWG5Y9Z72.jpg)

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
ある言語からほかの言語の関数などを呼び出す機構


# Page. 5

![Page Image](https://bcdn.docswell.com/page/4EZLNX9L73.jpg)

PyO3 ― RustとPythonをつなぐライブラリ
RustとPythonの相互運用を実現するためのライブラリ
●
RustからPython呼び出せたり、逆にPythonからRust呼び出せたりできる
うれしいこと
●
Rustのメモリ安全性があり高速な処理をPythonから呼び出せる
PyO3が使われている主なライブラリ
●
●
●
pydantic-core: データ検証ライブラリpydanticの内部実装
polars: データフレームライブラリ
ruff: pythonのlinter/formatter
○
備考：ruffはPyO3を直接使っていないが、 PyO3に依存している maturinを使っている


# Page. 6

![Page Image](https://bcdn.docswell.com/page/Y76W84KM7V.jpg)

Leanとは？
OSSの関数型言語＆証明支援系
●
証明支援系(proof assistant)：数学の定理やプログラムの性質・仕様を記述し、そ
れらの証明をコンピュータで検査するためのツール
2013年から開発が始まり、現在のバージョンはLean4
現在はLean Focused Research Organization（Lean FRO）とコミュニティによって開発
されている


# Page. 7

![Page Image](https://bcdn.docswell.com/page/G75M9QPQ74.jpg)

Leanを使ってうれしいこと
プログラムの性質の証明を書いて、動作の信頼性を高められる
●
●
一般的な言語で動作を確認するときは、具体的な入力に対するテストを書く
○ → 考慮漏れの可能性
Leanでは「この条件のとき必ずこうなる」を証明として書ける
○ 例「入力が整数ならばこの関数はエラーにならない」など
○ → 条件を満たすすべてのケースについて保証できる
暗号ライブラリやセキュリティ関連など、安全性が求められる分野でLeanが使われてい
る
●
●
AWSの認可ポリシー記述言語Cedar
Microsoftの暗号ライブラリSymCrypt


# Page. 8

![Page Image](https://bcdn.docswell.com/page/9J292P6WER.jpg)

最近、Leanの注目度が上がってる？
9月に入って立て続けにAI×Leanの話題があった
●
●
AnthropicがAIとLeanを使ってフェルマーの最
終定理の形式化をした
OpenAIが数学の未解決問題をAIとLeanを
使って解いた
9/23にClaude Codeの創出者がXで形式検証
(Lean関連)のことをつぶやいて、ちょっと話題になっ
た
link: https://x.com/bcherny/status/2102543349102338309


# Page. 9

![Page Image](https://bcdn.docswell.com/page/DEY4Y599JM.jpg)

やってみた
NerodiaのREADMEにあった方法を試す。
実行環境：Ubuntu, Lean 4.34.1, Python 3.14.4
pythonから呼び出すときのモジュール名
pythonで表示するDoc String
pythonでの関数名
Leanコードをビルド後、
Pythonパッケージにビルド
Leanで書いた関数を Nerodiaを使って
Pythonから呼び出すことができた


# Page. 10

![Page Image](https://bcdn.docswell.com/page/VJNYPNLD78.jpg)

現状の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は文字列の長さ以下である」証明


# Page. 11

![Page Image](https://bcdn.docswell.com/page/YE9P3R48J3.jpg)

まとめ
Nerodiaはまだ開発中
●
ロードマップ的には来年2月頃にもう少し使いやすくなっているかも？
Nerodiaのようなライブラリが発展すれば、PythonからLeanの資産を使える
●
●
Leanによって検証された信頼性の高い処理を扱える
将来的にはPyO3とRustのように、Pythonで使えるライブラリにLeanが使われるよ
うになるかも？


# Page. 12

![Page Image](https://bcdn.docswell.com/page/GE8DMWQZED.jpg)

参考資料
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