Millenium Prize Problems

Stream: Formal conjectures

[Franz Huschenbeth]

There exists this repository for the Millenium Prize Problems https://github.com/lean-dojo/LeanMillenniumPrizeProblems.

We can theoretically port them, although I wonder if we should ask the authors (Robert Joseph and Alex Bishop) to do the port or if we should do it.

They could not model everything perfectly, so it might make sense to wait, on the other hand it also does not look like that there will be much more changes, as the last commit was 3 weeks ago. Or we just port the ones, which are sure.

[Felix Pernegger]

I remember the statement of Navier Dtones being misformalized there. Do you know if tvis is fixed now?

[Franz Huschenbeth]

Felix Pernegger said:

I remember the statement of Navier Dtones being misformalized there. Do you know if tvis is fixed now?

I think they fixed it, atleast it says so in this commit https://github.com/lean-dojo/LeanMillenniumPrizeProblems/commit/540da94826f70f3edf4d4fc66ce6cda20e903f61.

[Franz Huschenbeth]

But we also already have a PR for Navier Stokes FC#1457, so that might be a millennium problem that we should not port (yet).

[Moritz Firsching]

For Navier Stokes we definitely want to go with FC#1457 by @Tomas Skrivan

[Moritz Firsching]

P vs NP we already have and for the other ones it is not quite clear to me how complete the formalisations at https://github.com/lean-dojo/LeanMillenniumPrizeProblems are.

[Paul Lezeau]

I think for other problems (e.g. the Hodge Conjecture) it would be nice to do those in a way that maximises the amount of background material that can be later upstreamed to Mathlib (i.e. use this as an excuse to add some more cohomology theory to Mathlib!)

[Franz Huschenbeth]

Can you maybe open a issue for the Hodge Conjecture with the required prerequisites or do you think that doesnt make much sense yet?

[Moritz Firsching]

I think, given that we have the "Milestone", having issues for the other two would make sense: https://github.com/google-deepmind/formal-conjectures/milestone/8

[Franz Huschenbeth]

Yes, I will open the Yang-Mills one then, it is probably the furthest away from being able to formalize it.