Formalization of the Millennium Prize Problems

Stream: general

[Robert Joseph]

Hey everyone! I am excited to release a work that I have been working on. The goal of this project is to formalize the Millennium Problems in the Lean. As many of you know the Millennium Problems are seven problems in mathematics that were stated by the Clay Mathematics Institute in 2000. A correct solution to any of these problems results in a one million dollar prize.

The github link is under the LeanDojo organization: https://github.com/lean-dojo/LeanMillenniumPrizeProblems

Also I have included detailed comments in all the files/plus relevant simplified explanations according to me: )!

Note: I tried to formalize the problems as accurately as possible. However, I am not a mathematician, so there may be inaccuracies in the formalizations. If you find any inaccuracies, please let me know or even open up a PR! The formalizations are complete in the sense that I use definitions (That are important to define the conjectures) that have sorries in them, and I do not prove all definitions/theorems that are needed to formalize the problems. I hope that this project can be a starting point for a bigger project where we can formalize all the definitions and theorems needed to fully say the formalization of the conjectures is complete from the ground up, like the Poincaré Conjecture formalization, which is already in Mathlib.

Also the Readme as the full details of all the status of the problems formalized! As of now the NS Unbounded domain, Riemann Hypothesis, and Poincare are fully formalized! PvsNP is almost done, just have to prove one more sorry: ) if someone wants to help prove that it would be great, similarly for the NS on the Torus (they are equivalent formulations as shown in this doc: https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf)

The hardest ones were the Hodge, YangMills and Birch which I had to take time to understand myself and come up with some basic definitions! So we will definitely need more domain experts to come and help formalize many parts of the definitions.

Lastly, I hope that we can make this a bigger formalization project with more domain experts! Also regarding the PDE part: ) more updates on that soon for another project! Maybe there should be an eight Millennium prize for the full formalization with proofs (assuming all of them are solved) of almost all of math in lean but one can hope:)!

[Kim Morrison]

