Comment by vld_chk
3 hours ago
I am not a mathematician, but I can’t see how we are going to address the problem which we already see in coding:
Impossibility to independently validate all AI results
And in math it goes even worse. In coding code reviews are typically still the form of action you do within days. In math, historically, the lifecycle of proof is months if not years. Take as an example Millennium problems. They require at least two years of validity after publishing. Two years! In modern times with amount of output AI can produce, it feels like infinity.
We are inches close if not at the moment already when humans can’t reliable validate proofs and mathematics produced by AI. Then next research will be based on this AI-written-no-human-in-the-loop results. And we will end up in just few years in a world where novel and frontier problems will be articulated by AI and proven by AI based on AI results and humans will be incapable of understating the mere nature of the solution.
I don't think that's actually the real problem. Along with the progress in answering mathematical questions, recent progress on AI-powered autoformalisation has been astonishing. All the recent AI discoveries have been accompanied by Lean proofs.
And, yes: that doesn't absolutely guarantee correctness. The Lean kernel has had soundness bugs, and may have some still. But it's pretty strong evidence of correctness nevertheless.
The concern among mathematicians is not mainly that they doubt the correctness of any of these discoveries, but that human understanding may be devalued.
I am not that worried, but rather just observing. Humanity is about to enter the phase when we will be using things based on ideas no human ever properly understands. This thought … disturbing, somehow?
It is perfectly valid counterpoint to say that we already do it. We everyday use myriad of things, tools, and software we have 0 clue how it operates. But for us as humans it was reassuring that we know that at least there are a few other alive humans who know it, who create it and who can explain it.
With AI soon that comforting zone will be gone.
>Humanity is about to enter the phase when we will be using things based on ideas no human ever properly understands. This thought … disturbing, somehow?
This is just normal though. We were building sophisticated bronze and steel tools long before any complex understanding of metallurgy or chemistry. Medicine is still the wild west.
1 reply →
>Humanity is about to enter the phase when we will be using things based on ideas no human ever properly understands.
Do any one person even understand the humble pencil?
https://dn790006.ca.archive.org/0/items/i-pencil-pdf-2019/I%...
But one of the things AI also excels in is summarizing and can do so hierarchically. One of my favorite things to do with a concept I'm new at is "ELI5" then "explain like I'm a high school student" then "explain like a bright undergrad in XYZ" then "explain to a working professional in this domain". It's a lot of steps, but I've found it very effective (for me) to learn with -- and I've done something similar with code and math (although not math proofs -- I'm not a mathematician). But my point is that I think we can use AI to also teach us these proofs they're building in a way that I don't understand today about human proofs.
If we use AI well here we could actually understand math much better than we do now.
I actually think it's the opposite: Lean proofs and autoformalization make it very easy to announce proofs alongside proofs of the correctness of those proofs (Lean certificates). It's not an absolutely fool-proof combination (the Lean kernel could still contain bugs), but it does immediately attach a very substantial degree of credibility to the result.
And that I think is essential to why some of the world's leading mathematicians are taking this so hard. In a world where we "merely" have AI systems capable of superhuman informal reasoning, verification, correctness, and acceptance could still only be conferred or anointed by human mathematicians. But a world that combines superhuman informal reasoning with superhuman autoformalization is a fundamental shakeup in the institutional order.
The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.
That seems like a red herring. Have you independently verified the human generated proof of FLT? Surely someone else will try to verify Anthropic's formalization on different hardware. Plus, it seems likely that FLT formalizations will improve / get shorter over time, requiring less compute. And computers (and type-checkers) will continue to get faster over time as well. So maybe in 5 years you could own a computer fast enough to verify a/the proof in say a week, instead of 5 hours.
With formalized math, you only need to validate the problem statement (in theory, in practice agents have already managed to exploit Lean compiler bugs, but the incidence of those should decrease enough to be practically lusable for 'blind' validation of AI proofs in the foreseeable future).