Statements of conjectures (without a sorry)

Stream: mathlib4

[Alex Meiburg]

Would mathlib reasonably have a place hold conjectures? I don't mean theorems without a proof -- I know that adding sorrys is verboten -- but I mean that plenty of good mathematics has been done relating conjectures to each other or alternate formulations. So I'm picturing something like this,

import Mathlib

def TwinPrimeConjecture_Statement : Prop :=
  Infinite { n : ℕ | Prime n ∧ Prime (n+2) }

def GolbachConjecture_Statement : Prop :=
  ∀ n ≥ 4, ∃ a b, Prime a ∧ Prime b ∧ n = a + b

def RiemannHypothesis_Statement : Prop :=
  ∀ z, riemannZeta z = 0 → z.re = 0 ∨ ∃ n, z = -2*(n+1)

def EulerMascheroni_Rat_Statement : Prop :=
  Irrational Real.eulerMascheroniConstant

so that there is a standardized way to refer to such conjectures. Then there's a lot of nice theorems we could prove about them, like (this would be my ideal first candidate):

--The Riemann hypothesis is equivalent to the statement that, for all ε > 0,
--the Mertens function M(n)=∑_{k=1}^n μ(k) grows as O(n^(1/2 + ε)).
theorem RiemannHypothesis_iff_sum_moebius_lt_O_sqrt_eps :
  RiemannHypothesis_Statement ↔
  ∀ ε : ℝ, ε > 0 →
    ∃ c : ℝ, c > 0 →
      ∀ n, Finset.sum (Finset.range n) (ArithmeticFunction.moebius ·) ≤ c * n^(1/2 + ε) := by
  --this is a well-known proof that we can reasonably fill in
  sorry

As another example, a theorem like Tunnell's theorem is most elegantly stated as "Assuming <open problem>, we know that <foobar>." It provides an if-and-only-if relation between some solutions to integer equations, and one direction is known unconditionally, the other requires the Birch-Swinnerton-Dyer conjecture, so we could state one as "<foo> implies <bar>" and the other as "BSD and <foo> together imply <bar>".

[Yury G. Kudryashov]

This was discussed multiple times and no one implemented it.

[Yury G. Kudryashov]

One of the ideas was to make these statements typeclasses.

[Mario Carneiro]

I think there is already such a thing for FLT

[Alex Meiburg]

As a side note, there were two other places I could see this convention being nice:

• The classification of finite simple groups (CFSG for short) resolved a lot of tricky questions in group theory, albeit kind of as a hammer. Even though CFSG has been completely resolved, (1) the proof is very long and not likely to get into mathlib in any near term, and (2) I know that a decent fraction group theorists make a point of trying to prove things explicitly without CFSG. If we declare CFSG as a statement, we're free to say that other results follow from it, before we get around to proving CFSG!
• The significant majority (> 70%?) of complexity theory is done in this form. "Assuming that P does not equal PSPACE, we know that ... <bar>."

[Mario Carneiro]

docs#FermatLastTheorem

[Alex Meiburg]

Yury G. Kudryashov said:

This was discussed multiple times and no one implemented it.

Do you know if that was due to people not liking the idea, organizational questions, or just a lack of someone driving it?

[Yury G. Kudryashov]

I was talking about some support in doc-gen to highlight "conjecture" assumptions.

[Mario Carneiro]

By the way, stating CFSG is apparently the subject of a book, it's not easy in the slightest

[Mario Carneiro]

https://mathoverflow.net/questions/199874/how-do-you-state-the-classification-of-finite-simple-groups

[Alex Meiburg]

Oh I'm aware! Not easy in the slightest. :) But certainly much easier than proving it!

[Mario Carneiro]

that's the subject of 13 books and counting... :)

[Kevin Buzzard]

Stating BSD is also highly nontrivial. The usual interpretation nowadays assumes that the L-function of the elliptic curve has analytic continuation to s=1 and the only known proof of that is at least as hard as FLT.

[Yury G. Kudryashov]

An idea with typeclasses works like this:

