conjecture declaration

Stream: general

[Yaël Dillies]

What do people think of introducing a declaration type (not sure this is the technical term) conjecture which can be named, would need no proof, and can't be called (or can be called but throws a sorry-like warning)?
For example,

import data.nat.prime

conjecture goldbach (n : ℕ) : ∃ p q : ℕ, p.prime ∧ q.prime ∧ p + q = 2 * n

Of course, that's cosmetic, but maybe the kind of cosmetics we want?

[Yaël Dillies]

@Kevin Buzzard, would it be any use for your outreach?

[Ruben Van de Velde]

Might also be interesting for this to support proving corollaries of conjectures

[Kyle Miller]

You can define conjectures as Props. This doesn't require any special features, and it lets you formulate corollaries of conjectures fairly easily:

def goldbach_conjecture : Prop :=
∀ (n : ℕ), ∃ p q : ℕ, p.prime ∧ q.prime ∧ p + q = 2 * n

example (h : goldbach_conjecture) : false :=
begin
  obtain ⟨p, q, hp, hq, h⟩ := h 0,
  linarith [hp.pos, hq.pos],
end

[Kyle Miller]

I wonder if being able to put named arguments before the colon would be useful. If you do that here with goldbach_conjecture, you get a predicate on n rather than a universally quantified statement.

[Eric Wieser]

I think pre-colon arguments would be the main motivation for a special command

[Kevin Buzzard]

Yeah I think that mathlib would be enhanced with statements of eg the Birch and Swinnerton-Dyer conjecture and more generally famous conjectures in mathematics such as the millennium problems. One thing about BSD is that in its most general form it assumes other conjectures, as well as assuming theorems which are too hard to prove in Lean

[Yaël Dillies]

Ruben Van de Velde said:

Might also be interesting for this to support proving corollaries of conjectures

Yes, that's one thing I had in mind.

[Yaël Dillies]

My point is mostly to make things look nice and clearly say "Hey, this is a conjecture".

[Eric Wieser]

What's the argument against a separate project for conjectures?

[Yury G. Kudryashov]

You can prove corollaries of conjectures without special syntax:

def conjecture.goldbach : Prop :=
∀ (n : ℕ), 2 ≤ n → ∃ p q : ℕ, p.prime ∧ q.prime ∧ p + q = 2 * n

lemma conjecture.goldbach.c1 (h : conjecture.goldbach) : ... := ...

[Yury G. Kudryashov]

If we put conjectures in namespace conjecture, then #print prefix conjecture will give us a list of all formalized conjectures.

[Adam Topaz]

I think it's important to have strong separation when it comes to conjectures being in mathlib, particularly if the intention is to build results depending on the validity of certain conjectures. The statements of conjectures changes over time, even famous conjectures. E.g. https://core.ac.uk/download/pdf/82815264.pdf (see the footnote on page 1)

[Mario Carneiro]

If conjectures are written as in Yury's or Kyle's post, then I don't think there is any possibility of confusion between conjectures and axioms, because the reader is reminded of the dependence on the conjecture in every theorem

[Adam Topaz]

So what would one do when a counterexample is found for a given conjecture? Delete the 37571 lines in mathlib that depend on it?

[Mario Carneiro]

sure

[Adam Topaz]

Ok fair enough.

[Mario Carneiro]

only after the counterexample is actually formalized though

[Mario Carneiro]

since then the counterexample theorem strictly dominates all 37571 lines

[Mario Carneiro]

some of those lines might actually be part of the counterexample proof though, in which case they aren't junk

[Mario Carneiro]

If it's "false for trivial reasons" like in Grothendieck's paper, then the conjecture can probably just be edited and the proofs modified to accomodate the change

[Mario Carneiro]

since presumably nothing was depending on the error

[Alex J. Best]

Adam Topaz said:

So what would one do when a counterexample is found for a given conjecture? Delete the 37571 lines in mathlib that depend on it?

