Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
ProofToLean  |
|
| | ||||
▪
proof is a such as the result of . Each premise becomes an , each derived step a with a tactic proof, and the goal the theorem.
axiom
theorem
"FinalGoal"
▪
Types are carried as expression trees; step proofs are emitted as Lean tactic blocks (, , , ). The result therefore round-trips through into compilable Lean source.
have
conv
simponly
exact
▪
Because the transpiled environment is real Lean, you can re-check it - opening the with and confirming it auto-completes verifies the transpilation.
"FinalGoal"
▪
A step of the proof with no translation to Lean yet, such as a substitution rule an axiom gives, leaves the theorem it proves with the proof , and says which theorems those are.
sorry
Examples
(4)
Basic Examples
(1)
Transpile an equational proof:
In[1]:=
proof=FindEquationalProof[ac,{ab,bc}];leanEnv=
[proof]
 | ProofToLean |
Out[1]=
LeanEnvironment
 |
|
The generated constants - premises, derived step, and goal:
In[2]:=
Keys[leanEnv]
Out[2]=
{Ax1,Ax2,Hyp1,SL1,FinalGoal}
The final goal's type:
In[3]:=
leanEnv["FinalGoal"]["TypeForm"]
Out[3]=
∀ (a : U) (c : U), a = c
Scope
(1)
Properties & Relations
(1)
Possible Issues
(1)
 |
|
 |
|
""