This video is making me sad. Any (rational) consolations?

No clue, but it doesn't really surprise me. Since math is a completely abstract system, it makes sense you can brute force solutions. AI's been beating us at chess for a decade at least.

I'm curious if AI "knew" it found the solution, or if it spit out multiple plausible solutions that needed to be vetted by a human. I'm guessing the latter.

The only thing that's new or special here is the "AI" grifting.

Mathematicians literally invented computers and have used them to do math since then. A primary goal of computational mathematics has always been computation, proof writing, etc. It's no surprise at all that these tools would improve alongside growth in compute availability. It's worth noting that certain problems are more susceptible to computational methods than others. For example, people have made a big deal about solving certain "Erdos problems" but (1) dude made up thousands of problems, (2) nobody cares about most of them, and (3) many of his problems are ripe for computational methods. There were no computers in his day, so it's no surprise that many of his problems would eventually be computable. Would we ever expect a human to outperform a computer when it comes to arranging a huge grid of dots? Not any more than we would expect a human to out-multiply a calculator...

Perhaps most importantly there's absolutely zero "AI" involved in any of this. These computer programs are no more intelligent than a calculator. "AI" doesn't exist. It's a huge fucking grift.

I'll leave it at that for now...

I have some math background so have a little insight here, although I don't have the specifics you might be looking for. This ended up long.

So, there's math software that's been in longterm development for proof verification, such as Coq and Lean. I did read pretty recently that multiple big results were announced proven and verified by one of these, but on human review the AI had exploited undiscovered bugs in the prover. Automating theorem-proving has been in development for a long while as well, and is (was?) often referred to as AI although is definitively not an LLM.

With that out of the way, whether by LLM or otherwise, legitimate computer-generated proofs are having a lot more success. The caveat is that they're not innovating and my understanding is they're not expected to anytime soon. I'll explain what I mean by that, although you might be able to guess.

Different disciplines and subdisciplines have different tools and strategies used as go-tos. If I'm doing categorical homotopy theory and I'm looking to find an appropriate model structure on some category, maybe my category has certain features that would suggest my first attempt start with a transferred model structure from a model category which admits an adjunction to mine. A computer with access to all existing math literature can make these connections, that this approach is used often in this situation.

Like any subject, math literature is absolutely enormous. There have been instances of teams of mathematicians, people who have devoted lifetimes to understanding existing literature for a single subdiscipline, working together to prove a result for a new paper, and after publication someone from an adjacent subdiscipline reads it and comes out of the woodwork to point out the journal where their result was first proven forty years back as a lemma used in getting another result. Computers can access all of this literature at once.

This leaves a ton of room for computers to play connect-the-dots in a much more exhaustive way than mathematicians with knowledge limitations can. We want to prove X, well Y technique is a common approach, we'll need to prove Z to get there, W technique would be where to start... but if Z was published in some obscure journal as a corollary to a little-known result from a seemingly unrelated discipline, a researcher won't know that, and won't know that this result somehow fell out of matroid theory instead of algebraic topology, which would have indicated who to collaborate with.

A computer can also go much much further down rabbit holes that look not worth digging into to a human solely based on inconveniencing people. If I need to ask a graph theorist and she says we need to understand more about finite group theory, and the group theorist takes time to think before saying more knowledge of K-theory would help, and all of this ultimately ends up going nowhere, I'm going to feel pretty silly for taking time from all these people and they might give me less time in the future when I might be more desperate. The computer doesn't take consideration of whether this is a hassle, it just explores.

The common tricks and tools of a trade weren't always there though. Someone has to be the first to realize that taking homology is extremely effective in the contexts I'm working in. Someone has to be the first to say the objects in the dual to the category of rings can be viewed as locally ringed spaces, lets try doing algebraic geometry by gluing rings together analogously to how open balls glue together into manifolds. Someone has to come up with the concept of a ring as a mathematical tool. I don't think computers are anywhere close to that.

Computers becoming good at connect-the-dots could still devastate mathematics as a profession though. A mathematician can make a living by knowing the literature of a hyperspecialized subdiscipline better than anyone else. That knowledge means he needs much less new knowledge to make easy "connect-the-dots" in his specialty. The more practice he gets doing that though, the deeper his understanding grows. Deep insights typically don't come from thinking better thoughts than everyone else, they come from an intimate understanding of what you're looking at. Removing all the low-hanging fruit removes a lot of the incentives for a professional to start understanding a discipline better. Grothendieck doesn't revolutionize algebraic geometry without spending a ton of time doing algebraic geometry first, and being able to publish while getting your feet wet doesn't hurt with that. If publishing math is my living, why am I going to spend years researching a discipline when people who spent lifetimes doing that couldn't crack the remaining problems? I'll need to accept that the time investment probably won't help me make a living. Being a grad student today must be a nightmare.

We've always understood all these different branches of math are all deeply connected, but I have to think limitations of how much one human can learn have prevented us from grasping just how deep. It's conceivable that a computer could string together a chain of thousands of very straightforward logical steps pulling from all corners of literature to solve a millennium prize. It would be the analogue of a computer solving an enormous maze by brute-forcing every possible path, while a human would never have the patience to spend that much time on an approach requiring zero intelligence. Evangelists lacking the background needed to comprehend the problem would declare human ingenuity obsolete against the sheer brilliance of the brute-forcing machine.

In a perfect society, math would be enjoyed as an art and could be pursued as an art without necessity to break new ground regularly to prove your worth. In a perfect society, math in academia would be driven by a desire to learn and do math. If being credited weren't important, mathematics would still thrive alongside advances in automated theorem-proving. Time investment is the requirement for deep breakthroughs, and there are definitely those of us who would love to invest time into learning without the pressure to be credited with successes. We don't live in a world where academia is about learning. It's hard to picture the profession staying the same as long as academia functions as an economic gatekeeper instead.

I’m no math. But all the behind the scenes crap behind stories like these read basically like this:

“Hey computer. We all think the answer to this theory is this [Whatever the fuck]. Is that true?”

“Wow. I checked and you’re totally correct. Everything in that theory points to [Whatever the fuck]. You’re cool for noticing.”

I've read a few of these "results." Often goes like this:

"We fed our problem into the LLM and carefully analyzed the pages of results. It was largely bullshit that didn't work, however it gave us an idea that we decided to pursue..."

I'm not actually seen any real stories about these systems solving anything in mathematics or computer science of value directly. Not like a human. For most of them it sounds more like inspiration. And, frankly, these models are decent(ish) regarding pulling information together that may be related. Statistical correlations are what they do.

And for us as researchers, that certainly can bring inspiration. I can't possibly know every single word or idea in some of the areas I study. LLMs don't either, but just pulling related things together can be helpful.

But, no, I've not seen results created directly by such a system that held water without his man intervention yet.

BTW, Your mental state should not be connected to the success of any computer tool. That's all these are is a tool, with lots of flexibility but dubious utility. The biggest things that bother me about them are social, political, and financial.

https://www.scientificamerican.com/article/no-ai-didnt-just-solve-the-thorniest-problem-in-math/

Very simply:

Ai is just very fast at generating bullshit. And sometimes it hits something that works.

Given the right tools this can be quiet helpful. Using big massiveLLMs for it is not acceptable in my opinion. That is just a waste of resources