Remix.run Logo
▲ vlovich123 5 hours ago

Fantastic. Let’s also apply this reasoning to math papers written by humans too?

Humans produce flawed Lean proofs. Indeed LLMs were successful at finding and fixing many issues in the “core” standard library if I recall correctly. Humans regularly produce flawed papers and have minor issues require fixing. And when it happens it often isn’t as prompt and clear as this.

▲fancyfredbot 4 hours ago | parent | next [-]

I think you are implying that my suggestion is unreasonable and exceeds the standards applied to science produced by "normal" human processes.

In fact we already follow exactly this process for human papers and have done for a very long time. Publications without peer review are treated with great suspicion. This is how we end up with journals of varying levels of prestige and rigour.

The process isn't flawless and there are huge problems with retractions, as well as weird financial incentives and rent extraction but there is definitely an increased level of trust in a paper published in Nature.

▲sashank_1509 4 hours ago | parent | prev [-]

Super-intelligence that’s going to end mathematics as we know it surely must be held to a higher standard than puny humans?

More seriously the problem is the complete utter lack of care OpenAI has shown in their desperation to demoralize mathematicians with their new LLM. In their words, it took 3 hours of ChatGPT pro per result, why not spend a hundred hours per result formalizing it, checking if the formalization matches the natural language proof, and whether the argument could be made more simpler and readable. Any human paper has hundreds of hours of work put into it, but OpenAI who is absolutely adamant in demoralizing the mathematical community and demonstrating their superior “intelligence” will only spend 3 hours, write unreadable, inscrutable proofs, not formalize all of them, and then dump it on the mathematical community for some reason.