Comment by mietek
18 hours ago
A proof written in a formal language can absolutely be illuminating to a human, but you have to pick the correct formal language and ecosystem.
Writing proofs in Agda is like writing programs in a more expressive variant of Haskell. Abelson said that “programs must be written for people to read, and only incidentally for machines to execute”, and by the Curry-Howard isomorphism, proofs can be seen as programs. All the lessons of software engineering can and indeed should be applied to making proofs easier for humans to read.
For a quick example, check out my mechanization of Martin-Löf’s 2006 paper on the axiom of choice:
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.
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...