Smells more like hype than substance, entire article has vague sounding platitudes and lacks the specificity necessary to make 'self improving agents' work. Reads like low effort AI slop.
The multithreading bug in Isabelle is fascinating from a systems design perspective: threads racing ahead assuming a stuck proof will succeed, creating false positives. That's exactly the kind of subtle concurrency issue that makes verification tools need... verification tools.
I don't think it's that subtle: it would be enough to have a continuous integration tool that tries to compile the proofs that are checked into version control and raises an error if it fails.
The linked blog post says "Unfortunately, a student once submitted work containing this error; it was almost entirely incorrect and he had no idea." I guess the student probably was aware that not every proof had gone through, and that the that he saw like "99 out of 100 proofs succeeded" and assumed that meant that he had mostly completed the task, not realizing that a false theorem would be used to the give incorrect proofs for the rest of the file.
Indeed this can simply be checked by a command-line invocation.
But I don't think the student was aware: They would only have seen a purple coloring of the "stuck" part, as shown in the linked example in the blog post. And if one assumes that the system only accepts correct proof steps, it's very easy to miss a small error in a theorem statement...
In the described case, this was a simple user error. But you are right nonetheless: To enable the concurrency, the system uses a parallel inference kernel (https://www21.in.tum.de/~wenzelm/papers/parallel-isabelle.pd...). I have heard the anecdote that in the first version, this also allowed one to prove false, by fulfilling a proof promise with a proof that depended recursively on the same promise.
And there are verification tools for verification tools! Isabelle has a verified proof checker that can check whether a given proof is sound: https://www21.in.tum.de/~rosskops/papers/metalogic_pre.pdf
The only caveat is that the proof checker itself is verified in Isabelle...
> The share of Americans who are in the middle class is smaller than it used to be. In 1971, 61% of Americans lived in middle-class households. By 2023, the share had fallen to 51%
In 1970 1 oz of gold was ~$35 (by statute); today gold is $5,100; a few years ago it was well under two thousand dollarydoos.
Almost everybody is broke. A better way to look at this is to realize that 2025 was the highest year of spending by the Top [whatever-percentage] of consumers. The US fiat dollar's superior global position is waning, and this'll rot all economies & classes.
We're literally watching the final steps of "Trickle Down Economics" — where the wealth falls up [first slowly, then fast]. Add in some thinking machines — and it's just 21st century "slavery... with extra steps" (–R&M)
You cherry picked a line and didn't include the rest:
> But the gains for middle‑ and lower‑income households were less than the gains for upper‑income households
And you're making claims that are only talking about income (where the evidence suggests that inequality is increasing) to suggest that people are better off.
Where is the evidence that "all income levels are doing better"?
You are not able to talk about these separately. Inequality is increasing, but everyone's incomes have also increased. That means everyone has more money to spend, but also some people have more money than others. Why is it so hard for your to understand this?
Certainly the higher your fiscal positioning, the better each recent decade has felt. Sure, we all have color TVs in our pockets [/s == "rich"], but can young people even afford to educate themselves in this economy?!
I know some very poor (and rich!) doctors and lawyers. Student loans and privatized healthcare are both evil within the USA — they can capture/demoralize just about any professional.
Background: I live in a working class duplex neighborhood, adjacent to newer lakeside mansions. Few neighbors have any college education; the majority don't pay taxes (if any, net). My community is mostly pleasant, but I definitely wouldn't raise a family here (mostly single moms and blue collar workers).
Yesterday among the poorest of neighbors said to me "I'm just trying to live a simple middle class life" — and I chuckled (rudely)... then responded "I'm among the wealthier people living on this street, and I'm not even middle class anymore — and we both still rent."
We're two tenants literally scrubbing out a former smoker tenant's filth, for rent credit, so that the next working class tenant can pay this distant slumlord more Rent. Yeah, we're rich... /s
The law (and the system/society) generally serves capital, instead of humans.
That's why big corporations can both use copyright against smaller companies and individual creators, while also ignoring the same copyright laws when it suits them.
I think this is unjust. As we see capital concentrate, we see more injustice as the power balance becomes more lopsided. This isn't good for anyone, not even the super wealthy because it undermines the stability of the whole system upon which their wealth depends.
The law (and the system/society) generally serves capital, instead of humans.
That's why big corporations can both use copyright against smaller companies and individual creators, while also ignoring the same copyright laws when it suits them.
I think this is unjust. As we see capital concentrate, we see more injustice as the power balance becomes more lopsided. This isn't good for anyone, not even the super wealthy because it undermines the stability of the whole system upon which their wealth depends.
And why you think all the big boys push for ML, LLM, AI? To cut off the middle class. Once stuff will work automagicaly, they can squish even more profits while not caring about middle class at all. They will just ask automatas to do things for them... Great bright future...
> And why you think all the big boys push for ML, LLM, AI? To cut off the middle class. Once stuff will work automagicaly, they can squish even more profits while not caring about middle class at all. They will just ask automatas to do things for them... Great bright future...
To be fair, I don't think "the big boys" are so actively malicious to be seeking "to cut off the middle class." I think they push for "ML, LLM, AI" because they've made investments and see dollar signs, and they just don't care about about who is harmed or what kind of damage they do. There might also be an element of seeing the bad outcome as inevitable, and selfishly focusing on ending up on top after all the disruption vs trying to prevent or mitigate it.
Don't get me wrong, that's a terrible attitude and those are awful people. They get no points for merely not being a cartoon villain. But I think it's important to understand the situation correctly if anything's to be done about it.
reply