Comment by ngruhn

> currently

A few years ago they couldn't do basic arithmetic. Is there any reason to think that capabilities flatline from now?

> proving by negation, not proving for all cases

I'm finding 2.2k "∀" symbols in the Navier-Stokes proof repo:

https://github.com/search?q=repo%3Aopenai%2FNavierStokesAndE...

It's not like can't proof universal properties.