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!