130k Lines of Formal Topology: Simple and Cheap Autoformalization for Everyone?