MathlibLink connects Wolfram Language to mathlib, Lean's mathematics library. MathlibLink prepares the runtime; LeanLink imports its declarations, evaluates expressions and checks proofs.
Requires Wolfram Language 15.0 or later.
Documentation · Wolfram resource · Releases
Install and load the paclet:
PacletInstall[ResourceObject["https://wolfr.am/1IuI3kKSs"]]Needs["WolframInstitute`MathlibLink`"]Prepare the pinned runtime once. Missing prerequisites are installed locally:
InstallMathlib[]Setup reuses working Git, curl and elan installations. See InstallMathlib for setup options and progress reporting.
Each setup run checks the latest published LeanLink and installs an update
when available. Restart the kernel after updating a loaded LeanLink. Existing
StartMathlibSession, MathlibCall and ProveMathlib calls remain supported.
Load LeanLink:
Needs["Wolfram`LeanLink`"]Import the binomial-coefficient module from the installed mathlib project:
env = LeanImport["Mathlib.Data.Nat.Choose.Basic", "ProjectDir" -> MathlibInstallation[]["Directory"], "PrepareEvaluation" -> True]Apply an imported function:
LeanEvaluate[env["Nat.choose"], 10, 4]Evaluate a family of inputs in one call:
LeanEvaluate[env, "(List.range 11).map (fun k => Nat.choose 10 k)"]"PrepareEvaluation" -> True prepares the evaluator while importing modules.
Later calls reuse it; Needs alone starts no Lean process.
Batching inputs also reduces transfers between Wolfram Language and Lean.
Compile a theorem using the same imports:
proofs = LeanImportString[env, "theorem addZero (n : Nat) : n + 0 = n := by rfl"]Check its proof and axiom dependencies:
LeanVerify[proofs["addZero"]]Release the environments when finished:
Scan[LeanFreeEnvironment, {proofs, env}]Use LeanImport["Mathlib", "ProjectDir" -> directory] for the full library,
or select modules to reduce startup time and memory use. Keys[env] lists
names; env[name] returns a Lean term whose type, definition and axioms can
be inspected. No function whitelist or separate mathlib evaluator is needed.
Computable expressions can produce Wolfram values. Noncomputable definitions and proofs remain typed Lean terms. See values and proofs for examples, and the coverage report for namespace and live verification results.
- Getting started
- Exact arithmetic patterns
- Partial computations
- Function guide
- Upstream mathlib documentation
The runtime pins Lean 4.35.0 and mathlib v4.35.0. The upstream documentation tracks current mathlib and may describe a newer release.
Load the source paclet from this repository:
PacletDirectoryLoad[FileNameJoin[{Directory[], "MathlibLink"}]]
Needs["WolframInstitute`MathlibLink`"]| Command | Purpose |
|---|---|
make check |
Check sources and reference coverage |
make test |
Run local tests |
make test-mathlib |
Run tests against mathlib |
make notebooks |
Build documentation with PacletPage |
make check-publish |
Build and check the paclet archive |
make publish |
Publish the paclet and documentation |
See GUIDE.md for development conventions and CI and releases for the three-platform workflow and publishing setup.