[kevinbuzzard]

:-) Yes, by assuming classical logic the Lean community is taking a non-classical approach to bringing formalisation to the masses :-)