I assume he's claiming to care about a great deal of math, including at each stage the equivalent of Morse-Kelley as a whole rather than just the statements it makes about sets alone.

But I don't know what post Wei Dai referred to, and I doubt I read it. Quick search finds this comment, which seems grossly misleading to me - we could easily program an AI to reason in an inconsistent system and print out absurdities like those we encounter from humans - but may have something to it.