cd /news/large-language-models/why-i-m-still-bearish-on-llms-after-… · home topics large-language-models article
[ARTICLE · art-130568] src=dank.systems ↗ pub= topic=large-language-models verified=true sentiment=↓ negative

Why I'm still bearish on LLMs after navier-stokes

A blog post argues that frontier AI labs remain overvalued because current large language models still require laborious oversight and fail outside a narrow neighborhood of their training tasks, despite headline results such as the Navier-Stokes proof. The author contends that solving reward hacking requires rigorous specification by domain experts whose time is expensive, citing hardware engineering projects where specification and validation engineers outnumber design engineers roughly 3 to 1, with 5:1 ratios not unheard of. The post notes that even Lean, the theorem prover used for the Navier-Stokes result, has had soundness bugs that let LLMs launder bogus proofs through the proof kernel.

read6 min views5 publishedSep 15, 2026

[thank you to claude fable 5.1, holden saberhagen, gabriel kammer, andres erbsen, alice mckean, and tristan wylde-larue for comments on this post]

i'll begin with a few theses for the reader to chew on:

  1. the frontier labs are priced according to the narrative that they have produced or will in the very near future produce a fully automated drop-in replacement for most knowledge workers, but current frontier models need laborious oversight and guardrails on even the simplest tasks. one misled by the headline shows of force (navier-stokes, freebsd RCEs, the huggingface incident) and frontier lab rhetoric into believing meaningful autonomy has been achieved need only look at the software firms continuing to employ and hire bottom quartile software engineers who would score far below the models they supervise on the benchmarks du jour.
  2. the models generalize well only on tasks within a small neighborhood of the specific tasks they've been trained on, and even then with severe caveats. the frontier labs have developed a general recipe to teach models almost any specific task enjoying clearly defined levels of task performance; many tasks are covered in the training data; but even small perturbations within a covered class of task result in outright failure or reward hacking.
  3. the present problem of reward hacking can be solved only by rigorous specification by domain experts. the time of domain experts is expensive. rigorous specification is itself a skill, demanding its own expertise outside of a given problem domain. even many skilled software engineers are bad at it. for the vast majority of domains, the intersection of domain experts and specification experts is ludicrously small.
  4. the labor costs of rigorous specification can greatly exceed that of direct implementation of an informal specification. the hardware engineering world presents a great case study on this, where a typical CPU project anecdotally has about three times as many specification and validation engineers as design engineers and a 5:1 ratio is not unheard of . even worse, many tasks don't admit a convenient spec-and-forget regime where you write a specification once and continuously implement against it: rigorous formal specifications frequently evolve in conversation with insights derived from discoveries made while implementing according to the informal specification. for tasks that enjoy high level one-and-done specifications (say an executable ISA specification for a family of CPU architectures) the costs of verification against such high level specifications are insurmountable with current technology, necessitating the use of lower level specifications that are both more expensive to construct and far more fragile to design flux.
  5. navier-stokes and statements in pure mathematics like it are the absolute best case scenario for agentic work against rigorous specification. the theorem statement itself is already a rigorous specification. it has undergone decades of auditing by the mathematical community and its rendering in lean is a straightforward translation defined in terms of battle-tested mathematical objects from mathlib. the verifier, the lean theorem prover, has been extensively audited and specifically designed to avoid the types of unsoundness that would make it vulnerable to reward hacks. even lean and theorem provers like it are not invulnerable: soundnessbugs have allowed LLMs to launder bogus proofs through the proof kernel before and it is not improbable that more such bugs exist. this is the rosiest setup; the vast majority of human knowledge work does not look like this. i'll comment below on the few areas of knowledge work that do resemble pure mathematics in this respect.
  6. the best alternative to rigorous specification is human review. human review doesn't scale well to the volumes of output produced by language models. to make matters worse, even expert human review is extremely vulnerable to reward hacking: consider the xz backdoor and the infamous UMN hypocrite commits that landed in linux. if human review remains a critical part of the agentic production loop, the pace of production is necessarily bottlenecked by factors like the limits of human time and attention; it is a total non-starter for the country full of geniuses in a datacenter frontier lab CEOs would have you believe is perpetually just a few more months out.

taken together, it appears that for most domains LLMs will continue to look like a cracked intern: quick and effective in the hands of an adult but not given run of the place. most firms will not be able to adopt fully autonomous AI, not for problems of skill issue or lagging technology diffusion but rather for structural reasons seemingly endemic to current architectures. the classes of firms that can accept the use of fully autonomous LLMs are few, by my count just three:

  1. those who can accept failure cheaply: firms that would otherwise hire interns, firms involved in rapid prototyping work, etc.
  2. those who need done a small set of narrowly defined tasks with existing clear guardrails: repetitive physical labor in a controlled environment, call center and customer service chat work, etc.
  3. those that can accept or already do by nature the costs of rigorous specification and validation: chip design, drug discovery, and other domains where failure on deployment is an existential concern.

the first two classes are price sensitive and arguably don't need the jump in reasoning quality you see going from cheap to frontier models. most of these firms will be best served by open models running on cheap hardware, perhaps even locally at the site of use. for the first and third classes, the type of fuzzy combinatorial search that has produced headline results in mathematics and security research seems more sensitive to agentic swarm width than reasoning capacity: see small open models reproducing the mythos CVEs that drove the spring 2026 hype cycle. if that is indeed true, there is even greater reason to use cheap open models that enable you to run the same workload with wider swarms.

the third class of firms might still use frontier models, though it's not totally clear that their work couldn't be done with cheap models like deepseek v4.1 flash, and the swarm width advantage i hypothesized above gives them all the more reason to push for cheaper models. another interesting property of firms of this class is that they are generally very secretive about their IP and probably aren't overjoyed about shipping it all to anthropic and openai even with supposed agreements to not train on user data.

now, you might propose that even if the frontier labs are cooked, the data center full of brainlets scenario drives just as much AI compute as an artificial superintelligence scenario. the difference is that the data center full of geniuses is self-driving and limited only by how much compute it can consume while the brainlet swarms will be heavily bottlenecked by their human orchestrators. my personal bet is that the blast radius will go far beyond the frontier labs.

── more in #large-language-models 4 stories · sorted by recency
── more on @lean 3 stories trending now
sponsored brought to you by zahid.host 4,200+ EU-deployed projects
reading about agents? ship yours in a single git push.

Run your AI side-project on zahid.host

EU-based hosting, git-push deploys, automatic HTTPS, no cold starts. Free tier with a custom domain — perfect for shipping the agent you just read about.

$git push zahid main
Live at https://your-agent.zahid.host
Get free account → Pricing
from €0/mo · no card required
LIVE [news/why-i-m-still-bearis…] indexed:0 read:6min 2026-09-15 ·