The Proof in the Code: A Conversation with Author Kevin Hartnett & Publisher Thomas Lin

How do we know with complete certainty if something is true? This question looms large even, or especially, in mathematics, where proofs can grow dizzyingly long and abstract, or in generative AI models that cannot distinguish between fact and fiction.

Enter the computer program Lean, the latest in the centuries-long series of attempts to build a “truth oracle,” which has the potential to revolutionize how math is done. Kevin Hartnett, the author of the new book The Proof in the Code and Quanta Books publisher Thomas Lin will discuss the birth and rise of Lean; the future of how mathematicians work, collaborate, and assess truth; and the existential question: Can computers reveal universal truths?

Kevin Hartnett is a math and technology writer whose work has been published widely in outlets including Quanta Magazine, The Atlantic, The Boston Globe, WIRED, Nautilus, and Scientific American. He was previously the senior writer at Quanta Magazine covering mathematics and computer science. His work has been collected in multiple volumes of the Best Writing on Mathematics series from Princeton University Press. From 2013 to 2016 he wrote “Brainiac,” a weekly column for The Boston Globe’s Ideas section. The Proof in the Code is his debut book.

Thomas Lin is the publisher of Quanta Books. He was previously the founding editor of Quanta Magazine, a journalist and editor at The New York Times, a board member at the Council for the Advancement of Science Writing, and an adjunct lecturer at the CUNY Graduate School of Journalism.