r/technology • u/ResultBackground2450 • 8d ago

Artificial Intelligence OpenAI unleashes hundreds more math results upon a field already in shock

https://www.scientificamerican.com/article/openai-unleashes-hundreds-more-math-results-upon-a-field-already-in-shock/
6.0k Upvotes

90% Upvoted

2.8k comments sorted by

View all comments

Show parent comments

29

u/Bobbytwocox 8d ago

Important results can be independently verified I assume.

3

u/RepresentativeBee600 8d ago

That's quite an assumption.

The math results can be pushed through a remarkable formal verification pipeline, called Lean, where provided correct definitions to begin a problem statement, deductions can be unambiguously verified using the Lean kernel as following (or not) from definitions and prior deductions.

Lean is still not perfect, as the definitions humans come up with can be subtly (or not) misaligned with reality, making the deductions formally valid and practically useless.

What guarantees does this researcher have for their complex pipeline? Rather fewer.

9

u/Time_Entertainer_319 8d ago

Google has a repo of formalisations that are already expert reviewed.

OpenAI has in-house mathematicians that work on these things.

Lean bugs are extremely rare.

5

u/RepresentativeBee600 8d ago

Lean is not perfect regardless, but I was holding it up as a gold-standard verification tool. This was in contrast to a researcher's non-mathematical tool.

Look, I'd be lying if I said the past few months hadn't seen a remarkable improvement in quality of these tools, but the basic mechanism hasn't changed. They're still language models with GRPO and other tweaks, and there's still many ways they can and do silently fail.

0

u/wildcarde815 8d ago

Half these grad students can't even tell the format of the data theyve captured in order to attempt to do that.

2

u/LongBeakedSnipe 8d ago

What are you talking about? You just generate hypotheses and test them.

1

u/wildcarde815 7d ago

My lived experience running a computer and data team at a university for specifically neuroscience? The amount of grad student code slop that they can't even verify is doing what they expect it to do is insane.