Comment by gaigalas
2 days ago
Is it trivial for any mathematician to understand lean code?
I'm curious if there is a scenario in which a large automated proof is achieved but there would be no practical means of getting any understanding of what it means.
I'm an engineer. Think like this: a large complex program that compiles but you don't understand what it does or how to use it. Is such a thing possible?
It's not trivial for a mathematician to understand Lean code, but it's something that's possible to learn to read and interpret in a day (without then necessarily being proficient in how to write it).
That's true though of Lean code written by a human mathematician.
AI systems are capable (and generally even predisposed to) producing long and roundabout proofs which are a slog to decipher. So yes the feeling is somewhat similar at times to an LLM giving you a large and sometimes even redundant-in-parts program.
With very difficult human generated proof, it's common that it take like 10 or 20 to make it understandable for mortals. The idea is to split the proof, create new notation, add intermedite steps that are nice, find a simpler path. It's like refactoring.
Sometimes the original proof is compleyely replaced, bit by bit, until there is an easy to understand version.
Too late to edit:
"10 or 20" -> "10 or 20 years"
Wow!
If curl developers are overwhelmed by AI PRs, imagine how mathematicians will feel verifying a huge backlog of automated proofs.
Or isn't there such a thing? Can someone make a very complicated automated proof that ultimately reveals itself to be useless?
2 replies →
[dead]
There's a couple of problems that were solved that way a while ago, and they have been formalized, but not in Lean:
https://en.wikipedia.org/wiki/Four_color_theorem
https://en.wikipedia.org/wiki/Kepler_conjecture
[dead]