• We decide that some namespace (e.g., Conjecture or a better name that doesn't exclude FLT or CFSG) holds conjecture statements, stated as typeclasses.
• Other theorems can assume, e.g., [Conjecture.FermatLastTheorem] and use it to prove other results.
• The documentation website shows a warning (at least, highlights [Conjecture.FermatLastTheorem] assumption in bold red instead of faded out, but we should also have support for visually impared people) whenever a theorem assumes [Conjecture.*].

[Mario Carneiro]

I don't think it's necessary to have these as typeclasses, they can just be regular assumptions to a theorem

[Mario Carneiro]

There's nothing wrong with proving implications from statements either independent, not known to hold, or having proofs which are out of reach

[Yury G. Kudryashov]

Probably, you're right, then we don't need any special support (though we can have a "tag" attribute or a yml file with the list of conjectures/hard theorems/facts independent with ZFC).

[Mario Carneiro]

If it becomes big business we can think about ways to locally make this cleaner but it's kind of a solution looking for a problem at this point

[Yury G. Kudryashov]

I think that the bar for inclusion of a conjecture statement in Mathlib should be "the author of a PR is going to prove&PR something reasonable about this statement soon" (e.g., a nice corollary or a fact that the conjecture follows from its particular case).

[Mario Carneiro]

In fact, even if we got a proof of big theorem X we may not want to make the corollaries depend on it, for dependency management reasons

[Yury G. Kudryashov]

Typeclasses can help with it. You define a TC in file A, prove corollaries in file B, then provide an instance in file C. If someone wants a proof that doesn't assume [Conjecture.*], then they can import both B and C.

[Yury G. Kudryashov]

And it just works without explicit mention of the proof.

[Yury G. Kudryashov]

Though I think that we can postpone this decision until we have at least one theorem like this.

[Kevin Buzzard]

Given that an AI just wrote lean code proving unseen IMO problems we might want to consider a "challenges" file or directory where we give them some harder problems...

[Ruben Van de Velde]

We also have docs#RiemannHypothesis fwiw

[Yury G. Kudryashov]

We should start a yml file with these statements.

[Yury G. Kudryashov]

BTW, shouldn't we mention Andrew Wiles and Richard Taylor (who else? @Kevin Buzzard knows better, I've just copied from Wikipedia) in the docstring of docs#FermatLastTheorem or in the module docstring? Kevin, could you please open a PR with some (very brief) text about references to the proof and to your project aiming to formalize the proof?

[Alex Meiburg]

An argument against typeclasses I see would be that there's not a great way to say "If X turned out false, then Y."

Of course you can flip this around and say that Not Y would give a proof of X. But that seems like a workaround more than a strategy.

By the same token, I don't think there would be an elegant way to say "X is equivalent to this particular statement Y". You can state two instances deriving one from the other, but not being able to write an Iff feels sad.

[Ruben Van de Velde]

You can still write the iff, though, and lean 4 should even be able to support instances in both directions

[Alex Meiburg]

Oh you can? My bad then, there must be something about typeclasses I don't understand properly then

[Notification Bot]

Junyan Xu has marked this topic as resolved.

[Notification Bot]

Junyan Xu has marked this topic as unresolved.

[Kevin Buzzard]

Yury G. Kudryashov said:

BTW, shouldn't we mention Andrew Wiles and Richard Taylor (who else? Kevin Buzzard knows better, I've just copied from Wikipedia) in the docstring of docs#FermatLastTheorem or in the module docstring? Kevin, could you please open a PR with some (very brief) text about references to the proof and to your project aiming to formalize the proof?

#15263

[Alex Meiburg]

Yury G. Kudryashov said:

I think that the bar for inclusion of a conjecture statement in Mathlib should be "the author of a PR is going to prove&PR something reasonable about this statement soon" (e.g., a nice corollary or a fact that the conjecture follows from its particular case).

That makes a lot of sense. I might go ahead and prove the Merten's/Riemann hypothesis equivalence (informal proof). But the Riemann hypothesis is already in there as a def. If I do, I'll maybe add a .yml mentioning these two instances -- Riemann hypothesis and FLT -- as non-proved definitions.