There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could automatically translate the steps into something resembling a natural language proofs.

In some cases, it seems like it would be relatively easy to do this translation. For instance, in many cases where apply is used in Lean, the natural language is something like "since we are trying to prove this statement, and we have this that the antecedent implies the statement, then it suffices to prove the antecedent".

On the other hand, some things might be more difficult! For instance, how would such a translator unpack statements made using anonymous constructors?

Has there been any work done on this, and would it actually be useful?

  • 2
    $\begingroup$ Not quite what you are asking for, but there is a style, maybe more common in the Isabelle/Isar world, where you are a bit more explicit in your intermediate steps, and use opaque tactics only for what would be trivial in a human readable proof. But it's maybe a bit the antithesis to the kind of proof golf done in mathlib. $\endgroup$ Commented Feb 12, 2022 at 22:16
  • 1
    $\begingroup$ I have to say, I very much enjoy the “proof golf”, but it does obscure the ideas of the proof. What I’ve noticed is that I can prove a statement without really knowing how to proceed because the tactics really do help suggest the method to generate the tactic proof but not the method to generate a forward proof. It would be nice (maybe as a pedagogical tool at least) to have something that can translate the tactic proof into something that resembles the “by hand” proof. $\endgroup$
    – march
    Commented Feb 12, 2022 at 23:36
  • $\begingroup$ I haven’t tried anything other than lean yet, but I find the automation and backwards style tactic proofs useful, so instead of generating forward style proofs in the proof assistant, I want to generate tactic proofs and then back convert them to forward real language proofs. $\endgroup$
    – march
    Commented Feb 12, 2022 at 23:39
  • 4
    $\begingroup$ Since the question is specifically about Lean, I will just leave it as a comment: I have written a prototype proof assistant that renders all proofs in the way you describe, e.g.: slate-prover.org/libraries/hlm/Essentials/Numbers/Real/…. This could potentially be adapted for Lean, but currently relies on proof terms that are especially optimized for this purpose (click button at bottom right to see the proof source code). $\endgroup$ Commented Feb 20, 2022 at 11:57


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.