Comment by ndriscoll
5 hours ago
Researchers normally don't pay each other to read each other's work. It's a symbiotic relationship. If they think the AI results are nonsense, they could ignore it like any other crank. If they think it seems plausible and it's relevant to them, they can try to understand it. Seems fine?
> It's a symbiotic relationship
That's right, and the difference is that this one is parasitic.
Why's that? Do you think that institutions and funding agencies won't cover researchers' use of advanced models, or what? The group I worked in in undergrad had millions of dollars of equipment for doing experiments. I'd have to imagine they could get funding for a few thousand dollars in tokens for the theoreticians to have AI assistance.
> Researchers normally don't pay each other to read each other's work.
If reading each others work is symbiotic it makes sense OpenAI is parasitic: whose papers are they reading in return? No-one’s.
1 reply →
That's just money flowing into OpenAI, from the people who used to pay mathematicians.
2 replies →
yes, but in this case, openai does a lot of PR how their models solve important math problems. if it goes unchallenged, parts of society would think that is true. what would happen if we scale it and 10k companies dump 10k papers every month claiming solved math problems. how is this scalable?
We need the companies to humanly review their papers. in the same way as at other companies we use humans to review the papers.
Well, per another comment in the thread, some 20% of their solutions come with formalization, so there's a very high chance (probably higher than typical asks of research mathematics) that they did solve the problem. And that also presents a pretty easy solution to the scaling issue: demand formal proofs.
(If you're going to object that it's difficult to validate the statement of the problem, please first state your level of experience doing so. It's getting tiring seeing people raise this objection and claim that a statement is just as hard as a proof over and over who don't seem to actually know any math and have never tried to write anything in Lean)
Formalization only helps you if you prove that the formalization is correctly implemented, that the model didn’t subtly mess up or cheat.
Someone still has to read the formalization.
[dead]