DiffNo. 027

Monday, October 12

3 new · 4 still open · ~60 s

landscapetooling

Linus Torvalds uses Claude Code on the kernel

Linus Torvalds working on a Linux kernel improvement with Claude Code is the strongest signal yet that AI-assisted coding has moved past app-layer convenience into the most conservative, highest-stakes corner of software engineering — a community that has historically treated automated code generation with open hostility. If it holds up through review, every argument that AI-written code can't meet rigorous scrutiny just lost its hardest counter-example. As the person reviewing how her own team handles AI-written code, it's worth watching whether kernel-style review (one patch, one maintainer, full audit trail) becomes the template everyone else copies.

via phoronix (via lobsters)

debateindustry

The widening gap in AI capability awareness

Karpathy's funnel — roughly 75% of people have barely touched an LLM, ~20% see 'derpy chatbots,' 0.2% of professionals watch agents complete weeks of work from a prompt, and a few thousand people inside frontier labs watch swarms of thousands of agents run at machine speed — is a sharper articulation of why AI discourse feels so disconnected: almost everyone is reasoning from a different tier of the same technology. It's worth holding onto before taking any 'the public doesn't get it' or 'this is overhyped' argument at face value this week. It's close to her stated interest in how frontier labs actually use agents day to day — this is effectively a field report from someone who has sat in several of those tiers.

via andrej karpathy on x

lessonresearch

A possible soundness bug undermines Lean4 proofs

A critic claims 90% confidence that Lean4's current implementation harbors a bug serious enough to let the system formally 'prove' True equals False — a direct challenge to the soundness of the exact tool OpenAI leaned on this week to certify its 90 solved open math problems. It's a sharp reminder that a proof assistant's output is only as trustworthy as its own unverified kernel, and 'machine-checked' has been doing a lot of unexamined work in recent AI-and-math coverage. That distinction — between a result being checked and a checker being trustworthy — is exactly the kind of gap her Ph.D. training in experimental rigor would flag immediately.

What’s Formal verification and proof assistants (Lean4)?

Lean4 is a proof assistant: a programming language plus a small trusted kernel that mechanically checks whether a mathematical proof, encoded as a formal object, actually follows from its axioms by pure logical inference — no persuasive-but-wrong argument can sneak through if the kernel is sound.

It became the go-to validation layer for AI-generated math results for a simple reason: an LLM's informal proof sketch is unreliable, but if the model can additionally emit a Lean-checkable formal proof, acceptance no longer depends on trusting the model's reasoning — only on trusting the kernel that checks the formal proof. That's exactly the role it played in OpenAI's 90-problems release this week.

The critique argues the kernel itself — the small trusted core every proof ultimately reduces to — may contain a bug that lets a false statement be 'proven,' which would mean every proof Lean4 has ever certified, not just the AI-generated ones, rests on an unexamined assumption.

Lean's maintainers haven't confirmed the bug, and most practitioners expect a careful fix rather than a crisis. But the episode stress-tests an assumption quietly built into this year's AI-and-math narrative: that 'formally verified' removes the need for human trust rather than just relocating it.

via lesswrong