> I don't follow how the proof text is generated from lean? Or is it not, they are doing the verification in lean and the proof text is completely separate.

My understanding was that the Blueprint tool that he linked is what's responsible for the human-readable math sections shown in the screenshots. I'm not saying it's easy, but it should definitely be doable, basically a spreadsheet like that one on steroids.