it’s been a little scary to follow AI’s rise in ability to solve math problems. Navier Stokes especially was pretty shocking, and recently we got some more bangers like quasi-RH that i wont pretend to understand but that by all expert accounts is Fields Medal worthy. but if we look beyond the upending of an entire academic field, i think it’s worth understanding the tools with which these and many others AI miracles have come about. with math specifically, many of the solutions use Lean, a programming language that lets you write a proof and have a machine verify it's correct. fun fact: at Brown, i was the head TA for the class that taught Lean :) we’ve also seen huge feats in large-scale software. this would include Bun’s rewrite from Zig to Rust (the famous 1M line PR), or the recently viral “porting PS5 to PC” project. in both cases, the agent has a ground truth to check against, like an existing test suite or the original behavior. the common thread is that: each of these tasks allows an agent to self-verify its work with a guarantee. i’m quite late to this realization, but many thousands of dollars of token usage later, some of my most successful work has happened because of finding the right loop for the right task. need to optimize performance? autoresearch! sandbox the workload, give the agent a benchmark to improve, and leave your desk. need to land code safely? build a strong CI pipeline and have the agents go ham. even if verifiability is a fuzzy concept, you can give the agent a goal and a way to self-evaluate. it's amazingly hands free. and i think this is a great callback, because when i was learning Lean, the proof/solution itself was not always the hard part - it was mostly just being precise enough that a machine can check your work. that's the new regime with agents too: true productivity leverage isn't necessarily the prompt, but the check itself.