Zulip Chat Archive

Stream: general

Topic: conjecture declaration


Yaël Dillies (Dec 12 2021 at 20:34):

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 (Dec 12 2021 at 20:39):

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

Ruben Van de Velde (Dec 12 2021 at 21:05):

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

Kyle Miller (Dec 12 2021 at 21:17):

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 (Dec 12 2021 at 21:21):

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 (Dec 12 2021 at 21:26):

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

Kevin Buzzard (Dec 12 2021 at 21:27):

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 (Dec 12 2021 at 21:47):

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 (Dec 12 2021 at 21:52):

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

Eric Wieser (Dec 12 2021 at 21:58):

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

Yury G. Kudryashov (Dec 12 2021 at 22:55):

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 (Dec 12 2021 at 22:56):

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

Adam Topaz (Dec 12 2021 at 23:03):

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 (Dec 12 2021 at 23:08):

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 (Dec 12 2021 at 23:10):

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 (Dec 12 2021 at 23:10):

sure

Adam Topaz (Dec 12 2021 at 23:10):

Ok fair enough.

Mario Carneiro (Dec 12 2021 at 23:10):

only after the counterexample is actually formalized though

Mario Carneiro (Dec 12 2021 at 23:11):

since then the counterexample theorem strictly dominates all 37571 lines

Mario Carneiro (Dec 12 2021 at 23:11):

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

Mario Carneiro (Dec 12 2021 at 23:12):

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 (Dec 12 2021 at 23:13):

since presumably nothing was depending on the error

Alex J. Best (Dec 12 2021 at 23:24):

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 (Dec 12 2021 at 23:24):

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

Alex J. Best (Dec 12 2021 at 23:25):

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 (Dec 13 2021 at 02:19):

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

Adam Topaz (Dec 13 2021 at 02:30):

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 (Dec 13 2021 at 02:31):

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

Reid Barton (Dec 13 2021 at 03:57):

This is a reasonable use for type classes

Yury G. Kudryashov (Dec 16 2021 at 18:26):

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 (Dec 16 2021 at 18:39):

(deleted)

Eric Wieser (Dec 16 2021 at 18:49):

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

Eric Wieser (Dec 16 2021 at 18:49):

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

Yury G. Kudryashov (Dec 16 2021 at 19:10):

We'll have instance todo.fermat_last_theorem 3

Yury G. Kudryashov (Dec 16 2021 at 19:10):

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

Yaël Dillies (Dec 16 2021 at 21:44):

Okay, I really like this idea.

Yaël Dillies (Dec 16 2021 at 21:45):

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

Yury G. Kudryashov (Dec 16 2021 at 22:03):

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 (Dec 16 2021 at 23:42):

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

Alex J. Best (Dec 16 2021 at 23:45):

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 (Dec 17 2021 at 03:55):

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

Alex J. Best (Dec 17 2021 at 04:01):

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 (Dec 17 2021 at 04:21):

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 (Dec 17 2021 at 04:33):

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

Reid Barton (Dec 17 2021 at 04:56):

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 (May 15 2022 at 16:18):

Did anyone make any progress on this?

Yury G. Kudryashov (May 15 2022 at 17:55):

I didn't.

Martin Dvořák (May 16 2022 at 17:39):

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 (May 16 2022 at 18:10):

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 (May 16 2022 at 18:29):

AFAIR, the plan was to create typeclasses for conjectures.

Kyle Miller (May 16 2022 at 19:52):

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 (May 16 2022 at 19:56):

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 (May 16 2022 at 20:00):

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 (May 16 2022 at 20:01):

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

Yaël Dillies (May 16 2022 at 20:03):

I really want the conjecture keyword, personally.

Kyle Miller (May 16 2022 at 20:04):

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 (May 16 2022 at 20:05):

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 (May 16 2022 at 20:07):

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 (May 16 2022 at 20:39):

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.


Last updated: Dec 20 2023 at 11:08 UTC