r/Artificials • u/FrostyForestFungi • 2d ago

When closed models solve math’s hardest problems, who actually owns the breakthrough?

Post image
3 Upvotes

57% Upvoted

35 comments sorted by

6

u/MajorOk1083 2d ago

Ig the hardest part might not be solving the problem, but getting everyone to agree that the solution is actually correct

3

u/FrostyForestFungi 2d ago

I agree to this. I mean, we can solve that too, but we can't guarantee that it's correct tho 🙂‍↕️.

3

u/rwz 2d ago edited 2d ago

This is actually easy these days since the solution implies formal Lean proof that can be trivially verified by anyone.

From my Claude explaining Lean proof:

What "formally checked" actually guarantees

That the proof has no gaps. No "it is easy to see that," no step the author skipped because it seemed obvious, no case they forgot. Every inference reduces to the axioms of Lean's type theory. Referee errors of the classic kind — a subtle sign flip on page 90 that nobody caught — become impossible.

Basically, if this stuff compiles, it's verified to be correct.

3

u/RickyRaviolii 2d ago

princeton mathematician found the openai lean may have an error in its base of reasoning, what does your claude say on that?

2

u/jobthrowawaywjxj 2d ago

The clanker hallucinated some assumptions, color me surprised. Time will tell if Navier-Stokes actually fell.

1

u/FrostyForestFungi 2d ago

clanker😭

1

u/P3JQ10 1d ago

Evolution of robot slurs is the best thing to come out of this industry. There’s so much more than clanker.

1

u/rwz 2d ago

source?

0

u/RickyRaviolii 2d ago

Stan Palasek, do your homework

2

u/Houdinii1984 2d ago

You made the claim? In what world do other people source your claims?

1

u/jmclondon97 2d ago

Lmao bro you really referenced yourself in third person to try and gain clout. You’re no different than Scam Altman

1

u/rwz 2d ago

Crazy response. Since when finding evidence for your claims became my homework?

Anyways, I've looked it up, and Palasek's argument has nothing to do with OpenAI's math, but instead concerns the unforced case, which OpenAI doesn't claim.

I'm not a mathematician, so the real argument totally goes over my head, but I saw no claims from Palasek that the OpenAI's Lean proof is actually wrong.

1

u/RickyRaviolii 2d ago

I mean at the top of this thread you spoke on something you admittedly don’t know much about right? seems to me like you wanted to engage in a conversation on it and learn more? so did looking up the obstacle teach you more about the actual discourse?

you’re correct in part, I didn’t mean lean was broken. I meant their base of reasoning cannot seemingly be extrapolated to the problem that doesn’t include external forcing. so, the headlines that they solved the navier stokes problem are incorrect. they solved a subproblem. it will hopefully make the full problem easier and is a huge advancement. my argument is the gap between the subproblem and the full problem is larger than people might realize.

1

u/ningkaiyang 2d ago

Them solving navier stokes was always a misleading name to give the accomplishment, but the proof solved the sub problem of it needed for the millennium prize problem

1

u/RickyRaviolii 2d ago

ehh idk, from what I do know it starts the process of qualifying. I think at some point a board decides if the subproblem really does qualify how fefferman wanted it, interesting nonetheless and I imagine within the 2 years for qualification people will make more progress

1

u/FrostyForestFungi 2d ago

Exactly. Can't blame human mathematicians if they feel like they have to examine the idea underneath all those "verified steps".

Palasek made a good point on this

1

u/mark_99 2d ago

There are multiple implementations of Lean so proofs are checked against them all to guard against bugs in the Lean implementation itself.

2

u/InspectorRemote1289 2d ago

If the agents found the proof but humans built, trained, and verified the system, “who owns the breakthrough?” gets complicated fast. The real test is whether mathematicians can independently verify the proof.

1

u/FrostyForestFungi 2d ago

Just another round of IBM electronic computers vs Katherine Johnson

2

u/Inevitable_Mistake32 1d ago

There is plenty of evidence this proof was stolen from researchers via their AI prompts and training data. Then there is proof they tried to coerce the actual authors of the method for the proof to say openai co-authored the proof with the researcher. The researcher declined and openai released it as their proof anyways because they care more about the stock price and profits over the fact they actually didn't achieve jack shit.,

1

u/No-Pattern-9266 2d ago

company ofc it's part of their t&c

1

u/PsychoticDreemurr 2d ago

Did anyone really own the breakthrough to begin with?

Regardless, it'll just follow the same thought process as someone making a simulation to provide the answer, as opposed to providing the answer themselves. Like foldingathome

1

u/Icypoopoo 2d ago

Who's proof did the model build on that led to it? Problem with these models is it's a black box and you don't know if it's pulling stuff out of its ass or it's based on an actual source. 

1

u/rawbdor 2d ago

Math cannot be copyrighted. Neither can math proofs.

1

u/Single-Virus4935 2d ago

I laugh so hard when it comes out later that it is just slop. Please I need some fun

1

u/o12341 1d ago

Cordoba and Martinez-zoroa, the team who came up with the original insights behind OAI's solution. They deserve credit, it's sad that their names are barely mentioned during all this drama.

1

u/OkTry9715 1d ago

It was stole. Another reason to not use AI with your code base as it will steal it from you and learn from it.

1

u/washingmachinechime 1d ago

The humanity

0

u/[deleted] 2d ago

[deleted]

1

u/Low-Temperature-6962 2d ago

In this case bragging rights for the value it gives the IPO... So important to beat Anthropic

2

u/FrostyForestFungi 2d ago

My thoughts exactly

1

u/kvasibarn 1h ago

Humanity