Change my mind: pseudogroups are the "wrong way" to formalize differential geometry.

What's wrong with formalizing charts and atlases, then a manifold is a set equipped with a maximal atlas?

We could formalize, e.g., complex manifolds using G-structures.

What is wrong with this approach?

#Mathematics #proofassistant #differentialgeometry