Mathematics Just Changed Forever — Kevin Hartnett

In this episode

Kevin Hartnett is the author of *The Proof in the Code*.SPONSOR:---Cyber Fund built the Monastery to help founders ship products that were impossible a year ago. Applications for Batch 1 are now open.Apply now: https://cyber.fund---In 1998 Thomas Hales finished a proof of the Kepler conjecture that leaned so heavily on computer code that the Annals of Mathematics could not say whether it was true. That impasse opens Kevin Hartnett’s book *The Proof in the Code*, and this documentary.Built around Tim’s conversation with Hartnett, the film follows Lean from a side project at Microsoft Research to the system mathematicians now use to check their own field. Leonardo de Moura, Lean’s creator, exp…