| ▲ | PunchTornado an hour ago | |||||||
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. | ||||||||
| ▲ | ndriscoll an hour ago | parent [-] | |||||||
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) | ||||||||
| ||||||||