alt Hacker NewsThis 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.
Replies
> 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
> 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?
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?
Irresponsible? You can safely ignore the GitHub repo if it bothers you so much. You can safely browse away.
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.
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.
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!
If you're disappointed OpenAI is an unethical hype machine that's on you man
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
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.