Repository navigation
v0.1.0
MathlibLink 0.1.0
Wolfram Language access to Lean's mathlib for exact computation and checked proofs.
- Browse the complete declaration namespace of imported mathlib modules, including functions, theorems, structures and instances.
- Apply named functions and evaluate Lean expressions, returning exact Wolfram values where supported.
- Retain other values as typed, session-owned Lean objects.
- Check proofs with Lean's kernel and inspect their axiom dependencies.
- Install the pinned Lean, mathlib and LeanLink runtime, including missing command-line prerequisites.
Requires Wolfram Language 15.0 or later. Supports Linux x86-64, Windows x86-64
and macOS ARM64. The runtime pins Lean 4.35.0 and mathlib v4.35.0.
The release includes the paclet archive, SHA-256 checksums, build provenance
and the PacletPage documentation build. Cloud publication uses this same
verified archive.