Building a Truth Machine

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, which is sparking a revolution in mathematics as the latest entry in a centuries-long quest for a “truth oracle.” In his new book, The Proof in the Code: How a Truth Machine Is Transforming Math and AI, Kevin Hartnett tells the definitive story of the birth and rise of Lean, the small, unlikely crew of devoted mathematicians who convinced their peers to adopt it, and the growing movement to usher in a new era of human-computer collaboration — and perhaps even machine intelligence.

Join us for a conversation between Hartnett and Thomas Lin, publisher of Quanta Books, as they explore the future of how mathematicians work, collaborate and assess truth, and grapple with the existential question: Can computers reveal universal truths?

Event attendees will have the opportunity to receive a special The Proof in the Code bookplate signed by the author. Learn more about the book and its release schedule.

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: How a Truth Machine Is Transforming Math and AI (Quanta Books, 2026) is his debut book.

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.