Comment by autuni

9 hours ago

No, in their original blog they wrote:

> As part of our GitHub repository, we are sharing formalizations of many of the proofs in Lean, a programming language that allows mathematical proofs to be checked by a computer. We will update the repository with more formalizations as we obtain them.

Meaning they published all results before checking all of them, and intended to add more Lean proofs later. In the linked post they state ~42% of the posted results now have formalized proofs, some were added, some verified, and I assume this means that some results turned out to be wrong.

45 comments

autuni

Reply
mrpopo  8 hours ago

This is extremely disappointing. It means they are sharing unproven work for PR, forcing the mathematicians community to do the verification job for them, while so-called "accelerationists" surf on the hype and help with the pro-AI propaganda.

If your AI tool can help advance mathematical research, share the tool with mathematicians. Using it like this is irresponsible.

"AI will kill us all": no. Greedy humans will kill us all. With AI.

  • solidasparagus  8 hours ago

    Every option is going to lead to someone shitting on OpenAI for what seems to be a pretty huge accomplishment. There have been opinions written by some mathematicians that OpenAI should just share the work that they have now so that people who are working on any solved problems can know. Which seems reasonable to me.

    • rich_sasha  8 hours ago

      It’s a funny one. I’m not sure what a Lean-less LLM proof even is. LLMs are amazing at bullshitting and skipping key steps and details. I’d imagine a LLM non Lean proof to be generally hard to evaluate - harder than that of a human mathematician perhaps. And the scale effect is against OAI here - the firehose just keeps squeezing out proofs.

      1 reply →

    • d0liver  3 hours ago

      I don't think that's true. If what you're doing is building a fuzzer for mathematical proofs then just say that? The fact that it's doing some of the initial work on hard problems is cool. So is the fact that the promise of that new approach is having a social effect of crowd sourcing talented people to follow up on that work. No need to try to misrepresent it as more than that.

    • ViktorRay  7 hours ago

      It’s not unreasonable to want OpenAI to be thorough and rigorously check their work before sharing it though. Sounds like that didn’t happen here.

      4 replies →

  • est  8 hours ago

    > they are sharing unproven work for PR, forcing the mathematicians community to do the verification job for them

    Lean 4 is relatively a new thing, last time I checked the formalization of undergraduate level mathematics isn't entirely done yet.

    example https://ai.math.uw.edu/projects/spring-2026/

    Lean itself is very hard to get rigorously correct, if you have every tried it yourself. I am not surprised if some AI even tries to benchmaxx Lean 4 by some loopholes

  • viraptor  6 hours ago

    > forcing the mathematicians community to do the verification job for them

    What do you mean? They're publishing the Lean proofs themselves. Who's forced into anything?

    • JohnKemeny  5 hours ago

      They are not publishing Lean proofs. They are publishing proofs in natural language, and are not submitting to journals.

      They are just putting out a bunch of weirdly written extremely long and technical papers and saying: Hey, here is the solution (we hope there are no mistakes).

  • happa  8 hours ago

    But that exactly how human mathematicians do things. They upload their research to preprint services like arXiv as they await it to be peer reviewed and accepted into a journal. Why is it okay for mathematicians to publish preprint papers, but when OpenAI does it, it's irresponsible?

    • autuni  8 hours ago

      The difference is that human mathematicians wouldn't post it online, claim they have achieved some proof, and then check after publication and announcing the results to the world. You would always check your work first, then publish it. It's not about preprint vs peer-reviewed. That of course is normal practice, it's the high-profile claims that are being made that are the problem here. They just blindly published results produced by the LLM, with 0 due diligence.

      3 replies →

    • mrpopo  8 hours ago

      See DDOS. That's exactly how humans access a web page. Why is it okay for humans to access a webpage, but when a bot swarm does it, it's irresponsible?

      That's an analogy among many others, but the point is that OpenAI should use their tools responsibly. If they have 700 potential ground-breaking but unproven results, they should share it in a way that they do not get free (possibly unwarranted) publicity for it.

      1 reply →

  • cm2187  8 hours ago

    Irresponsible? You can safely ignore the GitHub repo if it bothers you so much. You can safely browse away.

    • freecodeio  7 hours ago

      I don't think people in power that can affect my life with their decisions are ignoring this, or that they have a math background.

    • mrpopo  8 hours ago

      The "irresponsible" part is about how orange buffoons in power will read this, and immediately defund all universities, and mathematicians will lose their jobs, leaving us with nothing but an AI tool that no one can keep in check anymore.

      3 replies →

  • bbor  8 hours ago

    No, it's the exact opposite, actually. They were sharing them early on advice of mathematicians -- they were criticized for being opaque for too long with previous announcements. OpenAI is in ~bad faith, but this isn't a sound criticism.

    Also you are deeply confused about what accelerationism is, I believe. Sorry.

  • frizlab  8 hours ago

    I fail to see how this is disappointing. It was obvious from the start that it was what was happening, there is no disappointment to have!

  • pluc  7 hours ago

    If you're disappointed OpenAI is an unethical hype machine that's on you man

    • mrpopo  5 hours ago

      AI is an incredible tool, and yes I am disappointed that every leader in this field is acting unethically and irresponsibly because they want to "win" a race that would make them slightly richer than the loser.

  • AIblemblio  6 hours ago

    This is not propaganda, this is real AI progress and massivly too.

    And im completly lost on why you think sharing progress is irresponsible? Its not a recipe for building a nuclear weapon at home in 5 easy steps.

    THese are Math proofs.

    Either a Mathematican ignores it, or not. Thats the only risk.

    • andriy_koval  5 hours ago

      It were published proofs of unknown quality (how did they verify it) and unknown peer-review process. Its lower standards than usually accepted for math proofs.

      1 reply →

  • davidguetta  7 hours ago

    oh come on. even andrew wiles made a mistake and his original proof was still instrumental for the final proof of fermat's last theorem

devy  4 hours ago

Generating Lean proof is much harder and time consuming so these errors made were probably discovered during Lean proof stage.