Also, I’m going to nitpick here a little. While proofs “feel” right to me, that’s in part because I’m a math guy. Most people can’t reliably identify a flawed argument.
This was the part i was focusing on. Once you the idea is clear and present in your mind then you find a compelling truth there. While not every person is practiced and educated enough to make the idea clear, once it is then this feeling of necessity seems to be independent of person and culture. The model does not have that.
I agree and am not claiming the creative process of arriving at a proof is deterministic. Although i also do not think such a creative process is probabilistic in the same way that an llm is probabilistic, that is probabilistic.
The better models that are trying to do math are generating proofs and putting them into LEAN, which is a way to formalize and verify the validity of proofs.
It still feels to me like a good chunk of this LLM community is pretending like the Principia Mathematica and Logical Positivism project of the early 20th century succeeded in turning math into logic, and science into logical sentences about simple observations. In other words they are equating reasoning with mechanical inference. But in fact, both of those projects, despite being valiantly led by brilliant people, failed pretty completely.
The proof was confirmed by Terrence Tao, arguably the greatest mathematician in the world. He is skeptical of LLMs as well, but has started a list of their contributions to math all the same.
Again, at this point, I don’t think he would claim the LLM is intelligent either. The proof is not that original, and although the problem is open, that’s in part because it was recently restated.
It’s further complicated because LLMs are still rapidly improving. They change so much from one year to the next, or even one month to the next.
GPT 5.2 was able to solve this problem, but every other LLM until now probably could not have solved it.
We try to make broad statements about how they work, and what they can and can not do, but it’s a quickly moving target.
I studied proofs via his Analysis I and II textbooks in the US (they were quite good).
I don’t see LLMs solving the real complex problems because for those you generally do need original ideas. Right now, an LLM solves a problem by brute force interpolation using past solutions and math papers. None of it is really original.
Reminded me of a cartoon
4 Likes
Hopefully it was clear i was not saying that your post was specifically claiming it was intelligent, either.
I was instead speaking to how it would be talked about by the marketing teams of these LLM companies, at least.
1 Like
I have that one a t-shirt. It’s always a hit with my math students.
1 Like
I agree. Probably, LLMs have more offhand knowledge of existing proofs than anyone, and can research at unprecedented speed and breadth, and can borrow ideas and apply them to open questions. If so, then maybe they will prove many “easy” things, while still leaving space for groundbreaking mathematicians.
I don’t know. It would still be pretty amazing, and perhaps depressing for the many mathematicians. Until this year or so, LLMs couldn’t even talk about math without spewing nonsense. They are now able to apply an old idea to a new problem, and sounds very hard. That they are able to recognize the idea is both useful and valid sounds harder still.
If nothing else, “Brute Forcing” means knowing when you have the right answer. How do they do that? In this case, I believe GPT is not hooked up directly to LEAN, it is verifying its own ideas. Which I get doesn’t necessarily require “intelligence” but does require quite a lot of pattern matching and reliability.
There are “layers” of proofs:
- Convince yourself – least amount of rigor and this is the general goal of most undergrad math programs (especially with applied math as the focus)
- Convince a friend – more rigor involved, but to an audience willing to “give you the benefit of the doubt” on some claims; this is the goal of undergrad math programs that are not “applied math” focused (and the focus of applied math programs at the masters level)
- Convince an enemy – most rigor involved; this is the goal of most masters programs that are not “applied math” focused.
1 Like
I can see LLM’s being able to do the first layer of proofs described in my prior post above as it really doesn’t require “creative thinking” and the general goal of that approach is usually checking what someone else has done/claimed.
I can see LLM’s being able to do some at the second layer where, again, there is often not a lot of “creative thinking” required apart from perhaps novel use of known results/theorems. (This latter part is where LLM’s will fail, IMO).
But that third layer is where I don’t see LLM’s being useful at all since the creative thinking in that space is thinking from the other’s perspective . . . which I have yet to see LLM’s do w/o explicit prompting.
I think the big thing that has changed is the volume of data. The transformer architecture let that happen by allowing calculations to be scaled across many different machines. However, that data is spent. That may not be true for specialized areas but it seems unclear how much that helps.
Also, language is infinite. So is Math in the sense that its possibilities cannot be exhausted with data so that the “uncertainty” in a model predicting the next right word might decrease with the square root of N given the right model.
I am very hopeful for what these LLMs can do for us. But I do not see how it is different in principle from, say, Mathematica. Mathematica can apply integral tables better than any human, ever. We do not call it a super intelligence though. And it did not take away all work, or even much or any genuinely creative and adaptive work. No, it took away work that was mechanical in nature, namely computation.
I’m wondering if this is a harbinger of things to come…
Dell is dropping a bunch of the AI marketing on PCs because consumers aren’t interested.
I know Bell Canada has been pushing Google Gemini subscriptions instead of a streaming service on their cell plans. I’m not sure if they’ve switched back yet.
1 Like
I think AI use by consumers is a long way off. I’ve no idea why a consumer would order an AI centric PC, ain’t nobody running AI stuff locally.
OTOH, commercial applications IMO are going to be very much taking off in the next few years. Applications of LLM’s in particular abound. They just haven’t really penetrated industry yet.
And good news. I found local colo faciliites that will accept a larger server, and I just today ordered our AI server. Gonna start offering AI services in the insurance industry, have some products already ready to go.
1 Like
Yes, I think for 99.99% of people, buying an AI PC makes no sense at all. Even if you love and use AI constantly. The cloud is going to be easier, cheaper, and better almost always.
I haven’t looked at the sales, but it wouldn’t surprise me if they cross marketed with higher end gaming pcs. Either way you would want a $2,000 GPU. Might as well say, “also it does AI” but not very well.
I also don’t think many people need a subscription when they could just use free versions. Certainly less than they want TV.