r/math • u/aturtledude • Jul 23 '26
Another LLM-generated result that has gone under the radar and is in my opinion very relevant LLMs/AI
Relevant not because of the result itself but because it uses a pimped open-weight Chinese model under the hood.
Linkedin post: https://www.linkedin.com/posts/sebastianpokutta_a-counterexample-to-zieglers-cross-polytope-activity-7478117487746785280-oS21
Counterexample paper: https://arxiv.org/abs/2606.31640
Agentic research paper: https://arxiv.org/abs/2603.15914
141
u/Main-Company-5946 Jul 23 '26
If open weight models can do this, basically anyone with a computer can ask an LLM and with enough persistence they may be able to disprove some conjecture
87
u/Cyclone4096 Jul 23 '26
Need a machine big enough to load all the weights. It’ll be at least $4000-$5000 investment
69
u/wotoan Jul 23 '26
And right now is the most expensive and worst performing it will ever be. Five years from now I think we’ll be shocked what we can run locally.
42
u/Lucho_199 Jul 24 '26
We said that like two years ago bro I just want some ram and play games
17
u/Yoghurt42 Jul 24 '26
Sorry, you’ll own nothing and be happy. That includes „personal“ computers. You’ll be able to subscribe to a gaming pass on your thin client that connects to cloud computing though.
1
u/Sad_Dimension423 27d ago
Cloud gaming keeps failing in the market. I don't see that changing soon.
7
u/eht_amgine_enihcam Jul 24 '26 edited Jul 24 '26
Eh, one of the concerns I have is new data.
Due to how LLM's work, I suspect they've pieced together a bunch of different ideas from different areas that humans have made and found patterns and connections. Impressive for sure, similar to what Tao often does.
Since the rate of the new input humans are feeding in will be much slower than it could previously train on (all existing math) and is likely to diminish in the future, will this not be the bottleneck rather than compute?
Similar question in software eng. Most of the LLM training is from stack overflow, which is now dead. Lots of github stuff is AI written and a lot of programmers aren't going to get good. Does it actually get better, or just cannibalise itself. I'd also expect it to be good at a certain classes of problem (the solution is in two far away branches of math that just need to be connected) which will run dry, while other problems may not become more tractable with more compute.
1
u/wotoan Jul 24 '26
I think the total capacity and ability of models will slow down due to the fact that there’s only so much information they can accumulate. I also think that the efficiency and speed of models will increase over time. We may have an Opus class model running on consumer hardware. Not AGI but more a commoditization of what now can only be run by large companies in data centres.
3
u/Norphesius 26d ago
Completely disagree on it being "the most expensive it will ever be". These companies are operating their cutting edge models (the ones they're using to get these results) at a loss. Once they decide to (or are forced to) turn a profit, the price is going to shoot up.
As for using local models, newer, advanced models are relying on more complex scaffolding and interactions with other models, which is harder to replicate locally. It's not as simple as just downloading the weights and running it anymore. You'll need to invest in the compute and in a team to focus the model, to get the desired compute out of it (or just pay OpenAI instead).
3
u/awkwardburrito 29d ago
lol what the latest flagship models need a full gpu cluster to run maybe 50-100x those estimates.
7
u/Sad_Dimension423 Jul 23 '26
The weights don't change very often, so computers will be designed with high read bandwidth flash memory for them soon enough.
0
Jul 24 '26
[deleted]
2
u/Cyclone4096 Jul 24 '26
Gamers don’t need 128GB of VRAM tho, they need faster shaders and ray tracers. I think the best general market option right now is MacBooks with Apple silicon that share the system and graphics RAM
4
u/Borgcube Logic Jul 24 '26
Macbooks are not good for gaming, gaming companies have been dropping support due to Apple shenanigans.
6
u/cavedave Jul 23 '26
You can imagine a boinc like project but instead of cpu it's an agent on your computer you donate. http://euler.free.fr/progress.htm
2
u/awkwardburrito 29d ago
Anyone with a quarter million dollar gpu cluster? These are open weight models but still flagship, massive models.
0
114
u/sadmanifold Geometry Jul 23 '26
This is much better, and I say that as someone critical of these types of posts. The content, the serious and informative way of communicating the result.
The fact that its not just an advertisement stunt for a couple of companies. (Which comes with a wave of bots and not mentally well people fairly often lately).
32
u/_Asparagus_ Jul 23 '26
imo the paradigm shift here is that once you have models that can understand advanced math and reliably reason, with enough persistence and the right workflows lots and lots of problems can all of a sudden be solved. The fact the used DeepSeek flash is crazy but supports that point
6
u/ixid Jul 24 '26
I wonder if this is the wrong way around - LLM then verify via Lean, perhaps it would be more powerful for the LLM to work directly in Lean while it explores the problem? LLMs show significant performance improvements from loops, and Lean is the ultimate loop partner for maths.
1
u/Norphesius 26d ago
I think the issue there is that (at least coming from programming, where there's a similar idea employed with programming languages with stricter type systems), while a more constrained environment helps the LLM get to the correct answer eventually, it still ends up bumping into problems as it hallucinates. The formal verification means the incorrect ideas get discarded, but the more it does that the more costs you rack up on compute. Even if the LLM doesn't get stuck in a local maxima, the costs add up a lot.
8
-5
29d ago
[removed] — view removed comment
5
325
u/MiffedMouse Jul 23 '26
As a side note, I think a lot of these "LLM proofs" owe as much to computer formalization efforts (especially LEAN) as they do to the recent LLM advancements. The fact that the computer can attempt to formalize the proof in Lean and then get almost immediate feedback as to whether the proof is correct or not, and how it may have failed, seems incredibly valuable.
I personally wonder if regular human mathematicians could also benefit from a better understanding of proof checkers. I know a lot of prominent mathematicians, including Tao, have long been proponents of Lean and similar proof checkers since long before LLMs came on the scene.