本文發表於《大眾科學》的前部落格網路，反映了作者的觀點，不一定反映《大眾科學》的觀點
現在天氣又冷又多雨，你熬夜到很晚，試圖弄清楚為什麼定理中那個討厭的假設是必要的。要是你能訂購一個道路連通但不區域性連通的空間，那豈不是很好？ 你很幸運，有
一個應用程式，一個網站可以做到。 π-Base 將把一個 Alexandroff 方塊 直接送到你的家門口電腦螢幕上。
π-Base 是 Steen 和 Seebach 的著作《拓撲學中的反例》的升級版，任何人都可以為其做出貢獻。顧名思義，《拓撲學中的反例》充滿了不尋常的拓撲空間以及它們具有和不具有的拓撲性質。反例是一個具體的例子，它向我們表明某個一般陳述是不成立的。對於陳述“所有奇數都是素數”，9 是第一個反例。在拓撲學中，反例是具有一種性質但不具有另一種性質的空間，表明這兩種性質不必共存。《拓撲學中的反例》中的許多空間都非常怪異。通常當我們想到拓撲學時，我們想到的是整個“甜甜圈變成咖啡杯”的東西，在那裡我們有兩個空間，我們可以用橡皮泥製作並將它們相互變形。這本書和 π-Base 上的反例更難視覺化。例如，看看 康託的漏帳篷 （這一定是整個網站上最好的名字）。這個空間中沒有線段，所以無法用橡皮泥製作它並將其揉捏來觀察會發生什麼。
關於支援科學新聞
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞報道： 訂閱。透過購買訂閱，您正在幫助確保有關塑造我們當今世界的發現和想法的具有影響力的故事的未來。
π-Base 的創始人詹姆斯·達布斯是奧本大學的拓撲學研究生，研究餘零補空間。（別擔心，在開始寫這篇文章之前，我也不知道那些是什麼。達布斯的導師加里·格魯恩亨格有一篇關於它們的研究文章，點選此處。）這個性質沒有在《拓撲學中的反例》中出現，達布斯陷入了“令人窒息的文獻檢索”，只是為了找到例子並確定它們具有哪些其他拓撲性質。 內布拉斯加衛斯理大學的數學家奧斯汀·莫爾也有類似的感覺。“我過去在 Math Stackexchange 上相當活躍，我發現自己在回答諸如‘是否存在具有性質 x 和 y，但不具有性質 z 的空間？’之類的問題。我總是查閱《拓撲學中的反例》來解決此類問題，但如果涉及許多性質，參考圖表使用起來很麻煩，”他在一封電子郵件中寫道。他建立了一個名為 Spacebook 的網站，基本上是《拓撲學中的反例》的可搜尋版本，但當他看到達布斯正在進行一個更廣泛的專案時，他將自己的努力轉移到了 π-Base。
花費如此多的精力來尋找和描述反例似乎很奇怪，但它們在任何數學領域都很重要，這有很多充分的理由。首先，它們很有趣。無論你是在尋找連續但不可微的函式（魏爾斯特拉斯的“怪物”）還是試圖理解康託的漏帳篷到底是什麼，它們都會讓你感到有趣並拓展你的思維。
但它們對於實際（或者至少像 理論數學中的其他任何事物 一樣實際）的原因也很重要。我們希望證明儘可能普遍的定理，反例可以幫助我們檢查我們所有的假設是否都是必要的。反例還可以幫助我們找到證明。如果我們試圖證明一個具有某些假設的定理，那麼瞭解該定理在其他情況下為何不起作用會有所幫助。如果我們能比較定理在具有略微不同性質的兩個不同空間中的含義，我們就能更好地瞭解當我們去掉一個假設時會發生什麼錯誤。相反，反例也可以幫助我們對證明進行現實檢驗。如果你證明了一個定理，但你的證明適用於它不應該適用的空間，那麼你就做錯了什麼。由於所有這些原因，反例在教學上很有價值（儘管有可能做得過火——一個只包含反例列表的拓撲學課程並不理想）。反例幫助學生理解他們直覺的侷限性。
π-Base 不僅僅是《拓撲學中的反例》的可搜尋線上版本。除了列出拓撲空間及其性質外，該程式實際上還可以證明關於這些空間和性質的定理。如果每個具有性質 A 和 B 的空間也具有性質 C，那麼 π-Base 會將性質 C 新增到所有具有性質 A 和 B 的空間。這意味著人們不必手動輸入每個性質，並且該站點可以找到人們尚未費心檢查或記錄的性質。目前，該站點僅限於簡單的推論，但達布斯希望整合像 Coq 或 Isabelle 這樣的自動化定理助手來證明更復雜的定理。他還 建議，也許該程式可以“挖掘”猜想，透過找到沒有空間的性質組合，這樣它將既是一個定理建議程式，又是一個定理證明程式。
但就目前而言，人們正在承擔大部分繁重的工作，你可以提供幫助！數學家可以向該站點新增空間、性質和證明。程式設計師可以從 Github 獲取原始碼，並處理一些錯誤和所需的功能。你甚至可以點選頁面頂部的“貢獻”按鈕，以獲得一個需要證明的隨機斷言。我現在正在教拓撲學，很想把這些分配給我的學生！莫爾已在本科生研究課程中使用過 π-Base，並表示，用啟發式的人工證明取代計算機的自動化推論也將很有價值，尤其是對於學生而言。我們貢獻得越多，它對我們所有人就越有用。