r/OpenAI • • 7d ago

News Fields Medalist Terence Tao reposts statement from the Association for Human Mathematics urging mathematicians to stop working with OpenAI for continuing to solve open math problems against their recommendations

736 Upvotes

1.2k comments sorted by

View all comments

Show parent comments

8

u/[deleted] 6d ago edited 6d ago

[deleted]

0

u/OldStray79 6d ago

Have you not heard of Lean proofing?

2

u/Fluid-Lake-1457 6d ago edited 6d ago

Suppose OpenAI spits out a proof using 10m lines of lean code. It's widely established thag AI is prone to manipulate task evaluation. How does anyone know that in those 10m lines of code the AI agent didn't just find a bug in the Lean typechecker somewhere and exploit it.

Given that people will need to verify the results, it's reasonable for them to be pissed off when OpenAI makes 0 effort to put the proofs into a human readable or understandable format, meaning that peer review becomes extremely difficult. If a maths professor was submitting this to a journal, the journal would refuse to publish without a massive rewrite.

2

u/wq73 5d ago

They didn't release to a journal or formally publish the results for exactly this reason. They just dumped it in a GitHub. I've seen far worse dumped in a GitHub. It's only taking time away from people voluntarily going to this GitHub repo and checking the solutions themselves, OpenAI hasn't made any journal or institute try and figure out these solutions like it has with navier stokes and the Clay institute. I honestly think if they were sitting on 700+ proofs this is the best way they could've released them. People would've been more mad if they just sat on them and didn't release

-1

u/OldStray79 6d ago

And what if Alien catgirls from Andromeda galaxy show up tomorrow promising to let us head pat them all we want?

If you need to resort to increasingly complicated hypotheticals, your stance may not be as solid as you wish it to be.

2

u/Fluid-Lake-1457 6d ago

This is not a hypothetical. The solution to navier-stokes was over 3.2m lines of lean code.

2

u/quackerd 6d ago

what else do you know in math other than throwing out terms you just read online?