Code For Patrick Massot's Lean Informal Demo

Stream: Is there code for X?

[Frederick Pu]

Does anyone know if the code used in this video to generate informal proofs from lean4 code is available: https://www.youtube.com/watch?v=tp_h3vzkObo&t=1897s

[Kevin Buzzard]

@Kyle Miller is the ball in your court here? I would also love to see this available more widely.

[Julian Berman]

Is it not https://github.com/PatrickMassot/verbose-lean4/ ?

[Frederick Pu]

Julian Berman said:

Is it not https://github.com/PatrickMassot/verbose-lean4/ ?

I don't think so. Patrick Massot's demo converts raw lean4 code into natural language. Lean verbose seems to be simply a macro wrapper for regular lean4 tactics and definitions.

[Johan Commelin]

I'm not sure "simply" is the right word. But yes, it's a different project.

[Patrick Massot]

Lean verbose is quite a bit more than a wrapper. But it is indeed much simpler than informal Lean and going in the opposite direction.