$Cover Image$

The proof in the code : how a truth machine is transforming math and AI /

"The inside story of Lean, a computer program that answers the age-old question: How do you know if something is true? It began as an obscure bug-checking program at Microsoft Research developed by a lone computer engineer named Leo de Moura. Then an unlikely crew of mathematical misfits caught...

Full description

Bibliographic Details
Main Author:	Hartnett, Kevin (Math and technology writer) (Author)
Format:	Book
Language:	English
Published:	New York, NY : Quanta Books/Farrar, Straus and Giroux, 2026.
Edition:	First edition.
Subjects:	Artificial intelligence > Mathematics > Popular works. Mathematics > Data processing. Truth > Computer programs. Machine learning. Agile software development. Computer software > Development. Computer software > Testing. Artificial intelligence. Apprentissage automatique. Méthodes agiles (Développement de logiciels) Intelligence artificielle. Intelligence artificielle > Mathématiques > Ouvrages de vulgarisation. Mathématiques > Informatique. Vérité > Logiciels. artificial intelligence. TECHNOLOGY & ENGINEERING / Inventions. Computers / Artificial Intelligence / General. Mathematics/ Logic. Popular works.

Table of Contents:

Visionaries. Tom Hales's last resort ; Truth seeker ; A lean beginning
Early adopters. Building mathlib ; A formal crisis ; The perfect(oid) stunt ; Lean together
Influencers. Big-league math ; The AI grand challenge ; Team Terry Tao ; Lean into the future.