Ok so I claim that doing mathematics constructively obscures ideas which, to me at least, feel natural. Let me illustrate with a simple example: a locally open set is open. (1/n)

More precisely: let X be a topological space. Say V is a subset of X with the property that for every x in V there's an open subset U of X contained in V with x in U. Question for mathematicians: how would you explain to an undergraduate that this implies that V is open? (2/n)

Here's my proof. For each x in V, choose U as in the hypothesis. Now take their union. It's easy to see that this union is V! Furthermore, a union of open sets is open. Hence V is open. A *completely* uncontroversial proof, right? (3/n)

Wrong! This proof used the axiom of choice! Of course the choice of open neighbourhood U of x is not unique, and of course in general V is infinite, and indeed even uncountable in most cases, so we just made infinitely many choices all at once. (4/n)

Why did my second year topology lecturer not make a fuss about this? Probably because most mathematicians don't care about using AC and do it instinctively. But this use of AC is unnecessary! Exercise for mathematicians: prove that a locally open subset is open w.o using AC.(5/n)

Ok so did you actually do the exercise? Or do you not actually care? I'm not sure I care. Spoiler coming up in next tweet. (6/n)

The trick with these constructive approaches is to not choose, but instead use all of them. Let S be the set of all open subsets U of X which are contained in V. No choice needed. Obviously the union of the elements of S is open, and is contained in V. (7/n)

Conversely, say x is in V. By the locally open hypothesis there exists some U in S with x in U. So x is in the union. The choice-free proof is complete. (8/n)

This proof is more elegant to a constructivist and hence actually easier to formalise in Lean, because it doesn't use AC. I claim that it is also harder to remember, and seems to rely on a "trick". In contrast the AC proof is completely natural and follow-your-nose (9/n)

But why do I think this? Is it because I was brought up by savages who used AC when not necessary and hence indoctrinated me? Here's a question. Which proof "comes first"? Which is the most organic proof? (10/n)

For me, the natural proof is the AC proof, and the constructive one is manufactured using the AC proof and a general AC removal principle which has been known to constructivists for decades but which I only learnt last Thursday from Reid Barton on the Lean Zulip chat (11/n)

Homework: give a hard-to-remember constructive proof of the statement that a compact subspace of a Hausdorff space is closed. Discuss which proof would be best for teaching. (12/n, n=12)