It may be. Indeed how do helicopters even fly.

But the point is that Lean formalisation is a new bar for engineering and for physics and abstract math.