On: New Foundations is consistent – a difficult mathematical proof proved using Lean

[lmm]

> Godel's theorem shows that that context has to be stronger than T. This isn't some kind of obstruction, it is reality.

What distinction are you drawing? I see no contradiction between something being reality and something being an obstruction to be worked around.