@Robert Joseph, can you please state really prominently (bold, scrolling marquee, I don't care :-) in the README that this project is about the statements not the proofs. I know this, and one would hope everyone knows this, but ... better safe than sorry.

[Kim Morrison]

I think there are some problems. e.g. in https://github.com/lean-dojo/LeanMillenniumPrizeProblems/blob/main/Problems/NavierStokes/MillenniumRDomain.lean, the final statement is

def MillenniumProblemStatement (problem : MillenniumProblem) : Prop :=
  ExistenceOfSmoothSolution problem ∨ BreakdownOfSmoothSolution problem

but problem contains the initial conditions! The dichotomy needs to say that either for all initial conditions, there is a smooth solution or that for some initial condition, there is no smooth solution.

Currently what you've written doesn't do this.

[Kim Morrison]

Also, I don't think the default value of nse in MilleniumProblem can possibly be what you mean...

[Kim Morrison]

Writing something like

structure SmoothProjectiveVariety (K : Type*) [Field K] where
  /-- The underlying scheme -/
  X : Scheme
  /-- The scheme is defined over the field K -/
  base_field : Type*
  /-- The scheme is smooth -/
  is_smooth : Prop
  /-- The scheme is projective -/
  is_projective : Prop

is fundamentally wrong. Maybe you can write is_smooth : sorry, but writing is_smooth : Prop allows someone to create a variety using { ..., is_smooth := 1 + 1 = 3, ...}.

[Kim Morrison]

(The work you've done on Navier-Stokes looks like it has some good stuff. But given how far we are from even stating BSD or Hodge, I would suggest that this work would be better as a more focussed repository that just treats NS.)

[Jz Pan]

I think maybe it's not hard to prove that the Hasse-Weil L-function for an elliptic curve over Q converges on certain right half plane. So maybe you can state a cheat version of BSD that

if there exists an entire function which agrees with Hasse-Weil L-function on certain right half plane, then its order of zeroes at 1 is equal to the Mordell-Weil rank

[Jz Pan]

Or you can state BSD alongside with modularity that

there exists an entire function which agrees with Hasse-Weil L-function on certain right half plane, and its order of zeroes at 1 is equal to the Mordell-Weil rank

[Jz Pan]

Or, since the proof of Mordell-Weil theorem is not in mathlib yet, you can state Mordell-Weil + modularity + rank part of BSD

[Joseph Tooby-Smith]

Parts of the Yang-Mills part would make a good contribution to PhysLean, where there is already some material which would help fill in the sorries and we would eventually want a formal definitions of Yang-mills theory and gauge fields. However, it would be nice if things like GaugeField were done more properly and generally using principal bundles (see here).

[Kevin Buzzard]

My understanding from a talk of Hales is that it is not possible to formalise Yang-Mills and that the problem is not actually well-defined, it is more along the lines of "we'll know a solution when we see it". I've had students work on BSD before, and Mordell-Weil; it doesn't matter that we don't have a proof of Mordell-Weil because we're not going to have a proof that the L-function has analytic continuation for years (my work will give meromorphic continuation which is enough for the statement, but this will take years), you just assume the result as part of the statement. Strong BSD only makes sense if the Tate-Shaferevich group is finite and this is still not known in general so even the informal statement of strong BSD is of the form "assume some stuff that isn't known. Then..."

[Mario Carneiro]

Kim Morrison said:

The dichotomy needs to say that either for all initial conditions, there is a smooth solution or that for some initial condition, there is no smooth solution.

Unless there are some more definitional subtleties here, isn't this trivial by LEM?

[Kim Morrison]

Yes. The point is that you have to pick one in order to win the prize.

[Eric Wieser]

What was your reason for using

/-- General space of dimension n -/
abbrev Euc 𝕜 n :=  (Fin n) → 𝕜

instead of EuclideanSpace which comes with the right inner product structure already? Your standardBasis is then docs#EuclideanSpace.single, your euc_proj is then docs#EuclideanSpace.proj, etc

[Kevin Buzzard]

Kim Morrison said:

Yes. The point is that you have to pick one in order to win the prize.

I think that with BSD you even have to pick the one they wanted you to pick? Someone once told me that if you disprove BSD with an argument of the form "consider $Y^2=X^3+37X+12345$; the computer says that the algebraic rank is 0 and the analytic rank is 2 so it wasn't true after all" doesn't give you a million bucks.

[Damiano Testa]

I think that BSD is not the only such problem, where the Millenium prize is awarded for an "intended solution", but a disproof would only receive a prize subject to some further approval.

E.g. a disproof of the Poincaré conjecture may not have awarded a prize, just like a disproof of the Riemann Hypothesis may not.

[Julian Berman]

Just for my own curiosity, the rules seem to be here and say:

If, in the opinion of CMI, the counterexample effectively resolves the Problem, then CMI may recommend the award of a Prize.
If, alternatively, the counterexample shows that the original Problem survives after reformulation or elimination of some special case, then CMI may recommend that a small prize, of an amount to be determined by CMI in its sole discretion, be awarded to the author.

[Alex Meiburg]

Yang-Mills is a bit 'open-ended' in the sense that are several reasonable formulations in terms of different axioms for a QFT. ("Axiom" here in the sense that we talk about "the group axioms", not Lean axioms.) I think people _generally_ sort of expect that these are mostly equivalent, but, no one's holding their breath. Seeing any of these formalized would be pretty satisfactory as a formalization problem, I think.

But (in my entirely personal opinion, and given my current estimate of the work necessary) the act of fully formalizing in Lean a statement of the Yang-Mills existence and mass gap problem would be enough of an undertaking, with enough new mathematical decisions and physical subtleties to consider, that it would be a project pretty much worthy of a PhD. Like, if a student did this as their main project+paper for a physics PhD, that would be enough to merit getting the degree. So take that as a warning before embarking!

[Alex Meiburg]

It is possible that I'm wildly off-base with this and formalizing the problem is much easier than I think. But that's my impression from the talks I've seen.

Regardless, very cool project. :)

[Chris Henson]

A fully impractical but fun situation I've considered is if a bidirectional implication were found between two problems. Would it count because you would eventually (assuming one of the problems is solved in the future...) have a proof? Maybe they would let you negotiate to get an early payment in case it takes longer than your lifetime :joy:

[Kevin Buzzard]

Bhargava proved that 60% of elliptic curves satisfied BSD but the committee did not award him 600K

[Alex Meiburg]

To point out a few of the issues in YangMills:

• LieAlgebra is already in Mathlib, I would recommend using that. Similarly, IsNormalSubgroup and IsConnected are unneeded. You can use e.g. docs#LieAlgebra.IsSimple .
• You're trying to talk about Riemannian manifolds (and their metrics), but in fact you're just using plain old manifolds. A lot of it is sorryed out at the moment so it's a bit tricky to tell, but I think you're missing some statements about the compatibility of the smooth structure.
• Your LinearOperator is just defined as H → H - so it's a function, with no requirement for linearity at all! While Mathlib has linear operators of course, QFTs are not finite dimensional, and you need more than just linearity. Typically something like bounded operators, and you only trace against trace-class operators. Trace-class operators are not in Mathlib, and need to be constructed separately ... there's a prototype floating around somewhere on GitHub
• Your definition of hilbertSpace misses the topological aspect of Hilbert spaces, also you wrote it as a real vector space instead of a complex space. You can see the "canonical" spelling of Hilbert spaces, as used in Mathlib, at docs#OrthonormalBasis.toHilbertBasis for instance. (There E is a Hilbert space over 𝕜; you want ℂ.)
• In general, given that spacetime is infinite, you really don't want to take the Hamiltonian as just some operator on your Hilbert space. If you take a finite energy-density field across all of space, then you'd end up with an infinite expectation value of your energy - implying that the Hamiltonian isn't a bounded operator! Which makes it very difficult to handle correctly. What you want is a Hamiltonian _density_ that you integrate across space. Then you have some appropriately tempered average energies you can talk about.
• But really, no one would want to specify Yang-Mills in terms of the Hamiltonian (unless they're, say, building a time-stepping simulator or something...) because this kind of ruins the minkowski symmetry. It's much better to use a Lagrangian here. This is the typical Yang-Mills action that one would encounter in a textbook.
• The "existence" part of the problem statement might need some theory of the renormalization group to be a well-defined question. Nonabelian Yang-Mills has a trivial UV fixed point, so really specifying it directly in this way directly (a microscopic Lagrangian) might be a dead end -- I think you may need to start with an effective theory with a cutoff, and say that it UV completes under RG towards a microscopic Lagrangian consistent with Yang-Mills. Or something like that. I'm not an expert here enough to say for sure ... but it doesn't look like how I'm used to thinking about things.

[Robert Joseph]

Kim Morrison said:

Robert Joseph, can you please state really prominently (bold, scrolling marquee, I don't care :-) in the README that this project is about the statements not the proofs. I know this, and one would hope everyone knows this, but ... better safe than sorry.

Thanks, I just did that!

[Robert Joseph]

Kim Morrison said:

I think there are some problems. e.g. in https://github.com/lean-dojo/LeanMillenniumPrizeProblems/blob/main/Problems/NavierStokes/MillenniumRDomain.lean, the final statement is

def MillenniumProblemStatement (problem : MillenniumProblem) : Prop :=
  ExistenceOfSmoothSolution problem ∨ BreakdownOfSmoothSolution problem

but problem contains the initial conditions! The dichotomy needs to say that either for all initial conditions, there is a smooth solution or that for some initial condition, there is no smooth solution.

Currently what you've written doesn't do this.

Oh that is a good catch: ) I see the issue, so a potential fix that I can see, where now I have quantified over the problems which is the following setup? or does this not work

  1. Either for ALL valid initial conditions (smooth, divergence-free, finite energy),
     smooth solutions exist for all time (global existence)
  2. OR there EXISTS at least one valid initial condition for which
     no smooth solution can exist beyond some finite time (finite-time blowup)
-/
def MillenniumProblemStatement : Prop :=
  (∀ problem : MillenniumProblem, ExistenceOfSmoothSolution problem) ∨
  (∃ problem : MillenniumProblem, BreakdownOfSmoothSolution problem)

[Johan Commelin]

Yes, with the meta-caveat that the proof term MUST(!!!) start with Or.inl or Or.inr.

[Johan Commelin]

Because otherwise it is trivial to prove this using LEM, as Mario pointed out above.

[Robert Joseph]

Kim Morrison said:

Also, I don't think the default value of nse in MilleniumProblem can possibly be what you mean...

sorry what do you mean by this? I can see an error that nu = 1 should not be set to assume WLOG, and so it should be any positive constant correct like in the problem? also I see that I set the force to be 0, let me update that and just keep it to be any general force but with the caveat that it follows this rule, ill make an update to formalize that soon!
image.png

[Robert Joseph]

Kim Morrison said:

Writing something like

structure SmoothProjectiveVariety (K : Type*) [Field K] where
  /-- The underlying scheme -/
  X : Scheme
  /-- The scheme is defined over the field K -/
  base_field : Type*
  /-- The scheme is smooth -/
  is_smooth : Prop
  /-- The scheme is projective -/
  is_projective : Prop

is fundamentally wrong. Maybe you can write is_smooth : sorry, but writing is_smooth : Prop allows someone to create a variety using { ..., is_smooth := 1 + 1 = 3, ...}.

Aah I see, thank you for letting me know that! I can make a change to that then: )!

[Robert Joseph]

Kim Morrison said:

(The work you've done on Navier-Stokes looks like it has some good stuff. But given how far we are from even stating BSD or Hodge, I would suggest that this work would be better as a more focussed repository that just treats NS.)

Thanks: )! Yeah that sounds good, I can just expand on the NS one more, but can keep some of the others as just placeholders if anyone wants to contribute to that! Thanks for your comments.

[Robert Joseph]

Jz Pan said:

I think maybe it's not hard to prove that the Hasse-Weil L-function for an elliptic curve over Q converges on certain right half plane. So maybe you can state a cheat version of BSD that

if there exists an entire function which agrees with Hasse-Weil L-function on certain right half plane, then its order of zeroes at 1 is equal to the Mordell-Weil rank

Interesting, let me think about it as well as if you have some references on this cheat version for me to read upon?

[Robert Joseph]

Joseph Tooby-Smith said:

Parts of the Yang-Mills part would make a good contribution to PhysLean, where there is already some material which would help fill in the sorries and we would eventually want a formal definitions of Yang-mills theory and gauge fields. However, it would be nice if things like GaugeField were done more properly and generally using principal bundles (see here).

Thanks! Yeah I did check out PhysLean: ) it has some good stuff there, however I am not a physicist so wasn't really familiar with many of the concepts. Intuitively what does principal bundles mean? I can definitely take a look and yeah it would be great if you want to contribute or start parts of the yang mill formalized with your team!

