Lean

Lean is a language for translating mathematical proofs into a form a computer can check. Just as a teacher needs every step of your calculation written out to grade it, writing a proof in Lean means spelling out every single tiny logical step without skipping anything. In return, a computer can mechanically verify each line is correct, with no risk of a human reader missing a mistake by eye.

A typical proof written by a mathematician is a few pages of prose, full of shortcuts like 'this is obvious' or 'by the same method as before.' Human readers can fill in those gaps, but a computer can't, so translating a proof into Lean means unpacking every skipped step in full. That's why a proof that's only a few pages long can turn into millions of lines of code once it's rewritten in Lean.

This painstaking rewriting process is called formalization. Doing it by hand can take years of tedious, large-scale work, but once a proof is completed in Lean, its correctness no longer depends on human judgment at all.

The article notes that "Claude wrote up to 13 million lines of code in a proof language called Lean." Here, Lean is not a tool built by Anthropic — it's a proof-verification language that was already in use in the math community. Claude wrote a proof following this language's syntax; it did not create Lean itself, and that distinction shouldn't be confused.