One can ask the same question about all the lemmas in papers that assume GRH right? Its not so uncommon in some areas

[Alex J. Best]

They're still interesting results that are maybe worthless if GRH turns out to be wrong

[Alex J. Best]

But also maybe salvageable under a weaker assumption. At least many false conjectures aren't just outright wrong, rather true under some extra hypotheses, deletion seems a bit extreme

[Kevin Buzzard]

Especially if the 37571 lines constitute a proof of false from the conjecture and thus the disproof

[Adam Topaz]

I'm convinced. But I still think it's better to, say, name a proposition conjecture.the_Riemann_hypothesis as opposed to having sorrys and/or axioms around in the conjecture namespace.

[Adam Topaz]

I guess it wasn't made clear above how the conjecture idea would be implemented.

[Reid Barton]

This is a reasonable use for type classes

[Yury G. Kudryashov]

I suggest the following:

• We declare facts with no proofs as typeclasses in one of 2 namespaces todo (there is a proof on paper, not yet formalized in mathlib) and conjecture (there is no proof accepted by math community). E.g.,

class todo.fermat_last_theorem (n : nat) : Prop :=
(flt : 3 ≤ n → ∀ a b c : nat, a ≠ 0 → b ≠ 0 → a ^ n + b ^ n ≠ c ^ n)

• For each typeclass, we define a theorem that works as a public interface for this class. E.g.,

theorem pow_add_pow_ne_pow {a b n : nat} [todo.fermat_last_theorem n] (hn : 3 ≤ n) (ha : a ≠ 0) (hb : b ≠ 0) (c : nat) :
  a ^ n + b ^ n ≠ c ^ n :=
todo.fermat_last_theorem.flt hn a b c ha hb

