Leo3: Rust Bindings for Lean4

Leo3 provides safe, ergonomic Rust bindings to the Lean4 theorem prover, inspired by PyO3's architecture.

Quick Start

Requires Lean 4.25.2 (install via elan).

[dependencies]
leo3 = "0.2.1"

use leo3::prelude::*;

fn main() -> LeanResult<()> {
    leo3::prepare_freethreaded_lean();

    leo3::with_lean(|lean| {
        let s = LeanString::new(lean, "Hello from Rust!")?;
        println!("{}", LeanString::to_str(&s)?);

        let n = LeanNat::from_usize(lean, 42)?;
        println!("{}", LeanNat::to_usize(&n)?);
        Ok(())
    })
}

Features

Type Conversions

Bidirectional conversions between Rust and Lean types via IntoLean / FromLean traits:

Procedural Macros

#[leanfn] — Export Rust functions to Lean:

#[leanfn]
fn add(a: u64, b: u64) -> u64 {
    a + b
}

#[leanclass] — Expose Rust structs as Lean external classes with auto-generated FFI wrappers and Lean source declarations:

#[leanclass]
struct Counter { value: i64 }

#[leanclass]
impl Counter {
    fn new() -> Self { Counter { value: 0 } }
    fn get(&self) -> i64 { self.value }
    fn increment(&mut self) { self.value += 1; }
}

#[derive(IntoLean)] / #[derive(FromLean)] — Automatic conversion derive macros.

Meta-Programming

Full access to Lean's kernel and elaborator:

• LeanEnvironment — Create and manage declaration environments
• LeanExpr — Build expressions (binders, applications, literals, lambda, forall)
• LeanDeclaration — Define axioms, definitions, and theorems
• MetaMContext — Type inference, type checking, definitional equality, proof validation
• Tactic support

IO & Runtime

• IO operations: console, filesystem, environment variables, process, time
• LeanClosure — Create and apply Lean closures from Rust
• LeanTask / LeanPromise — Parallel computation with combinators (join, race, select, timeout)
• LeanModule — Dynamic loading of compiled Lean shared libraries
• Tokio bridge for async integration
• LeanThunk — Lazy evaluation

Architecture

leo3/
├── leo3/                   # Safe high-level abstractions
├── leo3-ffi/               # Raw FFI bindings to Lean4's C API
├── leo3-build-config/      # Build-time Lean4 detection and configuration
├── leo3-macros/            # Procedural macro entry points
├── leo3-macros-backend/    # Procedural macro implementations
└── leo3-ffi-check/         # FFI layout validation (à la pyo3-ffi-check)

Design

• Lean<'l> token proves runtime initialization at compile-time
• LeanBound<'l, T> (lifetime-bound), LeanRef<T> (unbound), LeanUnbound<T> (thread-safe) smart pointers with automatic reference counting
• #[repr(transparent)] zero-cost wrappers
• Copy-on-write semantics for &mut self FFI methods
• Worker thread architecture for all Lean runtime calls (avoids mimalloc heap issues)
• Version support: Lean 4.20.0–4.30 with #[cfg(lean_4_25)] gates

Comparison with PyO3

Development

cargo test                        # Full test suite (requires Lean 4.25.2)
cargo test --test meta_basic      # Specific test
LEO3_NO_LEAN=1 cargo test --lib   # Compile-only, no Lean runtime

License

MIT OR Apache-2.0

Acknowledgments

• PyO3 — Architectural inspiration
• Lean4 — The theorem prover Leo3 binds to