131–140 of 140 posts
Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?
Yes, because if AI can do maths then it can use that to improve the efficiency/quality of it's algorithms to self improve...
I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?
Is it currently possible to reliably limit the cut-off knowledge of an LLM (either during training or inference)? An interesting experiment would be to feed an LLM mathematical knowledge only up to the year of proving a theorem, and then see if it can actually come up with the novel techniques used in the proof. For example, having only access to papers prior to 1993, can an LLM come up with Wiles' proof of FLT?
There's the Frontier Math benchmarks [0] demonstrating that AI is currently quite far from human performance at research-level mathematics. [0] https://arxiv.org/abs/2411.04872
It's just hot air, just like the AlphaProof announcement, where very little is know about their system.
Earlier quoted context omitted.
It's not a theorem prover, it's more like a support system for decision making. They can probably isolate 100k facts from some domain for you if you pay for it, but their idea is to run inference on millions of "common sense" and everyday facts and have been for decades.
That sounds to me like something that will be subsumed by the combination of ITP and AI.
I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
Ok so Claude says that the Riemann hypothesis is proven and gives you 1200 pages of math symbols backing it up. Now what? You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?
The source of truth here is the code we wrote for the formal verification system.
Earlier quoted context omitted.
I guess it is tautological from the definition of "provable". A theorem is provable by definition if there is a finite well-formulated formula that has the theorem as consequence ( https://en.wikipedia.org/wiki/Theorem paragraph theorem in logic)
Not sure it’s a tautology. It’s not obvious that a recursively enumerable procedure exists for arbitrary formal systems that will eventually reach all theorems derivable via the axioms and transformation rules. For example, if you perform depth-first traversal, you will not reach all theorems. Hilbert’s program was a (failed) attempt to determine, loosely speaking, whether there was a process or procedure that could…
Earlier quoted context omitted.
There's the Frontier Math benchmarks [0] demonstrating that AI is currently quite far from human performance at research-level mathematics. [0] https://arxiv.org/abs/2411.04872
They didn't demonstrate anything. They haven't even released their dataset, nor mentioned how big it is. It's just hot air, just like the AlphaProof announcement, where very little is know about their system.
Earlier quoted context omitted.
Ok so Claude says that the Riemann hypothesis is proven and gives you 1200 pages of math symbols backing it up. Now what? You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?
The nice thing about formal verification is exactly that. You have a separate tool that's very much like a compiler that can check those 1200 pages and tell you that it's true. The source of truth here is the code we wrote for the formal verification system.
Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?
Earlier quoted context omitted.
The nice thing about formal verification is exactly that. You have a separate tool that's very much like a compiler that can check those 1200 pages and tell you that it's true. The source of truth here is the code we wrote for the formal verification system.
Could formal verification prove the nexus between the Taniyama-Shimura conjecture and Fermat's last theorem? I don't claim to know what the former is, but I am skeptical that a system that can only validate what we already know would have any luck with sudden leaps between disparate corners of the field. Or worse, what if we had this verification 30 years ago, Wiles gets excited thinking he proved a 300 year old myst…
But that's not how it works; rather it tells you about the specific issue with a particular step in the proof, which you then debug, as you would with code that isn't compiling (or not passing some static analysis test).