Navier Stokes Equations

[franzhusch]

What is the conjecture

One of the 7 Millennium Problems set by the Clay Mathematics Institute.

Detailed information can be found here:
https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf

[franzhusch]

Is being worked on in #1457

[Robertboy18]

This is great! I would also if possible like to contribute mine! I have spoken with the author who’s already working on this.

For completeness: I also have an independent formalization of Navier–Stokes in a different style in my repo lean-dojo/LeanMillenniumPrizeProblems. Happy to share details or align notation/statement if it helps the ongoing PR, but I won’t duplicate effort here unless requested. I can also change the defs to theorems for the formal conjecture style.

[franzhusch]

There is also a topic on Zulip on this, you can see it here:

https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Millenium.20Prize.20Problems/with/574114704