Translating term proofs to tactic proofs

Stream: general

[Jiang Jiedong]

Hi everyone,

Is there a tool for translating a term proof to a tactic proof? Of course, one can always just add by exact before the term, but this is cheating. What I am imagining is that if the term is a lambda expression, one translates it into intro, if it contains ▸, one translates it into rw, and the function application is apply, ... So in the end, from a term proof, you will get a tactic proof with lots of apply, intro, and some rw, have, let.

[Yuyang Zhao]

It has been discussed recently, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Tactic.20style.20to.20term.20style

[Jiang Jiedong]

Yuyang Zhao said:

It has been discussed recently, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Tactic.20style.20to.20term.20style

Thank you!

[Jiang Jiedong]

I have no idea how challenging this tacticfy would be, I sincerely hope that this feature can be implemented in Lean.

[Jiang Jiedong]

There's a background story behind my interest in tacticfy. My friends and I have been working on an auto-translation project using LLM to convert mathlib theorems into natural language. We discovered that the LLM performs well on tactic proofs, as the stepwise logic is clearly indicated by the tactic names and the proof states between tactics. However, long term proofs are hard; they are difficult to read even for humans. Therefore, I am keen on developing a tool that can first translate term proofs into tactic proofs, allowing us to apply the same method we used for tactic proofs.