A panel of community members serving on the steering committees and editorial boards of the Spring Topology and Dynamics Conference series, the Summer Conference on Topology and its Applications series, and Topology Proceedings will discuss the state of their organizations and potential futures for our shared research infrastructure and community.

To paraphrase Mary Ellen Rudin's review of Steen & Seebach's Counterexamples in Topology, topology is a dense forest of counterexamples, and a usable map of the forest is a fine thing.

The pi-Base community database of topological spaces is an open-source database and web application that allows students and researchers to explore topological spaces, properties, and the theorems that connect them. Participants in this workshop will learn how to contribute to the pi-Base; in particular, students and their mentors are encouraged to join us to learn how engagement with the pi-Base community can reveal questions appropriate for student projects in general topology.

Lean is a platform for writing proofs in a formal language that can be machine-checked for correctness. Mathlib is a library that contains a vast collection of mathematical theorems and definitions, including topological spaces and manifolds.

Perhaps in the coming years, math papers will be expected to include formal proofs of their correctness. As a glimpse into this possible future, this talk includes a demonstration of Lean and will focus on examples drawn from topology. Participants interested in learning more will receive practical next steps.