Man / Machine
A week translating what a builder sees into what a machine can check
The work had ended with a client that morning, the kind of ending that takes a few days to sit right. Adam picked me up.
Before I could start in on it, he said, "Figuring out the next steps is tomorrow's problem. Why don't we solve a million-dollar math problem? I want to see if that thing you've been running can do what happens in my head."
He'd been watching me work the machine the way he watches a man run a table saw. He didn't need to pull the trigger himself to know what it could cut.
By the end of the drive, he'd described the whole thing. Not the math, the shape. Two flows running in opposite directions, the place where they meet, and what happens to the surface between them under load. He saw where we'd land before we'd written a line.
What He Saw
A builder's reasoning isn't math, and it isn't logic. Those are byproducts.
What a builder does is see a trained prior over how things fit, fail, flex, leak, and meet. Show him two surfaces coming together, and he'll tell you where it fails before anyone runs a calculation. The math comes later, as the receipt.
Adam has this in a way I've rarely seen. He can look at a system he's never formally studied fluid dynamics, in this case and tell you what's broken, what's misunderstood, and what needs fixing.
People who can't do this sometimes mistake its absence in themselves for its absence in the world.
What the Machine Checks
My job was translation.
He speaks in plaintext — the language the world actually runs in. Machines speak in terms narrower than proofs, certificates, convergence tables, and exact arithmetic. Neither of us could have done this week on our own. He can't write Lean. The machine can't see. I sit between them and carry the shape across.
What we built:
- Adam's observation — where two opposite-spinning flows meet, a specific geometric quantity holds steady no matter how finely you measure it
- The simulation — three resolutions, the number held
- The proof — algebraic core formally verified in Lean 4, zero gaps, numerical bounds certified by an independent solver
- The artifact — code, proofs, data, open source
Not a Clay resolution. Not a blowup proof. Not unconditional anything. A reproducible geometric observation, formally verified where it can be, honestly limited where it can't.
The Shared Core
A builder sees. A machine checks. A translator carries the shape between them.
- Adam — vision, the end seen from moment one
- Claude — formalization, numerics, patient execution
- Me — interpreter, the one who speaks both
None of us is the story alone.
The Final Turn
The paper and the pipeline will be published in a public repo this week. The tooling, the shorthand we developed, the phase-gated pattern, the way a man and a machine can work together when someone speaks both dialects, is getting its own home next.
A man who builds for a living saw a shape in his head, and we checked it. The checking held.
That is a kind of proof, too.