I'm not really sure what you're asking. I wasn't commenting on any of the CAS asoects of Lean or Mathlib.

> what math would be missing

Just generally speaking, manifolds. There's no clear or standard approach in Mathlib. There seem to be approaches, but they definitely aren't turnkey.