[Robert Joseph]

Eric Wieser said:

What was your reason for using

/-- General space of dimension n -/
abbrev Euc 𝕜 n :=  (Fin n) → 𝕜

instead of EuclideanSpace which comes with the right inner product structure already? Your standardBasis is then docs#EuclideanSpace.single, your euc_proj is then docs#EuclideanSpace.proj, etc

That is a good and very valid point: ) So let me give you a bit more context, when me and the postdoc initially started working on the evans textbook formalization, we went ahead with doing everything from scratch to understand the concepts and wanted to do it by ourselves so we have full control of how we create the theorems (might not have been the optimal way but it did get us to where we wanted and helped us pick up the pace by learning it well) (also to be honest both of us didn't realize https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/PiL2.html#EuclideanSpace.single this was there )

Recently we spoke to Floris Van Doorn and he was of great help to us! He did tell us about this to use, and this was like 2 weeks ago, but I didn't make the codebase change but now we are planning on replacing Euc k n by the euclidean space to make it easier when we release the PDE repo! I will keep this in mind and also try to make the edits to this repo as soon as I can: )

[Robert Joseph]

Johan Commelin said:

Yes, with the meta-caveat that the proof term MUST(!!!) start with Or.inl or Or.inr.

Thank you: ) Ill make the push!

