Hacker News Reader

Noting that planes fly but there is yet no Lean proof of Bernoulli's principle in Mathlib or Physlib.

> the trustworthiness of math itself

Is abstract math rigorously proven?

Isn't it the case that planes mostly fly because the wing has an angle of attack? (a fighter jet has no problem flying upside down)

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.

Yes. The point of the airfoil shape is to make flying more efficient, i.e. the engine would need to generate much more power if the wings were flat slabs, but the plane could still fly given a big enough engine.*

*Assuming the "big engine" wasn't so heavy that it made flight impossible because of its weight.

Reply on news.ycombinator.com