Papers for

computational topologists

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Counting distinct topological bases for finite sets of size N

On the Number of Distinct Topological Bases of a Finite Set of Size $N$

Abstract: For a finite set $S$ with $\lvert S\rvert = N$, the number of families $\mathcal{B} \subseteq \mathcal{P}(S)$ that are topological bases is $\#(N) = \sum_{\mathcal{T} \in \operatorname{Top}(S)} 2^{\lvert\mathcal{T}\rvert - \lvert\mathcal{M}_{\mathcal{T}}\rvert}$, where $\mathcal{M}_{\mathcal{T}}$ is the canonical minimal basis of minimal open neighborhoods. The identity is proved in Lean 4 / Mathlib (`CARDB.lean`): bases generating $\mathcal{T}$ are exactly the sets with $\mathcal{M}_{\mathcal{T}} \subseteq \mathcal{B} \subseteq \mathcal{T}$. The small-$N$ table and the discrete-dominance sandwich are proved in `CARDB/SmallN.lean` and `CARDB/Asymptotics.lean`.

Sat 12 SeptLogic in Computer Science

The gist

When you have a set with a certain number of items, there are many ways to build a structure called a topology on it. The authors found a precise formula for counting how many different basic building blocks, called bases, can generate these topologies. They used a computer proof assistant called Lean 4 to verify their results and explored small examples and growth behavior. This work helps in understanding the underlying complexity of finite topologies.

Open → 2609.14102v1