[Kim Morrison]

Robert Joseph said:

Kim Morrison said:

Also, I don't think the default value of nse in MilleniumProblem can possibly be what you mean...

sorry what do you mean by this? I can see an error that nu = 1 should not be set to assume WLOG, and so it should be any positive constant correct like in the problem? also I see that I set the force to be 0, let me update that and just keep it to be any general force but with the caveat that it follows this rule, ill make an update to formalize that soon!
image.png

A default value is precisely that. It allows someone to override it with anything they want.

[Robert Joseph]

Alex Meiburg said:

Yang-Mills is a bit 'open-ended' in the sense that are several reasonable formulations in terms of different axioms for a QFT. ("Axiom" here in the sense that we talk about "the group axioms", not Lean axioms.) I think people _generally_ sort of expect that these are mostly equivalent, but, no one's holding their breath. Seeing any of these formalized would be pretty satisfactory as a formalization problem, I think.

But (in my entirely personal opinion, and given my current estimate of the work necessary) the act of fully formalizing in Lean a statement of the Yang-Mills existence and mass gap problem would be enough of an undertaking, with enough new mathematical decisions and physical subtleties to consider, that it would be a project pretty much worthy of a PhD. Like, if a student did this as their main project+paper for a physics PhD, that would be enough to merit getting the degree. So take that as a warning before embarking!

That is so valid! Thanks for your explanation and comments Alex. Again definitely not an expert in this field, and that is so cool! Hope some PhD student comes up with a good formalization of it or someone who has good background can atleats check the codebase to see if the definitions even if they have worries are reasonable and other structures defined. It was just my taking, but I'm very open to disucssion/PR's if there are mistakes to fix: ) Also do you have any good references for understanding the problem better?

Thanks, I hoped that this could start discussion on these problems and their formalizations.

[Robert Joseph]

Kim Morrison said:

Robert Joseph said:

Kim Morrison said:

Also, I don't think the default value of nse in MilleniumProblem can possibly be what you mean...

sorry what do you mean by this? I can see an error that nu = 1 should not be set to assume WLOG, and so it should be any positive constant correct like in the problem? also I see that I set the force to be 0, let me update that and just keep it to be any general force but with the caveat that it follows this rule, ill make an update to formalize that soon!
image.png

A default value is precisely that. It allows someone to override it with anything they want.

thanks Kim! Ill make the change and push it soon: )!

[Robert Joseph]

Alex Meiburg said:

To point out a few of the issues in YangMills:

