LeanとRust・Python・TypeScript・Clojureを双方向につなぐleanfranを作った

2026-11-13

Lean 4で書いて証明した関数を、Rust、Python、TypeScript、Clojureから呼べるleanfranを作りました。逆向きに、各言語で書いた関数をLeanに翻訳し、その性質を証明することもできます。Leanで証明した実装をアプリケーションに組み込む使い方と、普段の言語で書いた実装をLeanで検証する使い方があります。Leanから各言語への生成では、コンパイラの中間表現を読み、その言語のライブラリを作ります。生成したコードは、各言語の実行環境とleanfranの実行時ライブラリで動きます。リポジトリはconao3/lean-leanfranで、ライセンスはApache-2.0です。この記事はv0.6.0の機能を紹介します。

conao3/lean-leanfranWrite and prove functions in Lean 4, run them as Rust, Python, TypeScript and ClojureLeanStar

証明した関数をアプリケーションで使う

Leanは関数を書き、その関数の性質を証明できる言語です。たとえば、引数を2倍する関数と、その結果が常に引数の2倍になるという定理を、次のように書けます。

def double (n : Nat) : Nat := n + n

theorem double_eq (n : Nat) : double n = 2 * n := by
  unfold double
  omega

Nat は0以上の整数です。double_eq は、すべての n について等式が成り立つことを述べています。Leanはこの証明を検査し、すべての自然数で等式が成り立つことを確かめます。

アプリケーションでこの関数を使うときも、証明した実装をそのまま使いたいです。別の言語で関数を書き直すと、その実装とLeanの関数が同じ計算をするかを改めて確かめる必要があります。leanfranはLeanの関数からアプリケーションの言語のソースを生成します。日付や金額の計算、データの整列、状態遷移のような関数をLeanで書き、画面やHTTPの処理を普段使っている言語で書く使い方を想定しています。

対応する言語

leanfranは、Rust、Python、TypeScript、Clojureに対応しています。各言語に、Leanからコードを生成する機能と、その言語の関数をLeanに翻訳して検証する機能があります。パッケージはそれぞれの言語のレジストリから入れられます。

言語	パッケージ	ソースと使い方
Rust	leanfran	langs/Rust/
Python	leanfran	langs/Python/
TypeScript	leanfran	langs/TypeScript/
Clojure	io.github.conao3/leanfran	langs/Clojure/

各バックエンドはLean 4.35.0を使い、同じバージョンでリリースしています。各バックエンドには、Leanのコードを別ファイルから読み込む方法と、利用先の言語のソースに埋め込む方法があります。

TypeScriptでは、先ほどの関数と定理を次のように埋め込めます。次のコードを src/arith.ts に保存します。

import { lean } from "leanfran"
import * as arith from "./_lean/arith.ts"

export const arithBlock = lean(
  "arith",
  String.raw`
def double (n : Nat) : Nat := n + n

theorem double_eq (n : Nat) : double n = 2 * n := by
  unfold double
  omega
`,
)

console.log(arith.double(21n))

leanfran sync を実行すると、Leanが定理を検査し、 _lean/arith.ts に関数を生成します。その後は、生成された関数をTypeScriptから呼べます。この例を動かすと 42n が出力されます。導入の手順はTypeScriptのREADME、構造体を使う例は型とschemaのガイドにあります。

型と入力の検査

関数の計算だけでなく、引数と戻り値も利用先の言語で扱える形に変換します。Leanの構造体や帰納型をもとに、各バックエンドが公開する型と変換のコードを生成します。

TypeScriptではLeanの型からTypeScriptの型とStandard Schemaに対応したschemaを生成します。そのschemaをHonoのバリデータに渡し、HTTPのリクエストを検査できます。逆に、手元のzodなどのschemaをLeanの構造体にして、制約を証明の前提に使うこともできます。Pythonではpydanticのモデルとしてデータを扱えます。具体例はTypeScriptのpricing-apiとPythonのpricing-apiにあります。

ここで入力の検査は、アプリケーションが受け取った値を調べ、Lean側の証明が仮定する条件を満たすかを確かめます。たとえば、下限が上限以下であることを前提にした証明を使うなら、外部から受け取る値にもその条件が必要です。

普段の言語で書いた関数の検証

逆向きに、Rustなどで書いた関数をLeanの仕様と比べる使い方もあります。対応する範囲の関数をLeanに翻訳し、その翻訳について定理を証明します。

Rustでは #[leanfran::model] を付けた関数をLeanのモデルに翻訳します。たとえば、入力を2倍し、上限を超えるときは u32::MAX を返す関数です。10-ensuresのサンプルから抜き出しています。

#[leanfran::model(ensures(ge = double::ge))]
pub fn saturating_double(x: u32) -> u32 {
    if x > u32::MAX / 2 {
        u32::MAX
    } else {
        x * 2
    }
}

double::ge は「戻り値が入力以上になる」という仕様です。Leanで次のように定義しています。

def ge (x r : Std.U32) : Bool := decide (x.val ≤ r.val)

cargo leanfran extract を実行すると、Rustの関数を翻訳したLeanのモデルと、仕様を満たすことを述べる命題が生成されます。サンプルの lean/Proofs/SaturatingDouble.lean には、その命題の証明があります。

theorem saturating_double.proof.ge : saturating_double.obligation.ge := by
  intro x
  unfold saturating_double _root_.double.ge
  step* <;> simp_all [core.num.U32.MAX, U32.rMax] <;> scalar_tac

cargo leanfran check がこの証明を検査します。ここでは、どの入力でも戻り値が入力以上になることに加え、実行される掛け算でオーバーフローしないことも証明します。アプリケーションではRustで書いた関数を実行し、その性質をLeanで検証できます。

TypeScriptでも同じ向きの検証ができ、関数に model を付け、仕様との一致を表す refines や、戻り値の条件を表す ensures を指定します。

このとき証明する対象はLeanに翻訳した関数です。元の言語での実行に結び付けるには、翻訳が意味を保つことと、翻訳時の前提を守ることが必要です。たとえば、TypeScriptの number を整数として検証するときは、引数と計算途中の値が安全な整数の範囲に収まることを仮定します。対応する構文と前提は関数検証のガイドに書いています。

変換の仕組みと証明の範囲

leanfranはLeanのコンパイラが作った中間表現を読みます。この段階では実行に要る関数やデータの扱いが具体的な命令になっています。各バックエンドはその命令を対象言語のコードに変え、整数、文字列、配列などの操作は実行時ライブラリが担います。生成したコードの実行はその言語の中で完結します。

Leanの定理が直接保証するのは、Leanで定義した関数の性質です。生成したコードにもその性質が成り立つには、バックエンドと実行時ライブラリがLeanの計算を正しく再現する必要があります。この部分はテストで確かめています。LeanのCバックエンドで動かした結果と生成コードの結果を比べるテストも行っています。leanfran自体の変換の正しさをLeanで証明したわけではありません。

Leanを共通語にする構想

leanfranという名前は、共通語を表すlingua francaから作りました。Leanの型と仕様を、複数の言語で使う共通語にしたいと考えています。

現在使えるのは、Leanのコードを各言語へ生成する機能と、各言語の関数をLeanの仕様に照らして検証する機能です。今後は、たとえばRustからPythonの関数を呼ぶときも、Leanの型から引数と戻り値の変換を生成する仕組みを考えています。この言語間の呼び出しは構想段階です。

まず試すなら、使っている言語のREADMEから、短い関数と証明を1つ動かしてみてください。leanfranの段階ごとのサンプルでは、関数の呼び出しから、型、入力の検査、関数の検証まで順に試せます。