Very interesting. I think it needs to be clear that the fundamental theories (dependent type theory) is very much grounded. It's at the practical implementation of Lean4 that the critic aims at.