Abstract
<p> 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 major topics within this conversation, this paper provides an informal survey of another class of tools for advancing mathematics research: databases of mathematical objects that enable semantic search. In addition to defining and exploring a few examples of these tools, we illustrate a particular line of research that was enabled by one such implementation: the <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="pi"> <mml:semantics> <mml:mi> Ο </mml:mi> <mml:annotation encoding="application/x-tex">\pi</mml:annotation> </mml:semantics> </mml:math> </inline-formula> -Base community database of topological counterexamples. </p>