Wolfram Cloud Resource Object

Paclet Resource

Wolfram/LeanLink

Native link between Wolfram Language and Lean 4

Contributed By: Nik Murzin

The entry points are LeanImport and LeanImportString (load an environment) and LeanExport / LeanExportString (write Lean source back). LeanTerm and LeanEnvironment are the two computable wrappers; the Parse*-style CIC heads - LeanConst, LeanApp, LeanForall, LeanLam, LeanLet, LeanBVar, LeanFVar, LeanSort, LeanLitNat, LeanLitStr, LeanProj - build expressions, with universe levels LeanLevelZero, LeanLevelSucc, LeanLevelMax. LeanState, LeanTactic, and LeanGoal run interactive proofs; ProofToLean transpiles a ProofObject; LeanCompile, LeanToFunction compile to native code; LeanExprGraph, LeanCallGraph, LeanListTheorems query a project out of process.

Installation Instructions

To install this paclet in your Wolfram Language environment, evaluate this code:
PacletInstall[ResourceObject["https://wolfr.am/1HXtzUnZG"]]


To load the code after installation, evaluate this code:
Needs["Wolfram`LeanLink`"]

Details

LeanLink is a high-performance native bridge between the Wolfram Language and the Lean 4 theorem prover. It embeds the Lean runtime directly through a compiled LibraryLink shim - there is no subprocess per call and no text-protocol round-trip for the core API.
A loaded environment is a LeanEnvironment, a typed wrapper over Association[name → LeanTerm, …]. LeanImport loads constants from a compiled Lean module (Mathlib included); LeanImportString compiles a Lean source string on the fly.
Every Lean expression is a symbolic tree built from a small set of CIC heads - LeanConst, LeanApp, LeanForall, LeanLam, LeanBVar, LeanSort, LeanLitNat, … - each carrying box formatting so it displays in Lean-source notation.
A LeanTerm exposes "Type" / "Term" (expression trees), "TypeForm" / "TermForm" (pretty-printed source), "Parameters" (the unfolded binder chain), and "ExprGraph" / "CallGraph" (native Graph visualizations).
LeanState and LeanTactic drive interactive tactic proofs step by step; ProofToLean transpiles a Wolfram ProofObject into a checkable LeanEnvironment; LeanCompile and LeanToFunction lower a Lean definition to a FunctionCompile function.
The serialization backend is a compact binary (WXF) format, so goal states and expression trees cross the boundary without a parsing pass.

Paclet Guide

Examples

Disclosures

  • Wolfram Language built-in symbols

Paclet Source

Source Metadata

  • Citation: Leonardo de Moura, Sebastian Ullrich, *The Lean 4 Theorem Prover and Programming Language*, CADE 28, 2021

See Also