本文发表于《大众科学》的前博客网络，反映了作者的观点，不一定反映《大众科学》的观点
现在天气又冷又多雨，你熬夜到很晚，试图弄清楚为什么定理中那个讨厌的假设是必要的。要是你能订购一个道路连通但不局部连通的空间，那岂不是很好？ 你很幸运，有
一个应用程序，一个网站可以做到。 π-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，并表示，用启发式的人工证明取代计算机的自动化推论也将很有价值，尤其是对于学生而言。我们贡献得越多，它对我们所有人就越有用。