• LieAlgebra is already in Mathlib, I would recommend using that. Similarly, IsNormalSubgroup and IsConnected are unneeded. You can use e.g. docs#LieAlgebra.IsSimple .
• You're trying to talk about Riemannian manifolds (and their metrics), but in fact you're just using plain old manifolds. A lot of it is sorryed out at the moment so it's a bit tricky to tell, but I think you're missing some statements about the compatibility of the smooth structure.
• Your LinearOperator is just defined as H → H - so it's a function, with no requirement for linearity at all! While Mathlib has linear operators of course, QFTs are not finite dimensional, and you need more than just linearity. Typically something like bounded operators, and you only trace against trace-class operators. Trace-class operators are not in Mathlib, and need to be constructed separately ... there's a prototype floating around somewhere on GitHub
• Your definition of hilbertSpace misses the topological aspect of Hilbert spaces, also you wrote it as a real vector space instead of a complex space. You can see the "canonical" spelling of Hilbert spaces, as used in Mathlib, at docs#OrthonormalBasis.toHilbertBasis for instance. (There E is a Hilbert space over 𝕜; you want ℂ.)
• In general, given that spacetime is infinite, you really don't want to take the Hamiltonian as just some operator on your Hilbert space. If you take a finite energy-density field across all of space, then you'd end up with an infinite expectation value of your energy - implying that the Hamiltonian isn't a bounded operator! Which makes it very difficult to handle correctly. What you want is a Hamiltonian _density_ that you integrate across space. Then you have some appropriately tempered average energies you can talk about.
• But really, no one would want to specify Yang-Mills in terms of the Hamiltonian (unless they're, say, building a time-stepping simulator or something...) because this kind of ruins the minkowski symmetry. It's much better to use a Lagrangian here. This is the typical Yang-Mills action that one would encounter in a textbook.
• The "existence" part of the problem statement might need some theory of the renormalization group to be a well-defined question. Nonabelian Yang-Mills has a trivial UV fixed point, so really specifying it directly in this way directly (a microscopic Lagrangian) might be a dead end -- I think you may need to start with an effective theory with a cutoff, and say that it UV completes under RG towards a microscopic Lagrangian consistent with Yang-Mills. Or something like that. I'm not an expert here enough to say for sure ... but it doesn't look like how I'm used to thinking about things.

Thank you so much for the detailed comments! I didn't see it until my previous response haha so sorry for asking more details on the other message.

Let me try to answer them point by point

1. oh I can make that change! Let me try to fix that then: )
2. Oh that's because manifolds is already there in Lean correct so I just tried to use some parts of it: ) Yeah I was trying to get smooth manifolds, as you can see in some of the definitions I commented it out by worries, is cause I wasn't able to properly define the manifold without borders
3. This is such a valid point, I completely forgot about the linearity, I will make that fix soon and oh yeah we need boundedness. I will try to find those trace class operators prototype. Thanks

4. Aah my bad, my friend who is a mathematical physicist had mentioned this and I was going to make this change but completely forgot about this. I will do that!
   5 and 6. Interesting I will try to reformulate it then in regards to these points.

5. Yeah this I'm not sure, I can read more about it and ask clarifying questions here.

[Robert Joseph]

Thank you everyone for your interest and comments! They really were helpful : ) Also I would be happy if people could comment on the other problems especially if you find mistakes for the RH, PvsNP etc!

[Robert Joseph]

Also I will be at the https://simons.berkeley.edu/workshops/simons-institute-theory-computing-slmath-joint-workshop-ai-mathematics-theoretical/schedule workshop from April 7th to 11th! So if you would like to discuss this, I would be happy to in person.

[Tomas Skrivan]

Robert Joseph said:

Kim Morrison said:

Writing something like

structure SmoothProjectiveVariety (K : Type*) [Field K] where
  /-- The underlying scheme -/
  X : Scheme
  /-- The scheme is defined over the field K -/
  base_field : Type*
  /-- The scheme is smooth -/
  is_smooth : Prop
  /-- The scheme is projective -/
  is_projective : Prop

is fundamentally wrong. Maybe you can write is_smooth : sorry, but writing is_smooth : Prop allows someone to create a variety using { ..., is_smooth := 1 + 1 = 3, ...}.

Aah I see, thank you for letting me know that! I can make a change to that then: )!

This issue is with NSE too, for example

domain : Set (Euc ℝ (n+1)) := {x | 0 ≤ x 0 ∧ x 0 < T}

so you can claim $1M by setting domain to an empty set.

You are using structure fields with default values as let bindings. They work differently!

[Tomas Skrivan]

Also

nse : NavierStokesEquations 3 := {
    nu := nu,                            -- Kinematic viscosity (from parameter)
    f := f,                              -- External force field
    nu_pos := nu_pos,                    -- Proof that viscosity is positive
    initialVelocity := initialVelocity,  -- Initial velocity field
    initialDivergenceFree := initialVelocity_div_free  -- Proof of incompressibility
  }

[Alex Meiburg]

Robert Joseph said:

Also do you have any good references for understanding the problem better?

I'm afraid not. Or rather, the good references I could think of would essentially amount to learning QFT. Which is a fun and enlightening activity! But I think most people in this server can relate to having more things they'd enjoy learning than they have time for.

If you wanted a reference anyway, I think Srednicki's book on QFT does a good job of introducing the field, and does so in a way that doesn't go so deep into the "practical" physics of e.g. electrons, pions, or calculating tons of scattering amplitudes (none of which is so relevant here). It's free online.

Nonabelian Gauge Theory (which the Yang-Mills millenium problem is about) is covered in chapters 69-73. The chapters are short; those 4 constitute only 28 pages. But of course the mathematical prereqs stretch way back.

[Dean Young]

Kim Morrison said:

