Hard to Do, Easy to Check

Isaac Newton milled ridges onto the edge of a coin so that clipping it would show at a glance. This episode follows that idea, work made hard to do but cheap to check, from the Royal Mint to double-entry bookkeeping to the Lean proof assistant, and asks why AI raced ahead in code and math but stalls everywhere the only check is a person reading carefully.

Sources mentioned:

• The Great Recoinage of 1696 — Newton & the Mint, University of Oxford
• Why coins have reeded edges
• Luca Pacioli — the 1494 printed account of double-entry bookkeeping
• The Kepler conjecture — and the “99% certain” review that prompted a formal proof
• Lean — the proof assistant
• Terence Tao on formalizing his own paper in Lean

Written by Tabrez Syed. Narrated by an AI voice. A Mandalivia production.