★此書預定2026年6月出版，目前有sample chapters，完整書稿預定2025年6月能提供，此書將由Farrar, Straus and Giroux與《量子雜誌》(Quanta Magazine)成立的出版品牌Quanta Books出版，Quanta Books的社長Tom Lin是《量子雜誌》的創刊總編(Founding Editor in Chief of Quanta)

★凱文·哈奈特(Kevin Hartnett)曾在2020十月發表一篇文章Building the Mathematical Library of the Future，這也是THE PROOF IS IN THE CODE這本書的創作靈感。

一位備受推崇的數學記者，講述一個微軟程式如何徹底改變數學世界的幕後故事

1998年，密西根大學教授湯瑪斯·黑爾斯(Thomas Hales)宣布他已經證明了開普勒猜想(Kepler Conjecture)，這是一道關於球體如何以最有效方式堆疊的著名幾何難題，困擾數學界長達400年。然而經過四年專家審查，數學界依然無法確定他的證明是否正確。黑爾斯的證明不僅是一篇300頁的論文，還包含40,000行的程式碼。

在當時，頂尖研究數學家普遍不信任電腦。他們認為，電腦雖然能夠快速處理數據與解方程式，但並不具備創造力與直覺，無法參與真正的數學推理。而且，即使電腦真的能幫助建構證明，誰又能確保它是正確的？

在黑爾斯試圖讓自己的證明更具正式化的同時，微軟也在尋找方法來保護其價值數十億美元的軟體產業免受網路安全威脅。軟體工程師李奧·德·穆拉(Leo de Moura)因此開發了一款名為Lean的新程式。Lean最初被設計為一款數學證明助理(proof assistant)，能夠快速且確鑿地驗證或推翻任何數學或邏輯命題。

很快，一個熱情的社群開始構建Lean的數學函式庫，讓它從一個邊緣化的工具，轉變為現代數學研究的關鍵工具。包括菲爾茲獎(Fields Medal)得主彼得·舒爾茲(Peter Scholze)與陶哲軒(Terry Tao)等頂尖數學家都開始使用Lean來驗證他們的最新數學證明。如今，Lean已經成為新一代數學家的夢幻工具，不僅推動研究發展，也進一步鞏固了數學知識的基礎。一些人甚至預測，未來Lean將成為數學的運算基礎，能夠驗證數學命題、發現新數學理論，甚至確保人工智慧的安全性。

在《AI將顛覆數學: Lean程式如何改變數學世界》一書中，數學與科技專欄作家凱文·哈奈特(Kevin Hartnett)講述了Lean的誕生與崛起，以及這場數學革命如何改變整個數學界。他用深入淺出的方式探討這個新時代的人機協作，揭示數學、電腦與人工智慧的未來走向。本書不僅是一本關於數學的精彩故事，更是一場對於「電腦是否能真正算數學？」這一問題的深入探索。