Robert Joseph, can you please state really prominently (bold, scrolling marquee, I don't care :-) in the README that this project is about the statements not the proofs. I know this, and one would hope everyone knows this, but ... better safe than sorry.

I disagree because it was already clear enough that the claim here is to correctly state the proofs. I'm left unsure if this promise, already clear enough, will be left defocused.

[Kevin Buzzard]

But we don't know the proofs?

[Dean Young]

My concern is about casting doubt on peoples' ability to state things correctly.

And yes I agree we don't know the proofs.

[Mario Carneiro]

I think Kim's main concern is that people that claim to have solved a millenium prize problem are a dime a dozen and you do not want to be confused for one

[Mario Carneiro]

In particular, the topic title here is definitely ambiguous about whether it is a formalization of the statement or the proof. If I said "I have formalized the classification of finite simple groups" most people would interpret that as me having formally proved the theorem

[Dean Young]

@Mario Carneiro ok, thanks for your clarity here.

[Robert Joseph]

Tomas Skrivan said:

Robert Joseph said:

Kim Morrison said:

Writing something like

structure SmoothProjectiveVariety (K : Type*) [Field K] where
  /-- The underlying scheme -/
  X : Scheme
  /-- The scheme is defined over the field K -/
  base_field : Type*
  /-- The scheme is smooth -/
  is_smooth : Prop
  /-- The scheme is projective -/
  is_projective : Prop

is fundamentally wrong. Maybe you can write is_smooth : sorry, but writing is_smooth : Prop allows someone to create a variety using { ..., is_smooth := 1 + 1 = 3, ...}.

Aah I see, thank you for letting me know that! I can make a change to that then: )!

This issue is with NSE too, for example

domain : Set (Euc ℝ (n+1)) := {x | 0 ≤ x 0 ∧ x 0 < T}

so you can claim $1M by setting domain to an empty set.

You are using structure fields with default values as let bindings. They work differently!

Oh I see, so what would be the best way to go about doing this?

[Robert Joseph]

Alex Meiburg said:

Robert Joseph said:

Also do you have any good references for understanding the problem better?

I'm afraid not. Or rather, the good references I could think of would essentially amount to learning QFT. Which is a fun and enlightening activity! But I think most people in this server can relate to having more things they'd enjoy learning than they have time for.

If you wanted a reference anyway, I think Srednicki's book on QFT does a good job of introducing the field, and does so in a way that doesn't go so deep into the "practical" physics of e.g. electrons, pions, or calculating tons of scattering amplitudes (none of which is so relevant here). It's free online.

Nonabelian Gauge Theory (which the Yang-Mills millenium problem is about) is covered in chapters 69-73. The chapters are short; those 4 constitute only 28 pages. But of course the mathematical prereqs stretch way back.

Aah I see thank you for some of the references: )I can check them out when I have the time haha!

[Mario Carneiro]

@Alex Meiburg is it actually free online? I don't see a link to the book itself at that page, just a link to amazon

[Mario Carneiro]

oh nvm there is a draft version here

[David Loeffler]

I had a look at the Riemann hypothesis file in this project here. Note that we already have a statement of RH in Mathlib itself – docs#RiemannHypothesis – so I was curious what this file added on top of that.

One thing that jumped out at me from this file is the following:

/-- # A stronger form of the Riemann Hypothesis states that all zeros of the Riemann zeta function in the critical strip are simple zeros (i.e., have multiplicity 1).

    This means that each zero is a single root, not a multiple root, which would
    influence how certain related functions behave near these zeros. -/
def SimpleZerosHypothesis : Prop :=
  ∀ s : ℂ, CriticalStrip s → riemannZeta s = 0 →
    ∃ ε > 0, ∀ z ≠ s, ‖z - s‖ < ε → riemannZeta z ≠ 0

This is not a stronger form of RH; it is an easy theorem, because the formalisation is not saying that the zeroes are simple (or anything about them being on the critical line!) but just that they are isolated. The zeroes of holomorphic functions are always isolated (as long as the domain is connected and the function not identically 0, conditions which are trivially satisfied here), by various elementary theorems of complex analysis which you can easily find in Mathlib.

