v0.1.2

MathlibLink 0.1.2

• Check the latest published LeanLink on every setup run and update older installations, including when mathlib is already installed. No LeanLink version or archive is pinned.
• Validate evaluator capabilities and request a kernel restart after updating a loaded LeanLink.
• Preserve the final output of fast setup commands so a completed installation is not incorrectly reported as missing.
• Fix tutorial plots and quick-start examples using LeanLink's environment evaluator.
• Reevaluate documentation examples during builds and reject messages, unevaluated calls and unexpected failures before packaging or publishing.

Requires Wolfram Language 15.0 or later, the current LeanLink release,
Lean 4.35.0 and mathlib v4.35.0.

v0.1.1

MathlibLink 0.1.1

• Reuse LeanLink's imported environments for evaluation and proof checking when supported.
• Use LeanLink's in-process evaluator by default when available. Set "Isolated" -> True in MathlibEvaluate or MathlibCall to evaluate in a separate process.
• Prepare evaluation during imports, improve cleanup and remove unnecessary waits when reading installation output.
• Display sessions, declarations, values and expressions as expandable notebook summaries.

Existing MathlibLink session functions remain supported with LeanLink 1.2.5 or
later. The new environment interface, evaluator preparation and in-process evaluation require
LeanLink PR #4 until those
changes are released. Loading MathlibLink does not start Lean or install software.

Requires Wolfram Language 15.0 or later, Lean 4.35.0 and mathlib v4.35.0.

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.