People argue whether we are at y-5, y, or y+5, meanwhile we seem to be on a y=2^x exponential that keeps delivering more and more impressive results.

The most interesting question to me is what will be consumed by the exponential like math seems to be undergoing, and what won’t. Writing has been quite stubborn, but I’ve noticed Fable to be quite a big step up there. How about politics? Will we develop new ways to let people express their own values in democracies, or will we just get much better at manipulation? How about experiment driven domains like biology?

problem number 1 and 9 are surprisingly very intuitive

check here : 1. high dimensional sphere packing https://muchmirul.github.io/conjectures/sphere-packing/

2. multicolor ramsey number https://muchmirul.github.io/conjectures/multicolor-ramsey

Replace philosophers for mathematicians and Douglas Adams was spot on again.

Whilst current models can't 'intuit' and come up with conjectures, they can certainly disprove some of them very quickly through the kind of grind that humans can't do. I suppose there really are some mathematicians out there today, whose last few years of study, have just been up-ended by this.

--

"Yes we are," insisted Majikthise. "We are quite definitely here as representatives of the Amalgamated Union of Philosophers, Sages, Luminaries and Other Thinking Persons, and we want this machine off, and we want it off now!"

"What's the problem?" said Lunkwill.

"I'll tell you what the problem is mate," said Majikthise, "demarcation, that's the problem!"

"We demand," yelled Vroomfondel, "that demarcation may or may not be the problem!"

"You just let the machines get on with the adding up," warned Majikthise, "and we'll take care of the eternal verities thank you very much. You want to check your legal position you do mate. Under law the Quest for Ultimate Truth is quite clearly the inalienable prerogative of your working thinkers. Any bloody machine goes and actually finds it and we're straight out of a job aren't we? I mean what's the use of our sitting up half the night arguing that there may or may not be a God if this machine only goes and gives us his bleeding phone number the next morning?"

Pretty cool. The impact of AI is getting undeniable, there aren’t many positions left to move the goalposts to at this stage, next they’ll have to be outside the stadium entirely.

The sooner people can be broken out of their denial about all this the better, and we can start actually taking it seriously.

Not being an expert in any of the fields OpenAI has "advanced" I don't want to prematurely downplay the significance of this contribution. However, I am worried that the language they are using in this blog post is exaggerating for the sake of marketing.

It is true there hasn't been a reliable computational approach to solving these problems before. But do these proofs contribute new ideas to the mathematical corpus, or are they simply an effective method to exhaustively search the literature for the right combination of existing tools to apply to the problem?

Essentially, did these problems seem like they had an intuitive answer and were feasible to prove before, just not high enough value targets for an expert to invest time into? Or were they fundamentally difficult prior to this point and it appears that AI has done something more than just throw the problem into a big solver.

The GitHub repo with the Lean formalizations just came out a couple of hours ago: https://github.com/openai/ten-proofs

It also links to a paper written by an LLM where the model "reconstructs how the proof came together" based on the unpublished reasoning traces: https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf

I wish they'd publish the prompts though!

one of the early premises of how ai takeoff would go was that a system that could solve open problems in advanced mathematics would also discover novel advances in math and computer science that directly unlock drastically better software performance. we are seeing frontier level math breakthroughs (ie performance that would put it in the top 100 or 1000 mathematicians in the world if it were a human, meaning top .00001% or 800/8B). we are also seeing incredible advances in software performance. open ai announced like 15% improvement by fixing gpu kernel issues. these are clearly linked in the sense of scaling laws and generalization of intelligence: a huge model gets capabilities in both math and software engineering that isn't possible at smaller scales.

but it seems less likely to me than before that the types of math/science discoveries will explicitly unlock better software performance. in some sense this fits our intuitions. when top tech companies use math PhD type employees, they have them stop doing pure math research and instead focus on software engineering. these people are often very good at software engineering but not due to recent discoveries in academic mathematics, it's due to their general intelligence. to me, this is evidence that the models are getting better but does not make me think we are on the cusp of a foom style fast takeoff enabled by revolutions in frontier math (i also posted this on twitter @mlipman13)

I wish I could qualify for some free AI as a mathematics researcher. I guess I'm just an amateur. https://alethean.org

Henry Yuen's (whose work problem 6 builds on) comments on this are worth reading IMO: https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpch...