• If we formalize a fact that depends on FLT, then we assume [todo.fermat_last_theorem n] or [∀ n, todo.fermat_last_theorem n] and call pow_add_pow_ne_pow here and there.
• doc-gen highlights assumptions in the conjecture and todo namespaces (e.g., makes them bold red). This rule takes precedence over the current "semi-hidden typeclass assumption".
• If some day the theorem is formalized (it's not a realistic assumption for FLT in the next few years but we can use the same trick for simpler results), then we just drop the typeclass assumption and all proofs still work.

[Filippo A. E. Nuccio]

(deleted)

[Eric Wieser]

Is there a way we can get the bold red highlight without having to teach doc-gen about special namespaces?

[Eric Wieser]

Say for instance: typeclasses with no instances are always shown in red

[Yury G. Kudryashov]

We'll have instance todo.fermat_last_theorem 3

[Yury G. Kudryashov]

We need either a special namespace, or a special attribute.

[Yaël Dillies]

Okay, I really like this idea.

[Yaël Dillies]

This approach only works for conjectures we can state, but I assume this is doomed to be.

[Yury G. Kudryashov]

The main use case I thought about is formalizing some results that depend either on a conjecture, or on a very complicated theorem.

[Alex J. Best]

How would this work with conjectures which are known in some cases but not others

[Alex J. Best]

E.g. for elliptic curves in 1990 it was known that modular elliptic curves had many nice properties and several individual elliptic curves were proven to be modular, then wiles proved flt by showing semistable elliptic curves are modular. Only later were all elliptic curves over the rationals shown to be modular.

I don't really see with this system how you get useful results out of knowing the conjecture in some cases, compared to just stating theorems with regular hypotheses for the conjecture

[Johan Commelin]

@Alex J. Best you can have instances for the known cases. That looks nice to me...

[Alex J. Best]

But you would then need whatever conditions the partial result is known under to also be a class right? If I prove FLT for Mersenne primes I'd have to make is_mersenne_prime a class to fit into this system?
Its nice that one wouldn't have to change any lines sure, but some parts of mathematics just don't feel like typeclasses to me

[Eric Rodriguez]

I don't think that'd be the case; you could just state the signature originally as lemma flt {p : nat} (hp : is_mersenne_prime p) [todo.goldbach_or_some_nonsense p] {a b c : nat} : a ^ p + b ^ p != c ^ p, and when we actually have a proof just remove the todo. (apologies for the ascii art, haven't set up xcompose on this computer yet)

[Johan Commelin]

@Alex J. Best maybe using fact for that would be ok?

[Reid Barton]

or just make the proof of the special case into a def/lemma and then if you ever actually use it somewhere, use letI

[Stuart Presnell]

Did anyone make any progress on this?

[Yury G. Kudryashov]

I didn't.

[Martin Dvořák]

Speaking of conjecture as a keyword, we could also add corollary next to theorem and lemma. But adding conjecture is certainly more important.

[Stuart Presnell]

It would be useful to be able to formalise the statement of a conjecture, leaving it for someone else to provide the proof (since mathlib doesn’t allow sorry). This could also be used in proving that different formulations of a statement are equivalent — for example, the various statements of the Four Colour Theorem in graph theory.

[Yury G. Kudryashov]

AFAIR, the plan was to create typeclasses for conjectures.

[Kyle Miller]

To refine @Yury G. Kudryashov's idea a little, the typeclass could be fully parameterized as if it were the actual theorem statement.

class todo.fermat_last_theorem
  (n : ℕ) (hn : 3 ≤ n) {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (c : ℕ) : Prop :=
(proof : a ^ n + b ^ n ≠ c ^ n)

theorem pow_add_pow_ne_pow {a b n : nat} (hn : 3 ≤ n) (ha : a ≠ 0) (hb : b ≠ 0) (c : nat)
  [todo.fermat_last_theorem n hn ha hb c] : a ^ n + b ^ n ≠ c ^ n :=
todo.fermat_last_theorem.proof hn ha hb

That way you have the ability to fill in very specific special cases.

[Kyle Miller]

Potentially that framework could be automated using an attribute (for Lean 3), maybe something like this:

@[conjecture "pow_add_pow_ne_pow"]
def fermat_last_theorem : Prop :=
∀ (n : ℕ) (hn : 3 ≤ n) {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (c : ℕ),
  a ^ n + b ^ n ≠ c ^ n

In Lean 4, I think it's possible to define a conjecture keyword that would generate the typeclass and the typeclass-dependent theorem statement from something like this:

conjecture pow_add_pow_ne_pow {a b n : ℕ} (hn : 3 ≤ n) (ha : a ≠ 0) (hb : b ≠ 0) (c : ℕ) :
  a ^ n + b ^ n ≠ c ^ n

[Yury G. Kudryashov]

IMHO, typeclasses should only depend on typeclasses. So, I think that this should be

class conjecture.FLT (n : nat) : Prop :=
(flt : 3 ≤ n → ...)

Then you can prove lemmas assuming [FLT n] or [∀ n, FLT n].

[Kyle Miller]

What do you mean by "only depend on typeclasses"?

[Yaël Dillies]

I really want the conjecture keyword, personally.

[Kyle Miller]

Maybe it doesn't make sense having these propositions in the arguments for the class (though I'm not sure it hurts), and this would be fine too:

class todo.fermat_last_theorem (n a b c : ℕ) : Prop :=
(proof : a ≠ 0 → b ≠ 0 → 3 ≤ n → a ^ n + b ^ n ≠ c ^ n)

[Kyle Miller]

The point I was trying to make is that it would be good to have these classes be fully parameterized so that you can prove special cases and add them as instances -- it might be too hard proving it for all a, b, and c for a specific n.

[Kyle Miller]

I think it's fine if these instances can't always be found through typeclass search, which might happen if the conditions require additional proofs or data. Having them be instances lets them show up in the "instances" list in the documentation.

[Yury G. Kudryashov]

Kyle Miller said:

I think it's fine if these instances can't always be found through typeclass search, which might happen if the conditions require additional proofs or data. Having them be instances lets them show up in the "instances" list in the documentation.

I think that we should list non-instance definitions/lemmas in the documentation too.