WolframInstitute/MathlibLink

Connect Wolfram Language to mathlib for typed mathematics and checked proofs

Contributed By: Wolfram Institute

InstallMathlib prepares the runtime and MathlibInstallation gives its project directory. Import that project with LeanImport, evaluate with LeanEvaluate and verify theorems with LeanVerify. The environment interface requires the accompanying LeanLink development branch; existing MathlibLink session APIs remain supported.

Installation Instructions

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

To load the code after installation, evaluate this code:
Needs["WolframInstitute`MathlibLink`"]

Details

MathlibLink prepares mathlib; LeanLink imports its complete declaration namespace.

Functions, theorems, structures and instances share a declaration interface.

Exact supported values can be copied to Wolfram Language; other expressions remain typed Lean objects.

Proof construction includes kernel replay and axiom checks.

The external runtime pins Lean 4.35.0 and mathlib v4.35.0. Setup is explicit.

Loading the paclet installs nothing.

Paclet Guide

Examples

Paclet Source

Definition Notebook »