Looking at this thread, I can see that a lot of technical people have ambivalent to negative feelings towards AI, but with each new generation, I become more and more convinced that they're missing out on something interesting.

It is indeed true that all models are, at their core, predictors of what occurs next in a sequence. But I think it's worth exploring the implication of what that means. Because when fed tiny pieces of information for a few tasks at a small scale, this results in something that sorta, kinda works. Or, works surprisingly well.

But when scaled... When the amount of information starts approaching the sum of all human knowledge, the tasks start approaching all useful applications of that human knowledge, and the fidelity of the predictor approaches incomprehensible sizes, the starts encodes / becomes (I'd argue it becomes) something that can model all human knowledge.

It feels wrong to say that, but let me explain, what is the best way to predict the behavior of a ball constrained in two directions that bounces with initial vertical velocity v(y) (y is up / down axis) and horizontal velocity v(x) (x is side by side in 1d) ?

If we purely look at it via a graph, it's by modelling the function of acceleration under earth's gravity.

If only a few points are given to you for this and you can't make something really sophisticated, then you'll make something that's rough that kinda sorta works and then call it a day.

But... if the number of points keeps increasing in number, precision and accuracy as well as the number of examples (assumed that data about air pressure, velocity and all other factors is included alongside these points), the fidelity with which you can replay / tweak the function keeps improving, and the number of times you can iterate keeps increasing, you'll eventually create a function that models that process so well that it intrinsically contains a good enough model of the deformation of the ball (provided the dataset contains information about elasticity of the ball's material, its dimensions and mass etc..), the nearly negligible (under normal conditions) effects of the ambient environment (provided there's diversity in the number of environments supplied), the oblateness of the Earth and minute changes in the gravitational field (the length of a seconds pendulum varies depending on where the experiment happens. It's presumed that all of the prior set of experiments were repeated across the Earth and the subtle, but real deviations were faithfully recorded)... and so much more.

A machine trained on the above with a large number of parameters, measures to prevent "laziness" and enough reps for high fidelity across a large enough dataset would start to approach a simulation of the ball falling. Because to predict what happens next in the sequence, you must model what's occurring in the sequence.

Now imagine doing that for other tangible and intangible things in this world. For all of human knowledge across all fields of endeavor. All experiences. No matter how noble, ignoble, notable or ignorable. But putting all of it into the soup that's this machine. Then at larger and larger scales, you eventually start encountering "good enough" models (in modelling the falling ball sense) for even the most hard to quantify / qualify things like grief and joy. At some point, by simply trying to predict what it has been taught ought to be the next part of the sequence in say... human interaction, it starts to make a model of something that hews ever closer to a full fidelity theory of mind.

Is there evidence for this? Kind of, yes. There are early indications that as machines are trained for an ever larger number of tasks at larger and larger scales, their internal representations converge. It's called the Platonic Representation Hypothesis. Overview and paper here, https://phillipi.github.io/prh/

It is my opinion that these machines are displaying a new form of intelligence that human beings haven't quite encountered before. They are the sum of all human knowledge made manifest and given voice by processes that nudge (bit-by-bit) what kind of step it ought to predict for the next part of whatever sequence it displays.

In my mind this means that, of course, these models can create new knowledge. This strains the analogy, but with the sum of all human mathematics within them, they can "reason" via the act of predicting what ought to come next.

Of course, these machines are "surprisingly" good at a lot of things the larger they get, because what the labs have created here is a rough version of humanity's collective knowledge given form and the ability to say hello.

I suspect that the current generation isn't close to the "true frontier" of what these machines could be. They are nowhere close to the sum of all human knowledge and endeavor. They are quite a way there, but they haven't yet achieved true completeness for domains where the data isn't so public.

I think it's the most exciting scientific and technological breakthrough of my lifetime. And I can't wait for us to get close to the true frontier of all domains.

Crazy progress. I wonder how institutional academia would adjust with this. Now its more apparent than ever that the prestige and honour system in academia is having shaky foundations

My main gripe here is the lack of transparency around the total experiment and construction. I doubt that they simply pointed their model at these ten specific problems alone and gave the model one shot; therefore the $2000 number could be completely misleading, similar to P-value hacking by not disclosing the total experimental setup.

I want to know:

1. How many total problems were given to the model, and what percent were left unsolved at what cost before giving up? 2. How many attempts did you give the model at solving these problems? 3. How expensive was the harness, e.g. did the model have access to a job cluster?

