StevenXClontz’s Twitter Archive—№ 8,702

@raisinBrand_on Masters thesis pitch (not really): implement Topology2 in Lean where every open set must be non-empty and proper.