[mietek]

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:

https://research.mietek.io/mi.MartinLof2006.html

Recent HN discussion:

https://news.ycombinator.com/item?id=44269002

[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...

[daxfohl]

I see axiom of choice, and really LEM, as logic's equivalent to limit points in calculus. No, you can't calculate 0/0, but here's what the answer would be if you could. No, you can't prove the truthiness of this statement, but here's what it would be if you could.

I guess one could work in a brand of math whose axioms make defining and using limits impossible, which, maybe if formalization came before the invention of calculus, would make some 17th-century mathematicians feel more comfortable. Though I imagine it would make progress in physics challenging. I think the same about LEM/AoC. Given that almost every element in the power-set of reals is non-measurable, maybe stuff like Banach-Tarski is actually fundamental in real physics: it can't be predicted or computed, but it can be observed.

[riku_iki]

I would argue is that some portion of ecosystem should be readable by humans.

In programming engineering we already have this: there is human readable high-level code, and there is assembler and lots of auto-generated code.

In proof system we could have the same: key concepts/theorems should be encoded in human readable form, but no need for human to read through millions of generated lines.