Thariq wrote "personal software was a bit early in 2020 but in 2026, it really can be as personal as a home cooked meal, or a handwritten letter."

Ugh. The most depressing thing about the AI boom is watching tech people devalue human experience.

  On the other side of the AI-reasoning fence, the disdain seems to be mutual. “These ‘scientific’ papers from last summer — I would put this in big, big air quotes,” said Sébastien Bubeck, a member of OpenAI’s technical staff (and a prominent evangelist for the company’s reasoning models among scientists and mathematicians). He called earlier Apple results critiquing AI reasoning “wrong,” claiming that they were due to a training quirk in models that are now obsolete. “Modern models starting with GPT-5.5 do not suffer from this issue,” he said. “It would be interesting to revisit those results.” (Apple did not make its researchers available for interviews.)

  The “think” part is what OpenAI, for one, is doubling down on. When I asked Bubeck if the splashy unit distance proof was produced with methods outside the LRM’s own chain of thought — perhaps with Lean verifying its results — he seemed to find the question almost nonsensical.

  “It’s not like we’re making a mystery of it,” he said. “We have released the chain of thought. You can just go and look at it. The whole point is that the model is reasoning like a human would. And when humans reason, we don’t use Lean.” Technically, OpenAI released a “rewritten summary” of the model’s chain of thought produced by two human experts using Codex, another OpenAI model. Since 2024, the company has not publicly revealed “raw” chains of thought from its reasoning models, a policy also adopted by Google DeepMind and Anthropic.

https://www.cnbc.com/2026/07/30/leopold-aschenbrenners-hedge...

I thought they were referring to the inability of the aliens to make an accurate calendar.

Or, alternatively: refuse to accept a Lean program as a valid proof. I assume LLMs are pretty good at Lean -> mathematical English in LaTeX.

Edit: oops, see the reply below... and my grumpy response. I seriously forgot about that entire plot point.

More significantly: many major advances in scientific or mathematical programming were heralded as a thinking computer! 50's numerical scientific programming, 60's Lisp+ symbolic programming, 70's logic and symbolic algebraic programming, 80's unifying all this with encyclopedias and NLP like Mathematica - all of this is clearly useful and cool, all designed to offload intelligence... and, with modern eyes, we see plainly that not a single shred of intelligence is required to execute any of it. The AI researchers of yesteryear consistently made cool computer programs and consistently overestimated their progress at cracking human intelligence. It is plain as day to me that ANN researchers are making precisely the same scientific and philosophical mistakes as yesteryear's symbolics researchers, and even Alan Turing. This does not diminish from the coolness of the computer programs. But pretending these systems are intelligent, even "verbally" intelligent, is bad for society.

It's bad for computer science, too. None of the progress in LLMs or ANNs gets us any closer to making a robot as smart as a cockroach. I doubt any of us will live to see that milestone.

But even for a steel and concrete datacenter you would want a few carpenters for the interior where humans (at least occasionally) work, more to help with scaffolding and other temporary buildings (e..g housing) during construction, and building framing for drainage ditches and other landscaping. I imagine wood-and-nails carpenters are quite in-demand for most datacenter projects.

Note I said "meaningfully" - something with LLMs that deeply concerns me is that they provide edutainment, and people actually think they're learning something. One of the comments on this thread mentioned giving a "dense linear algebra pdf" and having an LLM use the Socratic method. I guarantee they would have learned more if they read the PDF. I strongly doubt they learned anything at all with a bunch of silly "Socratic" questions about linear algebra. But it felt like they learned something!

  Despite HAWK having survived two rounds of expert human review over a period of two years, Mythos was able to improve the best-known attack on it in just 60 hours of work—effectively cutting its key strength in half.

  Mythos’s attack works by finding a specific, previously unexploited symmetry called a nontrivial automorphism in the lattice used by HAWK. Prior work proved that efficiently finding such an automorphism would permit an attack, but did not answer if such an automorphism was accessible in the lattice used by HAWK. The automorphism discovered by Mythos allows a faster enumeration attack that, while still exponential, means that one needs to double the size of HAWK keys to achieve the same level of security.

...and it is kind of incredible to think that they spent $100,000 over 3 days looking for an automorphism. Not the possibility of an automorphism, that was already known. Man.

[1] ... or focusing too hard on the strange use of mathematical language...

The mean value theorem isn't true for the computable reals, differentiation of computable function isn't always computable, sequences tend to behave poorly, etc. There's still a lot you can say: https://en.wikipedia.org/wiki/Computable_analysis but in general calculus doesn't care about computability, that's a human problem.