We’re reaching a point where the interesting part isn’t just whether an AI found the proof: it’s whether anyone outside the company can reproduce the result. Publishing Lean proofs is great. Keeping the model closed means the process stays a black box.
this post was submitted on 02 Aug 2026
13 points (62.3% liked)
Technology
87214 readers
3809 users here now
This is a most excellent place for technology news and articles.
Our Rules
- Follow the lemmy.world rules.
- Only tech related news or articles.
- Be excellent to each other!
- Mod approved content bots can post up to 10 articles per day.
- Threads asking for personal tech support may be deleted.
- Politics threads may be removed.
- No memes allowed as posts, OK to post as comments.
- Only approved bots from the list below, this includes using AI responses and summaries. To ask if your bot can be added please contact a mod.
- Check for duplicates before posting, duplicates may be removed
- Accounts 7 days and younger will have their posts automatically removed.
Approved Bots
founded 3 years ago
MODERATORS
I don't understand enough about math and lean proofs - do you mean it's possible nobody can interpret and explain how the proof goes in "human language"?
The impressive part isn’t that an AI produced a proof, it’s that Lean lets everyone verify it. The frustrating part is the model stays closed. Science advances fastest when others can reproduce both the result and the method, not just inspect the finished homework.
But they do plan to release the Astra model to the public "after it's finished" I assume?
And yeah this Lean software sounds amazing, didn't know this was possible.
I misread your last sentence in a way that create a different problem: Imagine AI starts producing more and more proofs at a pace that humans can't keep up with. So science advances, and humans can even make use of it, but can't verify or really understand the theory any more. Like we get better working machines, materials and processes, but do not understand why because we can't keep up. If that happened then that I guess would a significant stage in the singularity.
It would be surprising if they didn’t release Astra. And yes, we’re living in crazy times.
Ok so? Do the proofs hold up or not?
The question is: are those real proofs, or just AI reasoning bugs again?
In other words its all marketing bullshit.
So youre suggesting they secretly have Einstein standing in the server rack, making loud fan noises with his mouth and just typing really fast?
Either the problems were solved or they weren't. If they were, then that's evidence enough; doesn't matter if they model isn't publicly available.
Having those sudden breakthroughs come from a person or even a large group of mathematicians, suddenly and all at once, would be more surprising than a well-harnessed LLM figuring it out.
With that said, I'm curious about peer review of the actual proofs. Just because Lean builds them doesn't mean they're materially valid. It could very well be that it's completely wrong and it just hallucinated well enough to fool OpenAI into publishing it, which would be a hilarious egg-on-face moment
I agree with you. If it solved it, it solved it. The title is an odd phrasing.
A few of the erdos problems have been independently verified. It's legit.
The thumbnail itself is the silliest ai shit. So his shirt becomes his arm then turns into his shirt at the wrist. And thats why these idiots are so mad. They are too stupid to see how actively bad it all is, but that's your fault for being perceptive, not theirs for being a compulsory idiot. These people are so lucky breathing doesn't require critical thought.
To believe anything these companies claim about their model is to demonstrate you're a gullible simpleton. You're exactly the type of non-critical thinker they need to thrive.