前排 spring break 得閒，想做點藝術，所以畫了一幅畫（不過應該是漫畫吧？）

問題：大家知道我依據甚麼來畫嗎？這 100 塊石頭上畫了甚麼？而石頭上有七個類似棋子的東西又是甚麼？提示

詳細解答：

要理解這幅漫畫，需首先釐清漫畫中「Formalizing」一詞的意思。

1. 近十年，人工智能（AI）發展迅速，應用的範疇多不勝數，例如自動駕駛、人臉識別、投資股票、甚至下圍棋、創作音樂、畫畫等等。在愈來愈多的行業、學科都有 AI 的身影。

那數學呢？AI 可以幫助數學研究嗎？

暫時還未成氣候。為甚麼呢？其中一個原因是，要教懂 AI 做數學研究，證明定理，首先需要大量「訓練材料」，讓它學習。這就像，要教懂 AI 做人臉識別，首先需要大量的人臉照片作為訓練材料。而中國之所以在這領域如此發達，正是因為有 14 億人，加上幾億個無孔不入的 CCTV，讓訓練材料隨手可得，對培訓 AI 無往而不利。

然而，在數學，這些訓練材料仍然缺乏。不要說最前沿的數學研究，就連大學 undergraduate 課程內的東西，都還未齊全，無法訓練 AI。

2. 你或許覺得奇怪，為甚麼呢？我們有教科書，有論文，記載著所有數學知識。我們人類一直都靠閱讀這些來學數學，不能用這些材料訓練 AI 嗎？

不能的，至少不能直接用。簡言之，是因為書本或論文中的數學，都是用人類的語言寫成（英文、中文等等），電腦根本不能真正讀懂它，理解它。然而，數學講求嚴謹性。如果我們夾硬將那些數學材料塞進電腦，讓 AI 囫圇吞棗地接收，然後胡亂訓練一通，那麼最後培植出來的 AI 也將不求甚解，沒有邏輯性或嚴謹性。這樣的 AI，若要來研究數學，是不合格的。

所以，要訓練一個 AI 數學家，必須先將現有的數學教科書、論文中的文字，翻譯成另一種新的語言，讓電腦也能理解。這才是合適的訓練材料。繼而以之訓練 AI。

3. 重點來了！這個所謂「翻譯」過程，正式的名稱，便是一開始提及的「formalize」！

故此，漫畫標題「Formalize 100 Theorems」的含意，便是「把 100 個數學定理翻譯，好讓電腦也能理解」。

那麼，究竟需要翻譯成甚麼語言呢？人類自己之間溝通的語言，肯定是不合適的。至於一般的 programming language（如 C++、Python 等），雖然是人類和電腦的共通語言，但卻仍不合適。因為它們的用途根本不是 formalize 數學，不能做數學嚴格的邏輯推論。

為此，人們需要創造新語言。事實上，這些語言早就有人創造出來，例如 70 年代創造的 Mizar，80 年代的 Isabelle 和 Coq，等等。而最新的一個，是 LEAN，由 Microsoft 在 2013 年創造。每當人們需要 formalize 某些數學定理，便必定是透過這些語言。時至今日，將數學 formalize 的工作仍然有人陸陸續續在做，而且愈來愈多人投入。

4. 有一個網站，列出了 100 個比較基本的數學定理，讓人們去 formalize 它們。這 100 個定理就像是一個目標。它亦像一個比賽：幾批數學家，分別使用不同的 formalization 語言，然後看哪邊人在數量上領先。（現在 HOL Light 和 Isabelle 以 86 個領先）

在我的漫畫中的 100 塊石頭，上面就是畫了這 100 個定理。而那七個棋子，其實是其中七個 formalization 語言的 logo。

這便是漫畫的謎底。

 

作者 Facebook