Comment by WheelsAtLarge
20 hours ago
I have very little understanding of higher math, so I ask you: Was the proof due to a type of brute-force solution that could be solved had you gained enough information from reading others' work, or was it more like a proof that was sparked by an insight that came once a clue on how to solve it was put forward? I guess my question is: Was the problem proven by using a collection of everyone's work, or was it due to a brand-new insight?
I'm still digesting the proof and translating a bit from the dual case back to the primal in which I most commonly thought about it. I don't think it was a brute force proof in the sense that it combined every possible paper and commentary. It's rather odd because I feel like most of the work on the conjecture was focused on an induction proof based around graph reductions, and this proof avoided those issues entirely by offering a concrete constructive proof of finding a Hamiltonian cycle. Rather, it explicitly selected the edges not in the Hamiltonian cycle, which is in line with previous attempts via the dual.
The "aha" insight for this is actually f**ing wild, it involves a complex valued exponential sum on the edges. I've seen a lot of clever counting arguments before in graph theory but this is the first time I've seen complex roots and annihilating terms like this, the symbolic manipulation tricks in this look like things out of quantum physics. I don't understand where this trick originated, I need to really digest this.
You should try asking an LLM to look for previous papers using similar ideas. The current/frontier generation of math AI is unfortunately very bad at citing the relevant literature for techniques its using.
I asked GPT here: https://chatgpt.com/share/6ac5fd7d-0390-83ed-a02a-6d80fc64f6... and it says:
> the exact Barnette argument appears quite novel, but nearly every ingredient in its cancellation trick has a recognizable ancestor.
> The closest precedent is much closer than I expected: in fully packed O(n) loop models, people have been assigning complex phases to the two orientations of a loop and making them cancel for decades. At n=0, the phases are literally +I and -I. And the n->0 limit has specifically been used to extract Hamiltonian cycles/walks.
You can judge better than me. But it's definitely worth it having a research assistant AI with you when reading these papers.
So much about LLMs can be framed as Information Retrieval, Compression, and Search. Computers have always been good at ruthlessly hammering through a huge but finite set of possibilities. The wild thing now is that you can define that set of possibilities as "all the ideas ever published in mathematics journals."
It makes solving advanced math problems feel like cracking a hash. If it's possible, it's just a matter of compute time.
BTW, reading your last paragraph reminds me of how Lee Sedol felt after move 37.
Ironic, as I remember staying late at the Google office to watch that match live. I didn't really understand anything going on but I knew enough to be excited. What a decade.
1 reply →
I just revisited this to make that exact comment.
I'm sympathetic to the mathematicians who are worried about the future of their field, but as an outsider I wonder if they couldn't learn from the go community's "recovery" after the introduction of an alien intelligence.
1 reply →
Complex roots and annihilating terms -- is it something like the derivation of Fourier / Laplace transform?
WOW
Why would the trick have any "origins", isn't this model creating new techniques never before seen or imagined?
There is a chance that someone from a completely different field came up with a solution for a tiny part of your problem.
If you can remember the content of any scientific publication and any book in the world, you are able to make use of this knowledge in every step of you proof.
However, this does now answer how the model came up with the specific route it has taken for the proof.
6 replies →
As I understand it it's undetermined yet whether LLMs can actually come up with anything novel or are instead pulling from their incredibly deep corpus of knowledge to present solutions that were there but we didn't realize it because our brains aren't libraries of almost all human writing.
15 replies →
Let me introduce you to 'obscure Russian mathematicians'.
> Was the problem proven by using a collection of everyone's work, or was it due to a brand-new insight?
Loaded question. A "brand-new insight" is still built off the work of others. A possibly better way to frame it would be in how many subjectively unintuitive logical leaps have been made from prior work.
From my current understanding (and a lot of theoretical physics I'm having to Google because the sentences I'm reading from Fable's analysis are so bizarre I think they are hallucinations) there are possibly 3 neat symbolic tricks borrowed from theoretical physics that make the heart of this proof. Forgive me for posting LLM output but I find this darkly hilarious:
"it's a matrix-tree cancellation wearing Kasteleyn's planar signs, run as a Witten index over Penrose-lineage states, evaluated as a fugacity-zero loop gas in an infinitesimal magnetic field — and the reason it reads like physics is that every one of those tools was built for partition functions"
I thought this was pure slop when I read it but there are some clear analogues in these other areas of physics, really neat computational tricks, and a very interesting paper by Penrose calculating Tait colorings I never knew about previously (extremely relevant, actually related to a separate approach I had once taken on this problem). The problem is that the paper isn't saying "aha, we were inspired by the related problems of pairing excited states and creating spanning trees out of cancelled coefficients" it just defines the function apropos of nothing. Which is kind of like the Jacobian counterexample in that it works but doesn't really explain how exactly it got there.
I really think the load-bearing concept here is "prior work". If prior work is considered papers on this problem or graph theory, yes this has one huge subjectively unintuitive logical leap. If "prior work" is the entire corpus of neat computational tricks that physicists derived to make their equations spit out something other than zero or infinity, maybe it's not so crazy?
I don't have much to add to the math parts, but I've read all your answers in this thread and wanted to thank you for taking the time to offer a detailed perspective from a subject matter expert. Thank you!
Actually reminds me of patent law. Prior art ist a defined term which includes all standard literature on one topic. To evaluate, whether the new solution is really inventive and thus patentable, one consults prior art, selects the most promising starting point, and from there asks oneself if an all-knowing but uncreative specialist would come up with the solution by himself. If he wouldn't, the condition of inventiveness is satisfied.
Makes me wonder how the patent space will be disrupted when that inventiveness step becomes obsolete because of LLMs. Given your example above, it seems like a combination of different methods from many different sources. This would be regarded as inventive, clearly. If eligible patents can now be brute-forced, the bottleneck becomes only selecting the most promising ones and paying for the patent.
1 reply →
Did anyone else wince at seeing the phrase "load-bearing"?
4 replies →
Kasteleyn signs definitely have math counterparts (Arf invariants). They’re just not as well-known.
2 replies →
It's a shame OpenAI will never publish the trace that led to the insight.