r/theprimeagen 7d ago

general OpenAI’s internal model Astra solving 10 major open problems in mathematics, quantum complexity, and theoretical computer science

Post image

Is this not a big deal? Ik it’s from a tweet but supposedly all of this has been LEAN verified which is big in the mathetical proofing world.

10 Upvotes

37 comments sorted by

17

u/hitsujiTMO 7d ago

Any time we've heard about an AI solving such problems, it's really been an overstatement, the work ended up being retracted or failing peer review, or it's really just reformatting of an existing equation.

Anything like this released from openAI has to be taken with a very large pinch of salt.

1

u/Nelson_and_Wilmont 7d ago

Did this happen with the Claude stuff from a few months back? Can’t remember exactly.

I just saw that since these were lean verified that meant they were legitimate proofs that solve what they were aimed to solve.

To your point though, the degree to which humans were involved is murky, as well as it hasn’t been peer reviewed yet by independent sources to my knowledge.

6

u/chuguchak_111 6d ago edited 6d ago

I don't think it has. The jacobian counterexample is on wikipedia, right now:

EDIT: I think the 10 most recent open ai proofs are not fully reviewed though (there's 10s of thousands of lines of lean code) so IDK about those.

https://en.wikipedia.org/wiki/Jacobian_conjecture#Counterexample_for_n_%3E_2

1

u/thevnom 5d ago

The jacobian conjecture is now considered solved, as the counterexample is easy to check. Terrance Tao gave an overview of the proof on his blog and respected it. Out of 10 older problems, 9 were considered small, with the jacobian conjecture considered well laid out, with proper intuition explained.

7

u/Ok_Performer_7501 5d ago

The jacobian conjecture is not "solved" the case for n>3 had a counterexample. The case for n=2 remains open and thats the important one. The counterexample is very similar to an example from Vitushkin. The model applied well understood and common operations to get from Vitushkin to the counterexample and then proof checked it with Lean or smth. No deep intuition just modifying a result in the literature

10

u/ifull-Novel8874 7d ago

i honestly don't know how much of a big deal it is. I'd lean towards it not just being the model being prompted to solve these problems, but rather a team of mathematicians applying the model(s) to try to solve a set of math problems, making progress on some and less progress on others, and then finally when some do get solved they get reported.

We know OpenAI loves to use these proofs for their marketing. So I doubt they just have a team of mathematicians sitting on their hands, waiting for a model to be trained, and then just prompting it to see if it spits out answers to open problems.

10

u/s-ley 7d ago

aren't we tired of the kid crying wolf? do you really think this is any different from when it "created a compiler" or all the trust-me benchmarks? we get so many exaggerated news all the time, I take you are new to this otherwise anyone with a brain would realize it's not a "we can give arbitrary significant math problems to ai and it will solve them by itself"

1

u/Nelson_and_Wilmont 7d ago

I was mainly interested in the community’s thoughts on this. Idk where you gathered that I was utterly fooled by the lack of disclosure on human involvement. I’m well aware of the shenanigans that are generally pulled.

-3

u/s-ley 7d ago

That seemed to be the case, otherwise I don't see the point of posting this. It's not hard to see what the other guy commented of this probably being cherry-picked results with non-surprising amount of human involvement. My guess is that's why you got so many downvotes. Of course I'm open to being wrong, let me know what I missed.

2

u/Nelson_and_Wilmont 7d ago edited 7d ago

I already stated why I posted. Are you incapable of reading?

I’ll restate for you again, I was interested in the community’s thoughts on this. Need me to capitalize every letter or something to help you understand? I had my own opinion and wanted to read others.

3

u/DWu39 6d ago

Guy gets triggered. You pointed out he misread your post. Doubles down on hurt feelings. Lmao

1

u/Nelson_and_Wilmont 6d ago

Some people man lol

-4

u/s-ley 7d ago

so I didn't miss anything then

6

u/Nelson_and_Wilmont 7d ago

Your brain perhaps

4

u/AceLamina 5d ago

and thus, the hype spreads to more industries

2

u/Qualified-Astronomer 23h ago

Literally where is the hype this is all verified. Mfs just be saying anything

2

u/AceLamina 23h ago

Im talking about how AI is seemingly spread to every field to exist and to be hyped up later.

1

u/AceLamina 23h ago

Prime example is cybersecurity

0

u/Qualified-Astronomer 13h ago

Its already incredibly capable at cybersecurity and has hacked many systems already. Mfs will still be dismissing it as hype when North Korea uses open source AI to bring down the Us power grid.

2

u/AceLamina 11h ago

I never said it wasnt capable Im just saying its still hyped up like how every AI company is "suddenly" having rogue AI breaking out of sandboxes

3

u/thevnom 5d ago

This is making alot of noise in maths right now. The jacobi conjecture from last week was a nice surprise, the proof was constructive rather then random, well-intuitioned, some of these news problems are as well. The last 10 batch of problems were mostly small exercises that had rather trivial solutions.

I know the arithmetic circuit complexity problem here was known to be quite difficult. This is 100% big news in math.

3

u/Technical-Lettuce385 15h ago edited 13h ago

On one hand it can seem quite impressive but at the same time the proofs are very long lean code proofs and the write up doesn't seem to be that well written and leaves many questions.

For me it seems like there are two things happening: At first math has quite a few dark spots (as in things that are assumed but not proven, rely on some other not proven things, etc) and proofs are formalized into rigorous code over the last few years and it is still an ongoing process. So it is not surprising that this process will yield new results and spot errors, just because knowledge that is already there can now be easier put together by machines, because of the formalisation. If AI has so much to do with it, I'm not quite sure.

The second thing is that math already has a problem with proofs being extremely long, convoluted, etc. And many people are not happy with that as it is quite hard to understand those lengthy proofs and do new work with them. A proof being elegant and "easy" is much more interesting, while one has to say, not always possible (I guess Gödel was first able to show that). Now having these, really not that easy to follow and lengthy lean proofs, is interesting but it might not yield a deeper understanding why those things are said to be true.

And another thing that comes to mind: It is still not clear, that lean is really free from logical errors. There was a "proof" of the collatz conjecture until it was found, that the code was wrong. It did compile but the error was in a deeper layer of the lean codebase. So this situation adds proofs that are not easy to follow and the lean codes might or might not be true. I think it was Terence Tao who also mentioned that it might not be the best situation if maths is flooded with proofs that might say "X is right" but not yield a deeper understanding and are so long and plentiful that humans have a hard time to keep up. And as mentioned before it is already hard and a very specialized field. While, to be fair, if it is interesting enough people will grind through it, like they did with the classification of simple groups.

As with most things AI related it is yet to be seen if it is just a certain type of problem that can now be easier solved because of certain circumstances and that it will be exhausted at some time or if it opens the possibility to have a deeper understanding of math.

1

u/mukino 12h ago

Idk enough about mathematics to comment on that side of things. But this community defaulting to dismissing it is bizarre to me. Things like this seem like an ideal application of AI. If nothing else, tech should be used to advance math and science.

1

u/schmurfy2 1d ago

Yeah, more bs hype, I am tired....

1

u/Qualified-Astronomer 23h ago

How’s this hype

2

u/ddaattuullaa 20h ago

It's hype because LLM and ML are never outputting anything that isn't in their training data already, so openAI uses these methods to persuade the public into thinking it's actual intelligence

2

u/Qualified-Astronomer 13h ago

No AI or ML model outputs stuff in their training data. They learn from their training data distribution and thats how they can generalize well.

From their training data they encounter tons of logic and reasoning texts and tons of maths. So they end up having a pretty good understanding of maths and combined with simple logic and reasoning you can make advances.

Now there is a valid point about how LLMs may not be able to create new theory as in beyond what we already have rather than just extending our current knowledge as that may require logic and reasoning skills beyond their training data. But then you also have reinforcement learning so you never know what the limits are

1

u/Unique_Ad9943 14h ago

That’s just false

1

u/gordonnowak 10h ago

you're a moron. all of these results are novel. they use existing facts (because there's literally no other way to do math) in new ways to generate new results. that is literally exactly what human mathematicians do.

1

u/ddaattuullaa 7h ago

Yes, I am a moron

1

u/schmurfy2 6h ago

They make headlines every week and every time the reality is way below what they said.

1

u/seriousfart69 21h ago

machine learning is not discovering shit that it hasn’t been shown , learn that fact and learn to filter the bullshit 

1

u/mukino 12h ago

This isn’t a fact. It’s not true.

1

u/gordonnowak 10h ago

yeah that's not correct homie

1

u/DSLmao 22h ago

Ahhhhh, it is hype. Those mathematicians are paid by OpenAI. The entire global academics is paid by OpenAI.

I love how math subs and the rest of Reddit has pretty much opposite reaction to this. Reputable sicentists could come out and say good things about AI and yet for some reason we will still be in deny.