Possibly Resolving A Conjecture On Matrix Theory With GPT Sol
Not sure yet though. On a conjecture by Khalkhali, Pagliaroli, Parfeni, and Smith,
A lot of people are writing results on math with AI. I kinda felt left out, because I even though I could’ve asked it to solve some problem X, I wasn’t sure how it would feel ‘real’. Or if I could be confident that it would be right, even if it was. Hell, even if it was formalised in LEAN, the formalisation could be wrong because of how complicated LEAN is. It took a while for me to figure out what would be cool to try, and also feel real in some meaningful way to me.
So I asked GPT Sol Ultra to hunt for some conjectures with resolutions that someone with my background could understand and check myself. Disclosure - I’ve studied theoretical physics up to Master’s level at Cambridge, and the math that I read usually has a statistical physics flavour. I also finished my fourth year with a score of 98/100 (though it was covid and so exams were easier).
One result that it found was a disproof of a conjecture on the limiting behaviour of a matrix model, with a fairly simple proof. The original conjecture is conjecture 2 from the following paper:
Masoud Khalkhali, Nathan Pagliaroli, Andrei Parfeni, and Brayden Smith, “Bootstrapping the critical behavior of multi-matrix models,” Journal of High Energy Physics 02 (2025), 158. DOI · arXiv:2409.07565
The resolution is here, which resolves the conjecture falsely. The full proof is below as well at the bottom of this post. The part which made me feel something was the fact that this conjecture used math that was basic enough for me to grasp it, and I have found the subject matter (field theory, random matrix theory) interesting previously.
I am spending some time to try and check if I got it right. My friend George Smith works on tools for math education and I’m trying to use his generated problems to gain a better intuition of what GPT Sol actually did.
I am well aware of being wrong, so I have emailed the authors of this paper to check to see if it makes sense. Formalising it feels to heavy as a tool right now, so I’ll stick to algebra tools. I will disclose in a later post if I have found that I have made mistakes.
Here are some notes on what I’m looking for when I try to make AI assisted proofs
Find a problem that I can understand.
This feels really important, what’s the point of doing research math if you don’t get the joy of trying to understand something new?
If you choose problems that you understand you will be more likely to somewhat be invested in the solution and also be more likely to take it in a useful place.
The concepts you learn are more likely to mentally hook to something you care about which might make some cool second order effects.
If you choose a problem you understand you will feel good when its solved, which I rate highly.
A lot of results in maths aren’t applicable to real life, the search space is huge, just chill.
Somehow I feel more drawn to math that has some empiricism in scope, or a model of the world that is not obvious.
If you understand more math you are more likely to have an expanded universe of problems that feel significant (and can hopefully solve with AI assistance)
This means that it is still worth trying to understand math.
It feels more likely to me that one part of the future of math is trying to digest results made by AI and trying to see if they have wider significance.
I still think people want to understand things, I still find understanding things fun and knowing how things work is fun. I don’t think it matters if something is already known, there are infinitely many presentations of knowledge that can be valuable in different ways.
I still think there is scope for a much needed, much better thought out way of communicating and storing such results.
Acknowledgements
Thanks to George Smith for the discussions. All mistakes are mine.
Proof
