Recent advances in computing have changed not only the nature of mathematical computation, but mathematical proof and inquiry itself. While artificial intelligence and formalized mathematics have been the major topics of this conversation, this paper explores another class of tools for advancing mathematics research: databases of mathematical objects that enable semantic search. In addition to defining and exploring examples of these tools, we illustrate a particular line of research that was inspired and enabled by one such database.

翻译：近年来计算领域的进步不仅改变了数学计算的性质，更改变了数学证明与探究本身。尽管人工智能和形式化数学一直是这一领域讨论的主要议题，本文探讨了另一类推进数学研究的工具：支持语义搜索的数学对象数据库。除定义和探究此类工具的具体实例外，我们还将展示一条由其中某个数据库启发并实现的具体研究路径。