261–270 of 525 posts
Earlier quoted context omitted.
> expressive enough to produce you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.
why should they be obvious? they are derived and have been thoroughly proven.
An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable. I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think…
Interesting to find this comment, I’ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen -and-paper proof feel to them.
Earlier quoted context omitted.
By this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.
Humans built the tool which enabled the result. AI used the tooling for eliminating the dead ends. Yes, I can appreciate the practical value of all this, but IMHO it is not a kind of breakthrough result the article gives impression of.
How much more magical do you want this to be?
Tool or not it did something you could never have accomplished.
Earlier quoted context omitted.
It's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.
Most of the kids in history died before age 5. Child mortality is very low now compared to the past, thanks to the modern medicine and technology. I am glad humanity "played God", and reduced this unnecessary child suffering.
Earlier quoted context omitted.
as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
Earlier quoted context omitted.
as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
Earlier quoted context omitted.
why should they be obvious? they are derived and have been thoroughly proven.
looks like we are in disagreement
Earlier quoted context omitted.
Humans built the tool which enabled the result. AI used the tooling for eliminating the dead ends. Yes, I can appreciate the practical value of all this, but IMHO it is not a kind of breakthrough result the article gives impression of.
A literal rock we carved patterns on and shot lightning into has accomplished something no human has. How much more magical do you want this to be? Tool or not it did something you could never have accomplished.