[nicf]

I certainly didn't mean to dispute that! Formal proofs have a lot in common with code, and of course reading code is illuminating to humans all the time.

I meant to be responding specifically to the case where some future theorem-proving LLM spits out a thousand-page argument which is totally impenetrable but which the proof-checker still agrees is valid. I think it's sometimes surprising to people coming at this from the CS side to hear that most mathematicians wouldn't be too enthusiastic to receive such a proof, and I was just trying to put some color on that reaction.

[mietek]

Ah, I do agree with this perspective. I think we must ensure that any such tools emit proofs that are not only valid but also readable.

On the other hand, humans do also occasionally emit unreadable proofs, and perhaps some troubles could have been avoided if a formal language had been used.

https://www.quantamagazine.org/titans-of-mathematics-clash-o...