Hard to Do, Easy to Check

Why AI raced ahead where we’d already built the check

Photo by Claudio Schwarz on Unsplash

Isaac Newton, Warden of the Royal Mint, had a problem.

A silver shilling was supposed to be a promise: this much silver, guaranteed. But the promise had a weak spot. Silver at the edge of a coin is still silver, so people shaved a thin sliver off the rim, spent the coin at full value, and kept the shavings. Melt enough of them together and you had free money. By the 1690s, England’s coins had been clipped so thin the currency was in real trouble.

The strange part is that this was never impossible to catch. You could always check a coin. You put it on a scale, weighed it against the standard, and a clipped coin came up light. The check existed. It was just too much bother to use. Nobody weighs their change in the middle of a market, or at a stall, or over a pint. So nobody checked, and because nobody checked, clipping paid. The fraud didn’t survive because the coins couldn’t be verified. It survived because verifying was expensive, and expensive checks don’t get run.

The morning after

I’ve been thinking about that gap lately, because it sits right at the heart of how we’re adopting AI.

Last week I set two agents running overnight. One took on a research project. The other built a feature in a piece of software I’m working on. By morning both had handed me something that looked finished. And I sat there with the same question about each one: how do I know it’s any good? I could go through all of it line by line, but that would take about as long as doing the work myself. And if checking the work costs as much as doing it, the agent hasn’t really saved me anything. It’s just handed me a big pile of output to inspect.

So what you actually want from any worker, human or machine, isn’t only that they’re fast. It’s that you can check their work cheaply. Some way to look at the finished thing and know it holds up, without retracing every step that got them there. The best kind of work has this built in: hard to do, easy to check. A finished jigsaw puzzle takes all afternoon to put together, but you can see it’s done from across the room. The doing and the checking come apart.

Most work isn’t like that, and that’s the trap. When the check is expensive, having a faster worker doesn’t help much, because now you’re the bottleneck, standing over a growing pile you can’t afford to look through. That’s where a lot of AI use is right now. Agents everywhere, producing code and writing and analysis faster than any human could, and almost no cheap way to tell which of it is right. We got the fast worker. We didn’t get the fast check.

Newton’s fix

Newton’s fix was to change the coin. Not the metal, not the law, the edge. The Mint started milling coins with a ring of fine ridges around the rim, and stamping a few with a raised inscription running all the way around. British pound coins carried the idea for centuries, spelled out in Latin along the edge: decus et tutamen, “an ornament and a safeguard.”

Here’s why it worked. The ridges are hard to add. You need a real mint, industrial pressure, tooling a backroom clipper can’t fake. But once they’re there, checking them costs nothing. Clip the rim off a milled coin and the ridges are gone; the edge goes smooth where it should be grooved, and you can feel it with a thumb without even looking. The check went from weighing every coin to running a finger along the edge. From a chore nobody bothered with to something you barely notice doing.

That’s the whole idea. A bit of work added up front, built into the thing itself, that tells you when something’s wrong. Engineers have a name for this: a checksum. A small, cheap tag that travels with the thing and gives it away if it’s been tampered with. Newton put one into a coin three hundred years before computers gave it a name. And notice what it does. The ridge doesn’t make the coin honest. It just makes a dishonest coin easy to spot, so you stop having to trust it and start being able to check it.

The same trick, scaled up

A coin is the small version. One object, one thumb, one check. But the same trick scales.

Take accounting. In 1494 a Franciscan friar named Luca Pacioli wrote down a method Venetian merchants were already using, and we’ve barely improved on it since: double-entry bookkeeping. Every transaction gets written down twice, once as a debit and once as a matching credit, and at the end of the day the two columns have to come out equal. If they don’t, you made a mistake somewhere, and the books tell you before anyone else finds out. The merchant doesn’t have to remember every deal. The structure remembers, and it complains when the numbers don’t line up.