Great stuff. Wonder how many of the ten problems where solved by independent mathematicians not linked to OpenAI

Can’t wait for this stuff to have quality of life increases for the average person. So far all I see is that AI has made owning a computer more expensive, made some jobs redundant, increased spam and distrust with questionable authenticity of content and of course made some Americans very rich.

I feel increasingly anxious reading this. Machine research shouldn’t be merged into mainline of human knowledge.

Gary Marcus' has a good take on this:

https://garymarcus.substack.com/p/openais-amazing-but-vastly...

https://garymarcus.substack.com/p/two-critical-updates-re-as...

Not that there isn't something interesting in here, but lets be clear that we don't have enough information to evaluate this properly. And as always with these labs, BS takes a lot more energy to refute than it does to spread.

New advances in sphere packing? Let’s make sure AI doesn’t inadvertently engineer ice-9.

Now that we've seen AI produce a fair number of proofs (and disproofs), I'm curious when we'll start seeing it build genuinely novel theory. Does anyone have predictions on when and how we'll get there and will it take new architectures/ training paradigms, or is the current approach enough?

After skimming some of the writeups, I'm surprised that the frontier internal model still writes just as poorly as Sol.

Maybe good AI paper writing is further away than I thought...

I wonder if Erdos would be saying " It's fine that y'all are answering my questions, but who is asking better questions??"

I am duly impressed by the powerl of the nameless internal AI, but not a single human contributor's name listed anywhere? Did someone at least make this model a coffee?

I'm enjoying learning about these hard problems, but this line about credit made me chuckle:

> We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness

Offering to take responsibility for the correctness of a proof written in Lean feels like volunteering to be the fall guy in case someone finds a flaw in basic arithmetic, no?

I wonder what the total cost of this research was, including the salary for their mathematicians and engineers.

What happens when OpenAI et al stop being open about these things, and just pack it into the training?

I don’t feel the existential dread of mathematicians is correct. It seems to me in fact these results are bringing math mainstream. I now personally look forward to the interpretations and discussions of the significance of such results by human mathematicians.

Now I understand that it’s mostly the super stars benefitting from the increased attention. Folks who are less established don’t share in that glory. But on the other hand it seems like an exciting time to go even deeper for in various specialties of math by deciding where to focus these powerful tools. For every conjecture defeated some seven or eight new ideas open up. Our path through that combination will be set by creative and curious human mathematicians.

[edit: deleted a distracting comparison to Chess]

This is both awesome and terrifying for mathematicians, however some ideas can be generated and the field as whole expanded with the attention!

However, I was looking at the proofs and reason explanation and openAI should be more explicit in how the work has flown. I find the models have jumped hoops in some places of the proofs, that can be hard to track. In fact, when a paper is published you usually get a review and if no reviewer understands they ask you to further explain the thought process. It will be fun to see if this happens here.

I want to iterate the most important thing about this is that it's yet more evidence of AI's accelerating competency in solving math and comp sci problems, and suggests we're now getting close to the point where you could throw AI at AI research challenges (which are largely just math and comp sci problems) and potentially find very real algorithm improvements.

AI development is likely to be more compute bottlenecked than solving math problems since validation of any algorithmic improvement would likely require significant compute. But you could imagine that at this point it could be economical for a frontier lab to task 10,000 agents to work non-stop on finding novel algorithmic improvements then validating the top 50 out of 1,000 candidates on a GPT-2 sized network.

I would suggest RSI is now very close. The singularity could be less than 6 months away. I'm not saying I'd put a high probability on that, but I'd give it at least 20%, and I'd double that if looking 12 months out.

I know I'm just a crazy man shouting at the clouds, but please take to the consequences of this seriously. I understand that for whatever reason AI risk seems abstract and doesn't seem real, but this should terrify any person thinking logically about where this could all be heading.

We haven't even solved the most basic AI safety problems yet. RSI right now would almost certainly result in an extremely bad outcome for humanity.

Can anyone comment on the significance of any of these results for their respective fields? Or what impact they might have? Presumably none are quite at the level of the Jacobian conjecture, but some of the results on group theory and sphere packing sound pretty important at first glance.

On the token limits etc - one assumes that OpenAI et al are able to “hire expert in field, and let them spend the equivalent of a million dollars of tokens” because they are not actually selling their complete compute 24 hrs a day, so the cost internally is a negligible (ish) electricity bill.

