Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Lean 4 from the Wolfram Language
Wolfram`LeanLink`
LibraryLink
Importing and exporting
compile a Lean 4 source string into a ; with it can import a built project
"ProjectDir"
build a Lake project's modules with its pinned toolchain
Environments and terms
one Lean constant, with , , , , , , , properties
"Type"
"Term"
"TypeForm"
"Axioms"
"Module"
"Source"
"Parameters"
"ExprGraph"
Querying a loaded environment
the type of a constant as a symbolic expression tree
the proof or definition body of a constant
load a Lean environment handle for repeated queries
release a loaded environment handle
Expression heads (CIC)
a reference to a declared constant at given universe levels
function application
a bound variable by de Bruijn index
a free variable (local hypothesis or parameter)
a metavariable (unresolved placeholder)
a natural-number literal
a string literal
a structure-field projection
marks a constant with no body (axiom, opaque)
marks an expression cut off at the depth limit
Universe levels
the successor of a level
the maximum of two levels
the impredicative max (collapses to 0)
a universe metavariable
Interactive proofs
Transpiling Wolfram proofs
The TypeTheory proof engine
import Lean constants into the Wolfram Language proof engine , whose own kernel checks them again
write a TypeTheory proof as Lean source, for Lean's kernel to check
Compiling Lean to native code
Out-of-process project queries
expression graph for a constant, computed by a Lean subprocess
call / dependency graph for a constant, via subprocess
list a project's theorems via subprocess
""