Scale it up again and you get something like a tax return. A return isn’t one number, it’s a stack of forms that feed into each other. A figure on one form has to match the figure it came from on another. Columns have to add up the same way down and across. Accountants call it tying out: two numbers worked out separately have to agree. Nobody holds a whole tax return in their head, and they don’t need to. The checks are built into the shape of the paperwork, so a mistake has nowhere to hide.

There’s a catch, though, and it’s worth noticing now because it comes back later. These checks catch the wrong form, not the wrong idea. Balance your books perfectly but put a payment in the wrong account, and everything still adds up. The columns agree. The mistake sails right through. The check tells you the arithmetic is consistent. It has no opinion about whether you did the right thing.

A compiler for math

Push this idea as far as it goes and you end up in mathematics, where the thing being checked isn’t a coin or a ledger but a proof: a careful argument that something is definitely true. For most of history a proof was checked the way a contract is. An expert sat down, read it line by line, and vouched for it. That worked until the proofs got too big to read. When Thomas Hales proved the Kepler conjecture in the late 1990s, about the most efficient way to stack spheres, the reviewers spent years on it and finally gave up, saying they were “99% certain” it was right. Mathematicians don’t usually settle for 99 percent. Being sure is the whole point of the field.

So Hales, and a lot of people after him, went looking for a check that didn’t depend on a tired human reading carefully. They found it in software called a proof assistant, and the one that broke through is called Lean. The idea is close to Newton’s. At the center of Lean is a tiny, paranoid program, small enough that you can trust it completely, and its only job is to confirm that each step of a proof really does follow from the step before. You do the hard work of writing the argument in a form the program can read. In return you get a yes or a no.

Here’s what that looks like up close. Say you want to record the simple fact that a + b is always the same as b + a. In Lean you’d write a line that reads, in plain English, “for any two whole numbers a and b, a + b equals b + a.” Then you have to supply the steps that prove it, and the program checks every one. It won’t take your word for it, and it won’t accept “looks right to me.” Math gets a compiler.

The payoff is real. Terence Tao, who is about as good a checker as mathematics has, was formalizing one of his own published papers in Lean, a result that had already been reviewed and printed. Partway through, the process turned up a bug: an expression that quietly broke in one small case. Nothing fatal, and he patched it. But it was the kind of gap the best reader in the field had read straight past, because on paper it looked fine.

What no check can catch

Lean has a limit, though.

Writing a proof in a form the machine can read is a huge amount of work, often ten or twenty times the effort of just proving it the normal way. That’s why most of math still isn’t done this way. And there’s a deeper problem underneath. Lean checks that your proof follows from your definitions. It doesn’t check that your definitions are the ones you meant. State the wrong theorem and Lean will cheerfully confirm a perfect proof of the wrong thing. It’s the same as the balanced books with the payment in the wrong account. The check tells you the answer is valid. It can’t tell you the answer is right, and it definitely can’t tell you the answer was worth having.

That’s true of every check in this story, from the coin to Lean. It looks at the form, not the meaning. It can catch a mistake, but it can’t tell you that you asked the wrong question, or that nobody needed the answer. Somebody still has to decide what’s worth doing, and there’s no ridge you can run a thumb along to know you chose right.

Which brings me back to that morning, and the two agents. The one that wrote code, I can check. There’s a compiler that makes sure it runs at all. There’s a test suite that checks the parts I care about. I can set up a small mock and watch it behave. None of that is free, but it’s cheap enough that I can look at a night of work and know where I stand in a few minutes. The ridge is already built.

The research is the hard one. The agent came back with an answer, and the answer sounds reasonable, and that’s exactly the problem. How do I know it didn’t miss the one document that would have changed the conclusion? How do I know it isn’t just confidently wrong? There’s no compiler for a five-page argument. To really check it, I’d have to go do the research myself, which is the thing I was trying to hand off.

So that’s roughly where AI stands. It ran ahead in the places where we’d already built the check: code, math, anything a machine can test. It’s slow everywhere the only check is a person reading carefully. The question I keep coming back to isn’t how smart the models get. It’s how much of the world we can actually make checkable, and what’s left when we’ve built every check we can, still holding the one thing no check will catch: whether we asked for the right thing in the first place.