LeanLink

Wolfram Language paclet for native integration with Lean 4.

Features

• Native LibraryLink bridge — embeds the Lean runtime directly via a C shim, no subprocess overhead
• Environment loading — loads .olean environments, queries constants, theorems, types
• Symbolic expressions — Lean expressions as LeanApp, LeanConst, LeanForall, etc.
• Pretty printing — WL-side notation rules for source-code-like output (a * b = b * a)
• Interactive proofs — LeanState/LeanTactic for step-by-step proof construction
• Mathlib support — import and inspect Mathlib modules
• ProofToLean — transpile Wolfram ProofObject to Lean environments

Quick Start

<< Wolfram`LeanLink`

(* Import Mathlib algebra *)
env = LeanImport["Mathlib.Algebra.Group.Basic",
  "ProjectDir" -> "~/src/mathlib4"];

env["mul_comm"]["TypeForm"]
(* "∀ {G : Type u_1} [inst : CommMagma G] (a : G) (b : G), a * b = b * a" *)

(* Interactive proof *)
state = LeanState[env["one_mul"]];
state // LeanTactic["simp"]

Building

Prerequisites

• Lean 4 via elan
• Wolfram Language 15.0+
• CMake 3.20+, C compiler

Build

./build.sh

This runs lake build for the Lean library, then cmake + make for the C shim. The dylib is output to LeanLink/LibraryResources/<platform>/.

Paclet archive

./build.wls

Packs LeanLink/ into a .paclet file, installs it, and uploads to Wolfram Cloud.

Tests

./run_tests.wls

Publish notebooks

./publish_notebooks.wls

Uploads .nb notebooks to Wolfram Cloud.

Notebooks

• LeanLinkIntro — Getting started with LeanLink
• MathlibExamples — Exploring Mathlib from Wolfram Language
• TuringMachineSuccessor — Proving Turing machines compute successor, with proof term graphs for every class in (2,2) and (3,2)

Architecture

LeanLink/
├── LeanLink/                  # Paclet root
│   ├── PacletInfo.wl
│   ├── Kernel/                # Wolfram Language package
│   │   └── Lean.wl            # Main API, pretty-printer, proof engine
│   ├── Assets/                # Bundled .lean files
│   ├── Tests/                 # .wlt test suite
│   └── LibraryResources/      # Built dylibs (per-platform, gitignored)
├── Native/                    # Lean + C source
│   ├── lib/LeanLink/          # Lean 4 source
│   │   ├── EnvStore.lean      # Environment loading, WXF goal export
│   │   └── WXF.lean           # WXF binary serialization
│   └── shim/
│       ├── leanlink_shim.c    # LibraryLink C bridge
│       └── CMakeLists.txt     # Multi-platform build
├── Notebooks/                 # Example notebooks (.md source + .nb)
├── build.sh                   # Native build script
├── build.wls                  # Paclet archive script
├── publish_notebooks.wls      # Notebook evaluation + cloud upload
└── run_tests.wls              # Test runner

License

MIT