Lean to natural language

Stream: general

[Vasily Ilin]

I can't remember the name of the tool that converts a Lean proof to natural language. I think it used some hardcoded rules like "It follows that" and produced an expandable HTML.

[Jason Rute]

Are you thinking of this talk by Patrick Massot?: https://youtu.be/tp_h3vzkObo

[Vasily Ilin]

I think not. I think it was something more basic, no AI.

[Vasily Ilin]

Actually, I think it is exactly what I was thinking of, thank you!

[Brando Miranda]

Vasily Ilin said:

Actually, I think it is exactly what I was thinking of, thank you!

@Vasily Ilin I am also interested in obtaining english proofs from lean proofs. Is there a simple github package I can check out or extension in vscode? What concretely is the usuable tool or research report form this direction?

[Kyle Miller]

I'm working on making it available, and I'll be sure to post it here once it's up.

[Miguel Marco]

Do you have any expected timeline?