Post

Last week in our department colloquium I showed how to formally prove that Hausdorff implies Urysohn separation. It was really easy. I just had to define Urysohn incorrectly. (And in reality: topology.pi-base.org/spaces?q=%24... )

topology.pi-base.orgπ-BaseA community database of mathematical objects, with powerful search and automated proof deduction.

ponder@ponder.ooo

lol arxiv.org/abs/2610.08144

8/10/26, 2:18 am0 reposts8 likes

Steven Clontz

@clontz.org

Then for my next act, I formally proved 0=1, by exploiting a bug I purposely added to the system. Computer aided reasoning in mathematics is going to be amazing for human researchers, actually. But right now I'm quite skeptical of these AI slop dumps...

Steven Clontz

@clontz.org

Something something #MathSky @code4math.org