Moreover, the restriction to s in the critical strip is not needed anyway, since the zeroes outside the critical strip are well-understood. Using the properties of zeta that are formalised in mathlib, it would be an easy exercise to show that all zeroes outside the critical strip are simple. (Then you don't even need to bother defining CriticalStrip since it is not used anywhere else in the file; and that actually also applies to several of the other declarations here, such as primeCountingFunction.)

[Robert Joseph]

David Loeffler said:

I had a look at the Riemann hypothesis file in this project here. Note that we already have a statement of RH in Mathlib itself – docs#RiemannHypothesis – so I was curious what this file added on top of that.

One thing that jumped out at me from this file is the following:

/-- # A stronger form of the Riemann Hypothesis states that all zeros of the Riemann zeta function in the critical strip are simple zeros (i.e., have multiplicity 1).

    This means that each zero is a single root, not a multiple root, which would
    influence how certain related functions behave near these zeros. -/
def SimpleZerosHypothesis : Prop :=
  ∀ s : ℂ, CriticalStrip s → riemannZeta s = 0 →
    ∃ ε > 0, ∀ z ≠ s, ‖z - s‖ < ε → riemannZeta z ≠ 0

This is not a stronger form of RH; it is an easy theorem, because the formalisation is not saying that the zeroes are simple (or anything about them being on the critical line!) but just that they are isolated. The zeroes of holomorphic functions are always isolated (as long as the domain is connected and the function not identically 0, conditions which are trivially satisfied here), by various elementary theorems of complex analysis which you can easily find in Mathlib.

Moreover, the restriction to s in the critical strip is not needed anyway, since the zeroes outside the critical strip are well-understood. Using the properties of zeta that are formalised in mathlib, it would be an easy exercise to show that all zeroes outside the critical strip are simple. (Then you don't even need to bother defining CriticalStrip since it is not used anywhere else in the file; and that actually also applies to several of the other declarations here, such as primeCountingFunction.)

Thanks for your comment David! I do apologize for not including the comment that the doc already does have the RH formalized like I did for the Poincare conjecture. Oh my bad, I shouldn't have written it that way: ) I will do all the modifications that you mentioned and I included the definition the critical strip because I want people to understand basic definitions needed to define the RH prop.

[Jz Pan]

Robert Joseph said:

Jz Pan said:

I think maybe it's not hard to prove that the Hasse-Weil L-function for an elliptic curve over Q converges on certain right half plane. So maybe you can state a cheat version of BSD that

if there exists an entire function which agrees with Hasse-Weil L-function on certain right half plane, then its order of zeroes at 1 is equal to the Mordell-Weil rank

Interesting, let me think about it as well as if you have some references on this cheat version for me to read upon?

Not yet. Maybe I'll try to write it down...

[Jz Pan]

[EDIT] make things mathematically correct as many as possible

Here we go:

import Mathlib.AlgebraicGeometry.EllipticCurve.Group
import Mathlib.Analysis.Analytic.Order
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Topology.Algebra.InfiniteSum.Defs

universe u

open Cardinal Polynomial

namespace WeierstrassCurve

section CommRing

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

/-- The number of rational points of a Weierstrass curve `W` over a ring `R`.
It is zero if there are infinitely many such points. -/
noncomputable def numPoints := Cardinal.toNat #W.toAffine.Point

/-- The trace of Frobenius isogeny of a Weierstrass curve `W` over a ring `R`.
This definition is mathematically correct if `R` is a finite field. -/
noncomputable def frobeniusTrace : ℤ := Cardinal.toNat #R + 1 - W.numPoints

open scoped Classical in
/-- The **local Euler factor** `f` of a Weierstrass curve `W` over a ring `R`,
as a polynomial over `ℤ`. This definition is mathematically correct if `R` is a finite field.
The corresponding term in the L-function is `f(q⁻ˢ)⁻¹` where `q` is the cardinality of `R`. -/
noncomputable def localEulerFactor : ℤ[X] :=
  if W.IsElliptic then
    1 - W.frobeniusTrace • X + Cardinal.toNat #R • X ^ 2
  else
    1 - W.frobeniusTrace • X

end CommRing

section Field

variable {F : Type u} [Field F] (W : WeierstrassCurve F)

/-- A `Prop` which asserts that the abelian group of rational points of a Weierstrass curve `W`
over a field `F` is finitely generated. Mathematically, this is true if `W` is an elliptic curve
and `F` is a global field. -/
def MordellWeil : Prop := Module.Finite ℤ W.toAffine.Point

/-- The **Mordell-Weil rank** of a Weierstrass curve `W` over a field `F`, defined to be the
`Module.finrank` of the abelian group its rational points. This definition is mathematically correct
if such group is finitely generated. -/
protected noncomputable def rank := Module.finrank ℤ W.toAffine.Point

end Field

section Int

variable (W : WeierstrassCurve ℤ)

/-- The *fake* **Hasse-Weil L-function** of a Weierstrass curve over `ℤ`.
Since the Weierstrass curve is not necessarily a global minimal model, it misses finitely many
Euler factors compared to the mathematically correct one, namely, it is `L(E,s) * ∏ p, fₚ(p⁻ˢ)`
for some finitely many `p`. Since `fₚ(p⁻ˢ)` is entire, this function is also entire.
Since `fₚ(p⁻ˢ)` has no zeros on reals, the order of zeroes of this function on reals is the same
as the actual L-function. -/
noncomputable def fakeHasseWeil (s : ℂ) : ℂ :=
  ∏' p : Nat.Primes, (aeval (p ^ (-s) : ℂ) (W.baseChange (ZMod p.1)).localEulerFactor)⁻¹

/-- The **rank part of the Birch and Swinnerton-Dyer conjecture** for elliptic curves over `ℚ`.
It is stated as that for any Weierstrass curve over `ℤ` with non-zero discriminant, the
Mordell-Weil group of the corresponding elliptic curve over `ℚ` is finitely generated,
and its *fake* L-function has an analytic continuation to the whole complex plane,
whose order of zeroes at `1` is equal to the Mordell-Weil rank. -/
def BSD : Prop :=
  ∀ W : WeierstrassCurve ℤ, W.Δ ≠ 0 → (W.baseChange ℚ).MordellWeil ∧
    ∃ (L : ℂ → ℂ) (σ : ℝ) (han : ∀ s : ℂ, AnalyticAt ℂ L s),
      (∀ s : ℂ, s.re > σ → L s = W.fakeHasseWeil s) ∧ (han 1).order = (W.baseChange ℚ).rank

end Int

end WeierstrassCurve

[Robert Joseph]

Jz Pan said:

Robert Joseph said:

Jz Pan said:

I think maybe it's not hard to prove that the Hasse-Weil L-function for an elliptic curve over Q converges on certain right half plane. So maybe you can state a cheat version of BSD that

if there exists an entire function which agrees with Hasse-Weil L-function on certain right half plane, then its order of zeroes at 1 is equal to the Mordell-Weil rank

Interesting, let me think about it as well as if you have some references on this cheat version for me to read upon?

Not yet. Maybe I'll try to write it down...

Thank you: )!

[Robert Joseph]

Jz Pan said:

[EDIT] make things mathematically correct as many as possible

Here we go:

import Mathlib.AlgebraicGeometry.EllipticCurve.Group
import Mathlib.Analysis.Analytic.Order
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Topology.Algebra.InfiniteSum.Defs

universe u

open Cardinal Polynomial

namespace WeierstrassCurve

section CommRing

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

/-- The number of rational points of a Weierstrass curve `W` over a ring `R`.
It is zero if there are infinitely many such points. -/
noncomputable def numPoints := Cardinal.toNat #W.toAffine.Point

/-- The trace of Frobenius isogeny of a Weierstrass curve `W` over a ring `R`.
This definition is mathematically correct if `R` is a finite field. -/
noncomputable def frobeniusTrace : ℤ := Cardinal.toNat #R + 1 - W.numPoints

open scoped Classical in
/-- The **local Euler factor** `f` of a Weierstrass curve `W` over a ring `R`,
as a polynomial over `ℤ`. This definition is mathematically correct if `R` is a finite field.
The corresponding term in the L-function is `f(q⁻ˢ)⁻¹` where `q` is the cardinality of `R`. -/
noncomputable def localEulerFactor : ℤ[X] :=
  if W.IsElliptic then
    1 - W.frobeniusTrace • X + Cardinal.toNat #R • X ^ 2
  else
    1 - W.frobeniusTrace • X

end CommRing

section Field

variable {F : Type u} [Field F] (W : WeierstrassCurve F)

/-- A `Prop` which asserts that the abelian group of rational points of a Weierstrass curve `W`
over a field `F` is finitely generated. Mathematically, this is true if `W` is an elliptic curve
and `F` is a global field. -/
def MordellWeil : Prop := Module.Finite ℤ W.toAffine.Point

/-- The **Mordell-Weil rank** of a Weierstrass curve `W` over a field `F`, defined to be the
`Module.finrank` of the abelian group its rational points. This definition is mathematically correct
if such group is finitely generated. -/
protected noncomputable def rank := Module.finrank ℤ W.toAffine.Point

end Field

section Int

variable (W : WeierstrassCurve ℤ)

/-- The *fake* **Hasse-Weil L-function** of a Weierstrass curve over `ℤ`.
Since the Weierstrass curve is not necessarily a global minimal model, it misses finitely many
Euler factors compared to the mathematically correct one, namely, it is `L(E,s) * ∏ p, fₚ(p⁻ˢ)`
for some finitely many `p`. Since `fₚ(p⁻ˢ)` is entire, this function is also entire.
Since `fₚ(p⁻ˢ)` has no zeros on reals, the order of zeroes of this function on reals is the same
as the actual L-function. -/
noncomputable def fakeHasseWeil (s : ℂ) : ℂ :=
  ∏' p : Nat.Primes, (aeval (p ^ (-s) : ℂ) (W.baseChange (ZMod p.1)).localEulerFactor)⁻¹

/-- The **rank part of the Birch and Swinnerton-Dyer conjecture** for elliptic curves over `ℚ`.
It is stated as that for any Weierstrass curve over `ℤ` with non-zero discriminant, the
Mordell-Weil group of the corresponding elliptic curve over `ℚ` is finitely generated,
and its *fake* L-function has an analytic continuation to the whole complex plane,
whose order of zeroes at `1` is equal to the Mordell-Weil rank. -/
def BSD : Prop :=
  ∀ W : WeierstrassCurve ℤ, W.Δ ≠ 0 → (W.baseChange ℚ).MordellWeil ∧
    ∃ (L : ℂ → ℂ) (σ : ℝ) (han : ∀ s : ℂ, AnalyticAt ℂ L s),
      (∀ s : ℂ, s.re > σ → L s = W.fakeHasseWeil s) ∧ (han 1).order = (W.baseChange ℚ).rank

end Int

end WeierstrassCurve

oh wow thank you so much! I will take a look at it and if I have questions I will ask you and then make a change then: ) and Ill give you credit for it!

[Jz Pan]

You're welcome. I think this needs to be double checked by other experts...