@tao

I think if humans would ever want to read these formalizations, then one would need to go through the proofs one by one and make the kind of manual optimization and streamlining that you also show in the middle of the video.

At the moment the "interface to human math" in my project are only the statements. I cannot assess how unnecessarily complicated the proofs are. I only ever look at the definitions and statements.