Comment by andriy_koval

Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.