The opening is an in-depth, technical analysis of a geometry proof by AlphaGeometry, the summary begins at 18:16.
Alex admits that he's not a Computer Scientist and props to him for acknowledging his limitations on this subject (rare nowadays, people tend to assume that, because they can use a computer, they intuitively understand CS which is just not true.) Fortunately for Alex, CS backs up the opinions and intuitions he expresses here.
It would be possible to make AlphaGeometry produce more human-like geometric proofs. When we work out new proofs or new knowledge of any kind, our notes look a lot like the "chicken-scratch" mess that AlphaGeometry produces. But then we do a second, editorial revision, to clean up our notes and present a reasoned argument from beginning to end. AlphaGeometry also does this, but it's just not very human-like in its presentation. So, you could use fine-tuning -- RLHF, DPO, human-preference ranking, etc. -- to make AlphaGeometry produce geometric proofs that are more in the style that humans prefer to read and write them. In other words, Alex's criticism on this point, while completely valid, is currently solved with existing methods, it would just be a matter of implementing it.
But on the wider implications of AlphaGeometry to mathematical proof-search, generally, this is where Computer Science comes back into the equation. Yes, there
are problems that cannot be solved, even by AI. It doesn't matter how "incepted" your AI is, it doesn't matter whether it trains itself, rewrites its own code, self-improves itself, etc. It doesn't matter how much energy the AI has access to, nor what frequencies the AI operates at. The entire observable universe can be devoted to the use of an all-consuming, black-hole-scale AI operating at trillions of times the gigahertz frequencies of modern CPUs, and it
still won't be able to solve the monster problems that are among the hardest problems in Computer Science. This is not speculation, it is not merely "empirical", this is
provable.
Thus, when people start hand-waving that "just like AlphaGo beat a game that nobody thought AI could beat, so now AI will soon be able to solve mathematical problems that no one thought could be solved!", they are talking nonsense. There may be problems that are too difficult for humans to directly solve, which AI will help us solve. In fact, we've already done that with the four-color theorem, and other elaborate proofs since then. If you imagine the "mathematical frontier" of proved mathematical theorems as a circle, we can imagine a slightly larger circle that defines the "new mathematical frontier" that we will be able to prove with the aid of AI. But the point is that this is only an incremental improvement, it is absolutely not the kind of "singularity" that some of the most ill-informed AI-hype promoters out there keep suggesting. AIs might be able to write better proofs than any human could, and for problems that no human could discover the proof but, as already noted, this does not generalize to the unbounded case, and certainly will not result in some kind of "mathematical singularity" whereby all provable mathematical facts become a mere question of querying the omnipotent-AI.
To ensure that I am being completely clear on this point, consider the
unsolvability of Hilbert's 10th problem. Diophantine equations are just elementary number theory, that is, they exist on the integers and you do not need to invent fancier number systems, like real numbers, complex numbers or even rational numbers, to reason about them. The proof works by mapping a Turing machine (a computer) onto Diophantine equations, thus "running a computer on pure numbers". The standard result of Computer Science regarding the unsolvability of the halting problem is then reduced to the question of the solvability of a (very large) Diophantine equation. Thus, this equation is provably unsolvable. There is provably no algorithm, however clever, which can solve it. And this is a simple question in the purest and most elementary subject of mathematics, often called "the queen of mathematics": number theory. "AI could solve it!", the singularitarian blindly shouts, shaking her pom-poms. No, no it can't solve it, we can
prove that it can't be solved, not by AI, not by
any finite algorithm whatsoever, even if it could use all the energy in the Universe and utilize all the matter in the universe to compute at the Bekenstein bound...