Writing
On the gap between a proof a machine accepts and a proof that's actually correct — and why AI-generated mathematics needs an independent human check.
The hype cycleWhen Twitter solves an open problem
Every few weeks a thread claims an AI cracked a famous conjecture. Some are real and important; many aren't — and a Lean checkmark doesn't settle which is which. A field guide.
The verification gapA green checkmark is not a proof
Lean certifies that a proof establishes a statement. It never certifies that the statement means what you intended. Here is that gap — and the numbers that show how wide it is.
Field guideFive ways a Lean proof can pass and still be wrong
Six concrete failure modes that type-check cleanly and have all shipped in real benchmarks or AI-generated proofs — with code, and how to catch each one.
The landscapeWho checks the AI mathematician?
Machines now generate proofs faster than anyone can read them. The bottleneck isn't proving — it's trust. Nobody owns the question yet.