Brando Miranda — April 2026 · 3–4 minute read

TL;DR. In the era of AI agents, formal methods, and Lean specifically, are finally within practical reach for scalable oversight of complex arguments. Let the verifier check the answer; let the human check the question. Deciding what to ask, knowing what we actually want, is the part we may not be able to outsource.

A conversation broke out in my lab channel this week about whether AI coding assistants are actually helping us do better research, or just helping us feel like we are. It’s a question I keep coming back to, and I want to write down where I’ve landed.

The worry

A colleague laid out the concern cleanly. Long-term, he thought the usefulness of these tools splits along three axes: how much you already know, what you choose to spend their output on, and how well you parse what they produce. His sharpest observation was the third. Models generate text faster than any human can read it. Over time that speeds up the surface and slows down the understanding. You skim, you trust, you move on. Another colleague echoed it from a different angle: he’d noticed a pattern of confidence without understanding, students sure they’d found something, unable to explain why, unable to catch errors when they appeared.

I don’t think either of them is wrong. I’ve felt the same pull, and I include myself on the list of guilty parties. But the picture is incomplete, because it treats “checking” as a single unstructured activity: one human eye against an avalanche of generated text. That framing makes the problem look unwinnable. It isn’t, at least not in every domain.

The need for simple verification

In mathematics, the act of checking has a structure we don’t always take advantage of. A proof of Fermat’s Last Theorem is long, intricate, and beyond most of us to audit line by line. But the statement of Fermat’s Last Theorem is short. If the theorem is written in Lean, the kernel checks the proof automatically and deterministically. What a human actually has to verify is not the hundreds of pages of argument but a single claim: that the Lean statement faithfully expresses the informal theorem.

This is still not trivial. Autoformalization is hard, and a wrong statement with a valid proof is worse than no proof at all. But checking a translation is dramatically cheaper than checking a proof. The complex reasoning gets offloaded to a deterministic verifier. The human is freed to do the one thing that was always ours to do: decide whether the question is the right question. The quality of research, like the quality of life, depends on the quality of questions one asks.

That, to me, is what scalable oversight looks like. Not a human racing a language model through a wall of text, but a human checking the short, human-readable end of an argument while a formal system checks the long, mechanical end.

And here’s what’s new: in this era of AI agents, formal methods are within practical reach in a way they weren’t five years ago, and Lean specifically is the tool. There is no comparable alternative, and the momentum is unambiguous. AWS verifies its Cedar authorization language in Lean. DeepMind’s AlphaProof reached IMO silver-medal performance proving theorems in Lean (Nature, 2025). Harmonic and Axiom were both founded with Lean as their backbone. The community library Mathlib is past 1.6M lines and includes the formal verification of Tao’s Polynomial Freiman–Ruzsa Conjecture and parts of Scholze’s Liquid Tensor Experiment. Coordinating this ecosystem is the non-profit Lean FRO, which is fighting to stay funded; if you care about trustworthy software and AI, it is worth supporting. What used to be a niche enterprise for a handful of specialists is starting to look like a workflow the rest of us can adopt, which is exactly why scalable oversight through formal methods is a live question now and wasn’t five years ago.

How far it goes

If you believe that most of what we care about can be expressed mathematically, a lot of oversight problems reduce to “are you asking the right question?” And here’s my hot take: I think “most of what we care about” includes things people usually assume are off-limits. Love included. Probability theory is surprisingly accommodating, and I don’t see a principled reason to exempt feelings, values, or relationships from formalization in some language rich enough to hold them. The claim is not that a Lean file replaces a relationship; it’s that the structure of what we mean by one is not, in principle, beyond expression. That’s not a small residue to be left with. What remains is the most important thing a researcher does. But it’s a residue we’re equipped to handle, because it’s the part that depends on intent, taste, and knowing what you actually want rather than symbol pushing.

There are limits, at least in theory. A brief conversation with a friend reminded me that some true statements have no proof: Gödel incompleteness, the halting problem, diagonalization arguments all roughly the same shape of result. These impossibilities apply to discrete, countable systems. If reality is that kind of object, the residue matters. If reality is continuous, or uncountably infinite in some way our formal systems don’t capture, the impossibility may not bite in the same way. And here’s the honest part: which regime we’re in strikes me as unfalsifiable. We don’t get to check whether the universe is the kind of structure these theorems quantify over. So the worry is real in theory but unknowable in practice, and I’d rather say that out loud than paper over it.

What this means for the worry

The concerns my colleagues raised don’t go away under this view; they sharpen. If the human job is to ask the right question and verify the formalization, then the human has to actually understand the question and the formalization. Shallow reading is still a problem; confidence without understanding is still a problem. But the target of understanding shifts. I don’t need to hold every line of a generated proof in my head. I need to hold the statement, the definitions, and the assumptions. That’s a much smaller object, and it’s the object that actually encodes what I meant.

This is why I find formal methods so generative as a research direction, and why I care about Lean beyond its role in mathematics. It gives us a way to scale human oversight by shrinking what humans have to oversee, without pretending we’ve removed humans from the loop. We haven’t. We’re still the ones who decide what counts as the right question. Could machines eventually learn to ask it for us? Maybe they can, maybe they can’t, I genuinely don’t know. But if there’s a limit, I suspect it’s not a capability limit; it’s a substrate one. These systems aren’t running on biological neurons, they aren’t human, and knowing what a human actually wants may be inseparable from being one. Wanting isn’t obviously a thing you can outsource.

Appendix A: Lean is also a real programming language

One reason industry is converging on Lean rather than treating it as a math-only artifact is that it is a full-fledged programming language, not a proof tool with a side of code. Lean 4 compiles to native code via C, the standard library (batteries) ships with hash maps, datetime, and concurrency primitives, and the IO monad covers the system-call surface: files, processes, threads, refs, environment. Lean is implemented in Lean. In 2025 it won the SIGPLAN Programming Languages Software Award for “significant impact on mathematics, hardware and software verification, and AI.” For a guided tour of the language as a language, see Functional Programming in Lean.

The point, for this post: when you formalize a system in Lean, you are not crossing a chasm into “the math world.” You are writing a program in a language whose compiler happens to also be a proof checker. That is why the same artifact can both run and be verified, and why formal methods stop being exotic and start being a normal thing a working engineer can do.

Appendix B: A note on the em dashes

If you have read this post and noticed that I lean on em dashes, I want to flag that this is a habit I picked up from William Zinsser’s On Writing Well, in the “Bits & Pieces” chapter on the dash. Zinsser called the dash an invaluable tool, “widely regarded as not quite proper, a bumpkin at the genteel dinner table of good English,” but one that “will get you out of many tight corners.” I bought the book years before generative AI was a thing, and the punctuation has been mine ever since. I am leaving this note here because the em dash has lately been treated as a fingerprint of AI writing, and I do not want a stylistic preference I learned from a book to be mistaken for laziness. (A future post on this is in the queue.)

If you’d like to cite this post:

@misc{miranda2026formaloversight,
  author = {Miranda, Brando},
  title  = {Asking the Right Question: Formal Methods as Scalable Oversight},
  year   = {2026},
  month  = {April},
  howpublished = {\url{https://brando90.github.io/brandomiranda/2026/04/22/formal-methods-scalable-oversight.html}},
  note   = {Blog post}
}