Basic Examples 
(4)
 

Load the bundled example environment:
In[1]:=
env=
LeanImport
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]]
Out[1]=
LeanEnvironment
Constants: 32
Kinds: 18 theorem11 def2 constructor1 inductive

_________________________________________________________________________________________________________________
How many constants, and of what kinds:
In[1]:=
env=
LeanImport
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]];​​Length[env]
Out[1]=
32
In[2]:=
Information[env,"Kinds"]
Out[2]=
theorem18,def11,constructor2,inductive1
_________________________________________________________________________________________________________________
A single constant is a
LeanTerm
summary box:
In[1]:=
env=
LeanImport
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]];​​env["id_proof"]
Out[1]=
LeanTerm
Kind: theorem
Name: id_proof

Its type, pretty-printed as Lean source - the proposition it proves:
In[2]:=
env["id_proof"]["TypeForm"]
Out[2]=
∀ (P : Prop), P → P
And the proof term:
In[3]:=
env["id_proof"]["TermForm"]
Out[3]=
fun x hp => hp
_________________________________________________________________________________________________________________
Every expression is a tree;
"ExprGraph"
draws it:
In[1]:=
env=
LeanImport
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]];​​env["id_proof"]["ExprGraph"]
Out[1]=
"CallGraph"
shows which constants a proof depends on:
In[2]:=
env["or_comm_proof"]["CallGraph"]
Out[2]=

Scope 
(2)
 


Applications 
(3)
 


Properties and Relations 
(1)
 


Possible Issues

◼
  • The native bridge needs the platform shim under
    LeanLink/LibraryResources/
    and the Lean toolchain it was built against (
    leanprover/lean4:v4.30.0
    ) installed via elan: the ~190 MB Lean runtime is not bundled, so on first use LeanLink links
    libleanshared
    from that toolchain next to the shim. Install it with
    elantoolchaininstallleanprover/lean4:v4.30.0
    . Mathlib import and the out-of-process graph functions (
    LeanExprGraph
    ,
    LeanCallGraph
    ) additionally need
    lake
    on
    PATH
    and a built project -
    LeanImport
    of an unbuilt module returns an empty environment.
    • ◼
  • LeanCompile
    's dependent-type path (Vector-sized signatures via
    TypePi
    ) requires a forked Wolfram compiler; the non-dependent path works against the stock compiler.
    • ◼
  • A type shown in isolation can print an unresolved bound variable as
    #0
    /
    #1
    ; the full-theorem
    "TypeForm"
    resolves binder names.

    • Neat Examples 
    (1)
     
    