Some people buy on "day 0", before it hits the stock exchange. This determines the price they pay on day 0. For example, if they buy 10% on day 0, they pay $130 billion.
The stock exchange is a "secondary market", which means you're buying stock from investors who own it, not from the company itself.
The discussion here is talking about helping individual research with proposals a human will read. That is different from spending 10s of millions to do a brute-force search of lots of different proofs which can be verified by LEAN automatically. There is no "automatic verification" of a system design proposal, and no way to figure out from 10s of millions of proposals which is best automatically, and also assuming people in this discussion don't have 10s of millions of dollars to throw at every design problem.
I guarantee that you could not find a proof using brute force, even with literally trillions of dollars of compute. You're betraying a lack of understanding of the complexities involved, unless you're using a definition of "brute force" which is essentially equivalent to "intelligent search."
Brute force is certainly the wrong way to put it, but that doesn't mean it's easy to distinguish superhuman effort from superhuman intelligence, or, in the words of Thomas Edison, perspiration from inspiration.
Especially as the pure gruntwork involved in acquiring the knowledge required to merely understand the details of the mathematics involved represent at least a significant fraction of a human lifetime.
And unless this human process of knowledge acquisition continues, eventually no one will be left to understand and attach any significance to the results machines produce.
> That is different from spending 10s of millions to do a brute-force search of lots of different proofs which can be verified by LEAN automatically
It’s kinda like the project where someone generated a lot of midi files for all possible pop riffs to copyright them. If you have a start and endpoint, rules for navigation, and unlimited computes, you can brute force anything. The nice stuff is when you made exploration efficient.
Other than for maybe Navier-Stokes, they just didn't brute force it in the way you guys are thinking. Most unsolved math problems are not susceptible to brute force, which is why the problems remained unsolved. AI is so quick it can of course try more ideas than a person, but each idea is executed at genius IQ level. Even if you knew the broad outlines of the proof of quasi-Riemann, there are probably only 20 people in the world who could have executed it.
This is trivially true for any theorem with a proof that can be automatically verified in finite time, but does not preclude the universe lacking a suitable combination of monkeys, typewriters, and time to do so.
>That is different from spending 10s of millions to do a brute-force search of lots of different proofs which can be verified by LEAN automatically.
That is not remotely how the vast majority of the proofs have worked. You don't know what you're talking about, but that seems par the course for these discussions.
I don't know how to communicate this, but what you are saying is almost entirely wrong.
People can follow what they did. The documents OpenAi produced in their big drop are hard to read because they are poorly written in weird ways, not because they are beyond human intelligence. They didn't brute force in the normal sense. AI doesn't get tired, so it can try 1000 promising ideas, but it's like 1000 Ph.D.-level mathematicians trying different ideas, not 1000 calculators trying all combinations.
The biggest results -- quasi-Riemann, no Siegel zeros, and Unique Games Conjecture -- have already been digested by experts. No Siegel zeros in particular already has like five different write-ups, and Tao has written a exposition on his blog.
So did we get any new mathematics out of this, or just solutions to problems without new techniques or insights? I haven’t been able to keep up with this or read the writeups you mention, genuinely wondering since this seems to be a central concern of the math community
It's only been a month and people aren't that fast, but I think yes. Analytic number theory and complexity theory were stuck on the lack of progress on certain questions, that is now unstuck.
After they announced the formalization of the classification of Finite Simple Groups, I immediately wondered "What would happen if you tried to formalize the Stacks Project?" Despite also being very long, it's the opposite of the CFSG: instead of a poorly organized set of results that contribute to proving one big theorem, it's instead a carefully-organized set of results that cover a broad area.
The Stacks Project was the model for how mathematics should be done (at least for the pre-LLM era). Algebraic geometry had lots of poorly organized foundational results that were not really created for themselves, but in order to solve problems in the field. One person, Aise Johan de Jong, set out to fix it by organizing a project to write out the proofs of all of the results in a carefully organized fashion. He's led the project since, though of course there are multiple contributors. The whole thing is thousands of pages.
I would be interested in hearing more about the gaps they uncovered in the existing results, and how they fixed them.
I actually believe that this isn't the way to go when proof is cheap. Due to the straitjackets of type theory sharing proofs across domains is painful for most human readers to consume. With AI it's much easier to specialize theories. It's just not worth the cognitive cost to build on top of broad and shallow theories. To have any hope in keeping up with AI we need to instead better appeal to the largest component of our brain - namely our visual cortex.
It would be great to prove that there is or isn't a non-galactic polynomial-time algorithm for NP-complete problems. But we can't even solve the easier problem of proving there is or isn't a galactic polynomial-time algorithm, so what hope is there for the harder problem?
If you could prove that any polynomial-time algorithm for NP problems had to be galactic, you would be the most celebrated computer scientist since Turing. It's just no one has any idea how to do that.
Yep, ranting against galactic polynomial algorithms reminds me of the people who oppose the use of infinity. Like, yes, it's not physically realistic construction, but it makes things simple enough that we can do analytic solutions to problems and simplify terribly complicated things.
Polynomials are closed under multiplication, so you can do a poly algorithms poly number of times and still have a poly algorithm. That's very convenient.
The article makes the point that not all polynomial algorithms are created equal. If you combine ten O(n^2) algorithms, you can end up with an O(n^1024) algorithm, which isn’t practical anymore, despite being polynomial. That’s inconvenient.
A general affine coordinate change in 3d is Ax + b, where A is a 3-by-3 matrix and b is a 3d vector. If you add a fourth coordinate that you set to 1, you can write it as a 4-by-4 matrix. That's homogeneous coordinates.
And what this means geometrically is that the translation becomes a shear in the 4d space, which is a linear transform. It’s easier to visualize if you think in 2D; the matrix
(1 b)
(0 1)
maps a point (x, 1) to (x+b, 1) which is exactly what we want, while vectors (which we model as points (x, 0)) remain at (x, 0) as they should - translation shouldn’t act on vectors!
The problem with math is that there's more you need to know than there's class time to teach it to. Projective space is a good example. It comes up in several different ways, but you're probably not going to see them all.
Given the capabilities of OpenAI's unreleased model, I think the model helps mathematicians more than it hurts them. Some of the open problems that were solved were "It would be nice to know that", but many of the others represented ways in which we had been stuck for many years. There had been very little progress on analytic number theory, particularly the Riemann hypothesis or its variants. (One result, "no Landau-Siegal zeroes", even had a 10-page elementary proof that everyone missed for a century.) Complexity theory had seemingly more open questions than results. Progress could meaningfully accelerate now that we have a quick test of which of our ideas are good, and which are bad.
The wildcard is that we have no idea what the model after that will be capable of, or the model after that.
> I think the model helps mathematicians more than it hurts them
I would agree with you if these models were available to mathematicians, and OpenAI wasn't effectively competing with them by spending millions of dollars in compute to rush out solutions.
$/token/intelligence is dropping exponentially. Soon, they will have access.
Why do I get this feeling that people who complain about these models not being accessible are the same ones who are anti-data center build out, thinks AI is in a bubble, and thinks AI labs are evil.
In other words, they want cheap, available access to highly intelligent models, but they believe everything about AI industry is wrong.
The stock exchange is a "secondary market", which means you're buying stock from investors who own it, not from the company itself.
reply