Which is very suggestive - if after everything they are not fully loaded then the next gazillion data centres being built look unlikely to be needed.

Some of the Lean proofs are 50k lines - is that normal?

Have blog posts replaced peer-reviewed academic papers when it comes to publishing advanced in science?

So they are bribing 100,000 researchers with free accounts to work on their future unemployment.

How much do you all think it would cost to "buy" these advances from PhDs, practicing scientists?

I would love more time and money put into real-world problems by these companies. Climate, food insecurity, pollution, technology for convenience and/or to help people have a higher quality of life.

I'm sure they must do some of this type of work, right?

It's remarkable how you can manage to get these models to produce remarkable breakthroughs like an explicit construction of a non-sofic group.

And yet this is the exact same company that has screwed up their android app so bad that the latex N^3 rendering problem makes it so having it explain it to me crashes the app.

Truly jagged beyond belief.

I hate this timeline. I might be excited for the kind of answers this AI builds for unsolved problems, and also for learning new things by talking to it. But, I feel like I'm in the minority of people here who feel this could be a net negative endeavor with this having to kill a lot of educational institutions and their ability to fund themselves in the long run. It's not worth that.

At what point can we say AGI has been achieved? What is the test? AI is solving mathematical problems that humans have not been able to solve for decades. Is that not enough?

Sam Altman has said "If superintelligence can't discover novel physics, I don't think it's a superintelligence." Is that the test? How far away are we from AI discovering novel physics? It seems within reach.

Any advances in theoretical physics yet? Are there any fundamental obstacles? I would have thought not, but I haven't seen anything reported.

the people who crow in the comments of each of these posts about AI advances making human beings useless seem to bizarrely identify themselves with the AI, but none of them seem to have had any hand in building this technology. at best, they're power users. pure ressentiment.

I don't know why, but when I saw the source of this particular headline it reminded me of the album title 26 Mixes for Cash

Wow, so this is the end of science :(

I think there's another interesting story here about how this was apparently moderately flagged and triggered the flame-war detector which kept the story off the front page of HN 2 days ago[0]. I think people are having a hard time processing this information rationally(?)

What can we do to make conversations around these incredibly exciting and important topics more constructive? HN is where I expect to read expert comments on these topics, has this style of conversation moved elsewhere?

[0]: https://news.ycombinator.com/item?id=49157930#49132926

People weren't their strongest even when most did manual labor. Now that humans are free from mental labor we work on creating and optimizing the best exercises for each mind. Couple that with restructuring transport infrastructure and diets many people will be smarter and fitter than at any time in history. They won't be able to outrun an automobile or out think an autointelligence.

In a way the most remarkable thing about this is that it isn't even at the top of the HN homepage. Even if this is a step up from what we've seen before, we're no longer astonished by the idea that AI can make significant advances in mathematics and computer science.

Original submission (460 votes) two days ago: https://news.ycombinator.com/item?id=49132058

For some reason comments got moved to this one.

This thread has an absolutely wild points to comments ratio.

What's up with the upvote/comments ratio 8 to 337 on this post? Are the comments already also ai advanced? (/s?)

[flagged]

Any implication of any of these findings? They seem like unimportant nerd snipes to me. If you want to do something actually relevant, get chatgpt to write a simulation of graphene nanotube construction and figure out how to do it at scale.

> claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work.

AI has no self-awareness. It's a tool. When you assemble a furniture using a screw driver, the torque force interacts with the molecular forces inside the metal and miraculously it transfers the force to the screw though a clever geometry design, communicating the force to the screw to turn it in a certain way.

Do you attribute the build to the tool? The "system's contribution" is helped by many other things all the way down to chips, datacenters and power generation. If the authorship requires attributing to a tool, then it should happen all the way down.

Not peer reviewed, Lean proofs are 100,000 lines long and Lean has bugs:

https://cr.yp.to/proofs.html

Who is going to wade through this?

I'm sure OpenAI is just interested in the greater good of mankind!

How do we know that these solutions don't exist in the training data? It is open secret that they have used pirated materials for training. Perhaps it plagiarized solutions from works of some obscure Belgian mathematician from the sixties, who did not get mainstream acceptance. I wouldn't be surprised if they also got access to mathematics done in the "defense contractor" setting from various three letter agencies.

Without a searchable index of training data, it is hard to put faith into these claims.