PL/ML people: is there work on "proof summarization"? Ie, given a proof (in coq or lean or something), emit a natural language proof that's human-readable.
Maybe would know?
Conversation
This came up in our proof engineering reading group today and we couldn't find anything about it online. Maybe we were just googling the wrong words. It seems like this has to have been done!
2
4
Alfa used some sort of ‘Grammatical Framework’ thing as a way to describe proofs: web.archive.org/web/2021111601
1
1
Oh woops, it was already mentioned in another thread! 😅
Quote Tweet
Replying to @alpha_convert and @TaliaRinger
I remember hearing the alfa proof editor has functionality for translating proofs to english but haven't used alfa myself to say how good it is at that task