This is a problem where experts have no clear idea whether it holds or not (and different mathematicians have strong opinions here). For a civilized discussion on whether the Smooth Poincaré Conjecture holds, see for example https://mathoverflow.net/questions/97464/how-to-tackle-the-s...
Additionally, "by mere coincidence" :-) (which makes this problem very fitting for the drama around the recent AI proof drops), the Smooth Poincaré conjecture is a problem where Selman Akbulut, who made a lot of progress on it, posted strongly worded claims of how his results were "stolen" by other famous mathematicians in the past:
"Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding."
"Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding."
> If the blog had pseudo-code instead of 18th century scribbles
E for expectation, blackboard bold, double-bar norms and indexed max/min are all early to mid 20th century notation, making them thoroughly modern. Only summation notation dates since the eighteenth century, and its relative stability over that period is in fact rather a strength and not a weakness. Summation notation is also nearly universal in any quantitative field, and far, far more concise than the equivalent looping C-style pseudocode or functional-style pseudocode.
> You're also connecting the syntax to understanding of the concepts which is the cherry on top of the math snobbery in this thread
Because that is in fact a big part of how it works. Good notation takes a lot of time and thought to develop, and the notation used in the post is far, far more concise and packs far more information into a tiny amount of space than pseudocode or other programming conventions. Much of math is abstraction (compacting complex ideas into specific symbols or concepts, and then coming up with simple rules to allow their manipulation), and is possible in large part only because of good notation like this. See some of Terry Tao's thoughts on the subject below.
The notation here is really also all first-year introductory notation, and incredibly simple. Most CS or computer engineering students should have seen it, and anyone that thinks they can learn anything non-trivial at all about neural networks by avoiding such basic notation is simply not a serious person at all.
EDIT: And it is a mistake to imply pseudocode is generally superior or easier to understand, because pseudocode is often too precise, and implies more structure and relations and implementation details than are actually needed or important. Meaning it actually often communicates the wrong thing compared to good notation.
"How and whether specific mathematics might lead to improving the world (whatever that means) is usually impossible to tease out, but mathematics collectively is extremely important."
There are good reasons not to delay publishing at all:
> They should release all their results immediately. (Imagine working on one of the problems they already solved.)
This is the most popular answer to a question regarding AI advisory group and immediate access on a popular website for professional mathematicians: https://mathoverflow.net/a/515442/473286
The whole debate regarding the behaviour of OpenAI is a red herring. Mathematics need to redefine their profession and how they work (like us software developers too). There are very good reasons to believe mathematics has an important role to play. If they could just stop talking about OpenAI and get back to work - they are very much needed, in particular now!
That's what math has always been about, even if not everyone is necessarily as talented a communicator as someone like Thurston -- who was himself an exponent of computational tools in math research:
>I think of mathematics as having a large component of psychology, because of its strong dependence on human minds. Dehumanized mathematics would be more like computer code, which is very different. Mathematical ideas, even simple ideas, are often hard to transplant from mind to mind....Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding....
Your monopoly theory lacks a credible motive and also ignores the fact that your quote specifically targets the frontier labs, not LLMs or computational tools in general. The group (https://agmai.org/) comprises of world-renowned mathematicians, including several Fields medalists, who have nothing left to prove. If they felt like it they could quit mathematics today and take private sector jobs paying far more than their professor salaries.
The basic purpose of mathematics has always been human understanding (see for example
https://mathoverflow.net/a/44213), and the working group's various recommendations simply aim to ensure that computer-generated mathematical activity aligns with that purpose.
https://mathoverflow.net/q/511601 is a fun little math problem that came up in one of my projects, I didn't have any reason to expect it to be particularly tough, but none of the models I've thrown at it have been able to solve it past a few minor reductions and special cases.
I expect that there is some relatively easy-to-state solution to this problem, but that it's different in form from what most existing proofs and tools yield. Perhaps if I dumped millions of dollars into it an agent might chance on the solution. Or perhaps my luck is such that my fun little problem is truly intractable...
> The product of mathematics is clarity and understanding. Not theorems, by themselves. Is there, for example any real reason that even such famous results as Fermat's Last Theorem, or the Poincaré conjecture, really matter? Their real importance is not in their specific statements, but their role in challenging our understanding, presenting challenges that led to mathematical developments that increased our understanding.
Yeah, that mirrors what I've seen throwing some of the leading models at a set-theory problem that's stumped me (https://mathoverflow.net/q/511601): in this case, the problem does not easily yield to the standard tools, but the LLMs do not recognize it as a major open problem they should give up on. So they seriously try it, but typically end up in a loop of inventing certain classes of simple solution or counterexample attempts, defeating them, and trumpeting each one as a major result, each time inventing some new terminology.
It's definitely quite curious that the AI labs are able to push these results through seemingly with pure brute force. Perhaps it's largely a function of how many monkeys you have attempting various constructions on top of the known results and strategies the models have memorized.
When Thom, the mathematician who now alleges plagiarism, posted his digestion [1] of OpenAI's construction of a non-sofic group, he does not mention the proof being familiar. He even calls the crucial argument clever, without noting he thought of it first.
[1]https://mathoverflow.net/a/513885
There are a couple of proof languages that are designed for formalized mathematics (rather than formal verification of software) and to be readable by mathematicians. For example, look at the proof that square root of 2 is not rational written in Naproche (retyped from [1], typos are mine):
Theorem. $\sqrt{2}$ is irrational.
Proof.
Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.
Qed.
Or, say Isar in Isabelle/ZF [2].
There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.
Anyone interested in the subject area has noticed the recent surge of AI-assisted or generated mathematics. From the outside, it is very hard to see, if AI indeed already speeds up progress in mathematics in general - apart from a number of spectacular results, (https://mathoverflow.net/questions/502120/examples-for-the-u...) - or if the quality of the large majority of these "proofs" is so poor that reviewing them is a waste of time.
I would be grateful, if someone familiar with the situation could say a word about this.
As for the proof in question - I'm not sure the author himself can firmly state he understands every detail of what he presented. In a way it's amusing that people who already enjoy a certain level of recognition outside the field are now using it to find (via shiny websites) reviewers for proofs they have worked out as a hobby using Chat GPT and the like.
What we definitely need is more recognition for those who possess the competence and energy to assess the correctness and relevance of such "results".
> > Proofs which fewer and fewer people are able to understand
This is the trend for proofs of famous old theorems in general, even pre-AI. Some particularly extreme examples are the proofs of Fermat's Last Theorem [0], the abc conjecture [1], the classification of finite simple groups [2], and the four colour theorem [3].
I’m pretty sure no one (except perhaps Anthropic insiders who had prior access, and probably not even them) has properly digested this paper yet, and some caution is warranted given the notoriety of this problem and the history of claimed solutions that did not stand up to scrutiny. But if it stands up, it’s a really big deal.
For a list of AI accomplishments in mathematics see https://mathoverflow.net/questions/502120/examples-for-the-u... - or a candidate list here: https://aimath.robertj1.com/ . Many have observed an affinity of AI to the search for counterexamples - or examples. Looking at afore lists, something much more sociological crosses my mind: There is a hunt for answering prominent, clearly stated problems. I'm not a mathematician, but is this mostly what progress in mathematics is about? How about stating worthwhile problems in the first place? What about theory building? Am I right saying this is equally important, but none of those utilizing AI for mathematics seem to be interested in such?
One curiosity that in the case of infinite graphs, "no odd cycles" doesn't imply "2-colorable" without the axiom of choice for families of 2-element sets [0]. It's somewhat similar to how in the definition of a well-founded relation, "no infinite descending chains" doesn't imply "every nonempty subset has a minimal element" without dependent choice.
(One of my recent projects has been trying to prove the existence of a 2-colorable subgraph for a certain class of infinite graphs in ZF, which has led me surprisingly deep into choice principles and models refuting them.)
Math is very hit-or-miss; the complexity of a question does not give much of an indication about how complex the answer will be. Look up the formula for solving a degree-4 polynomial equation to get a purely visual idea how this can look (and then degree-5 suddenly forces you to use complicated new functions). And there are problems (like the Collatz conjecture or P vs. NP) that there doesn't seem to be any promising angle of attack for over at least decades.
I would wager that this is a fundamental part of the structure of math that has been a constant from ancient Greece till LLMs. There are even some formal results, similar to Gödel's theorems, that say that the maximum necessary length of a proof grows arbitrarily fast (e.g. more than exponentially, double-exponentially, or any function with a formula) with the length of the statement being proven.
Point is, math will most likely never suffer from this particular problem.
Your reply isn't a response to the comment, but rather a general expression of antipathy towards mathematicians, who are apparently fatcats who have fancy lifestyles.
I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system like Metamath?
One problem where that mathematicians would love to see resolved is the Smooth Poincaré Conjecture (in dimension 4): https://en.wikipedia.org/wiki/Generalized_Poincar%C3%A9_conj...
This is a problem where experts have no clear idea whether it holds or not (and different mathematicians have strong opinions here). For a civilized discussion on whether the Smooth Poincaré Conjecture holds, see for example https://mathoverflow.net/questions/97464/how-to-tackle-the-s...
Additionally, "by mere coincidence" :-) (which makes this problem very fitting for the drama around the recent AI proof drops), the Smooth Poincaré conjecture is a problem where Selman Akbulut, who made a lot of progress on it, posted strongly worded claims of how his results were "stolen" by other famous mathematicians in the past:
* https://selmanakbulut.com/plagiarism.pdf
* https://selmanakbulut.com/story.pdf
* https://selmanakbulut.com/story2.pdf
--
Addendum: Also clearing up the situation of the Generalized Poincaré Conjecture for Diff manifolds would be very interesting:
https://en.wikipedia.org/wiki/Generalized_Poincar%C3%A9_conj...