Wolfram/LeanLink | Paclet Repository

LeanLink

Wolfram`LeanLink`

embeds the

Lean 4

theorem prover in the Wolfram Language through a native

LibraryLink

shim.

LeanImport

and

LeanImportString

load constants from a compiled module (Mathlib included) or a source string into a

LeanEnvironment

of

LeanTerm

values; each term carries its type and proof as symbolic expression trees built from the CIC heads (

LeanConst

,

LeanApp

,

LeanForall

, …), pretty-prints as Lean source, and draws as a

Graph

.

LeanState

and

LeanTactic

run interactive tactic proofs,

ProofToLean

transpiles a Wolfram

ProofObject

into checkable Lean, and

LeanCompile

lowers a Lean definition to a

FunctionCompile

function.

LeanImport

import constants from a compiled Lean module, returning a

LeanEnvironment

LeanImportString

compile a Lean 4 source string into a

LeanEnvironment

LeanExportString

convert a

LeanEnvironment

back to Lean 4 source

LeanExport

write a

LeanEnvironment

to a

.lean

file

LeanEnvironment

a collection of named Lean constants; supports

,

,

one Lean constant, with

"Type"

,

"Term"

,

"TypeForm"

,

"Parameters"

,

"ExprGraph"

properties

LeanConstant

the raw

name/kind/type/term

record returned by the native shim

LeanExpr

the type of a constant as a symbolic expression tree

LeanValue

the proof or definition body of a constant

LeanConstantInfo

full constant info as a

LeanConstant

LeanListConstants

every constant in a module as an

Association

LeanLoadEnvironment

load a Lean environment handle for repeated queries

LeanFreeEnvironment

release a loaded environment handle

LeanConst

a reference to a declared constant at given universe levels

LeanApp

function application

LeanForall

a

∀

/ dependent function (arrow) type

LeanLam

a

λ

-abstraction

LeanLet

a

let

-binding

LeanBVar

a bound variable by de Bruijn index

LeanFVar

a free variable (local hypothesis or parameter)

LeanMVar

a metavariable (unresolved placeholder)

LeanSort

a universe (

Prop

,

Type

, …)

LeanLitNat

a natural-number literal

LeanLitStr

a string literal

LeanProj

a structure-field projection

LeanNoValue

marks a constant with no body (axiom, opaque)

LeanTruncated

marks an expression cut off at the depth limit

LeanLevelZero

level 0, the universe of

Prop

LeanLevelSucc

the successor of a level

LeanLevelMax

the maximum of two levels

LeanLevelIMax

the impredicative max (collapses to 0)

LeanLevelParam

a named universe parameter (

u

,

v

)

LeanLevelMVar

a universe metavariable

LeanState

open a theorem as a proof goal; holds

"Goals"

,

"Complete"

,

"GoalCount"

LeanTactic

a tactic, applied as

LeanTactic[tac][state]

LeanGoal

a single goal, with

"Target"

and

"Context"

transpile a Wolfram

into a checkable

convert a

into a

with

arguments

compile a

(or whole environment) via

FunctionCompile

LeanCompileTyped

compile and annotate the result with its dependent type

LeanExprToType

translate a Lean type expression into a compiler type object

LeanExprGraph

expression graph for a constant, computed by a Lean subprocess

LeanCallGraph

call / dependency graph for a constant, via subprocess

LeanListTheorems

list a project's theorems via subprocess

ImportDOT

import a DOT digraph file as a styled

Graph

▪

Lean 4 (lean-lang.org)

▪

Mathlib4 (GitHub)

""