terminology of conjecture/proof

Stream: Equational

[Floris van Doorn]

Minor terminology suggestion: I recommend to change the terminology of "conjecture"/"proof" by "proof"/"formalization". So e.g. on day 22 there are 362 implications without formalization and 132 implications without proof.

If someone writes a proof on Zulip or an ATP finds and checks a countermodel, I would say that the anti-implication is proven, just not formalized. And most of us do actually have a conjecture about the remaining 132 unproven(unconjectured) implications.

[Terence Tao]

I view "conjecture"/"proof" in this context as "formal conjecture"/"formal proof" rather than "informal conjecture"/"informal proof". So, a statement which we have proven informally, but can only mark in Lean as a conjecture rather than a theorem, would be a "formal conjecture" even if it has an "informal proof".

I can also imagine that theoretically we might in future create some formal conjectures that we can only obtain by techniques less rigorous than "informal proof", for instance by applying some probabilistic heuristic that we strongly believe (but cannot prove) to be accurate. (Though for this current project there are so few outstanding implications without conjectures remaining that I doubt we would do so.)

It's also true that using the standard of "informal conjecture" we could simply mark all outstanding implications as conjectured to be false, but this gives us no useful guidance on which implications to focus on next.

[Jared green]

so how do you distinguish between a counterexample found by vampire waiting to be placed in lean from a completely informal proof, or a guess?

[Terence Tao]

The category of "conjecture"s is meant to be a temporary category, since hopefully all implications will eventually be proven or disproven in Lean; it's main purpose (besides the psychological morale boost of having a smaller number of completely unresolved implications) is to allow us to focus our efforts, either on formalizing the implications that are classified as conjectures, or to find new techniques to turn completely open (anti-)implications into conjectures, as a first step towards formalizing them in Lean.

Because of this, a "guess" with no actionable path towards converting the guess into a Lean formalization would probably not qualify for the label of "conjecture" for practical purposes, though of course nothing strictly prevents us from doing so. However, a Vampire proof or a completely informal proof both offer such an actionable path, and so could usefully be placed in the "conjecture" category. (Because of this, I think I retract my previous claim that a plausible probabilistic heuristic argument would be sufficient to qualify for the "conjecture" label, since such a heuristic would likely also not offer a plausible path to formalization.)

[Terence Tao]

I think the particular usage of the "conjecture" category that we landed on is also a consequence of our widespread belief that pretty much all outstanding implications are in fact false. (This was not quite the case though when the category was first introduced about two weeks ago, and we initially used the proof_wanted keyword instead of the conjecture keyword.) If the situation was different in that the split between true and false implications was suspected to be 50/50, then using "conjecture" in the more traditional sense of identifying what we believe to be true even in the absence of actionable ways to obtain a proof could be useful to the project, in cutting down the number of statements we would try to prove by about 50% (since presumably we would not look for counterexamples if we believe the implication to be true, or vice versa). In that case it might even make sense to have three categories "conjectured", "informally proven", and "formally proven", but this is currently unnecessary as we have simply repurposed "conjectured" to mean "informally proven / proven by a non-Lean calculation".

[Mario Carneiro]

I tend to agree with Floris here, this usage of "conjecture" is slightly confusing because it misrepresents the level of understanding we have in the claim (and also unfairly maligns unformalized proofs in general). What you describe as "a 'guess' with no actionable path towards converting the guess into a Lean formalization" is exactly what I would call a "conjecture", e.g. the Birch–Swinnerton-Dyer conjecture, and I think most onlookers will have a similar association for the word. A proof sketch is not a conjecture, but a probabilistic heuristic could be.

[Terence Tao]

For reference, here is the discussion from two weeks ago when we landed semi-randomly on the conjecture keyword for implications lacking a formalized proof: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Lean.20script.20for.20extracting.20current.20set.20of.20implications/near/473366542
The choices at the time were between conjecture, claim, and proof_wanted'.

I'd say all of our subsequent use of the word "conjecture" flows from this Lean keyword conjecture. I guess I can open a poll to see if there are strong feelings about changing it.

[Terence Tao]

/poll What should we do with the conjecture keyword?
Keep it as is
Change to proof_wanted' or similar
Change to informal_theorem or similar

[Mario Carneiro]

Isn't this the role of the blueprint in similar formalization projects? If you want to represent informal proofs in lean, one thing which I think is important is a link to the proof and any other information relevant for a formalizer to use

[Mario Carneiro]

Another possible representation is as a regular proof with a sorry in it (and comments with the informal proof or a link to it)

[Daniel Weber]

Mario Carneiro said:

Another possible representation is as a regular proof with a sorry in it (and comments with the informal proof or a link to it)

This seems nice because it lets you prove theorems up to some different conjecture, and @[equational_result] has a check to prevent it from accidentally being marked as a theorem

[Terence Tao]

I think one thing we've discovered is that the blueprint works differently for a project like this (in which we want to (formally) prove a very large number of small new theorems) than in a more "traditional" formalization project (in which we want to formalize a single existing theorem (or cluster of such theorems), broken up into many pieces). Obviously there is no way we would place all 22 million implications in the blueprint. But even the human-generated portion is mostly present in the blueprint in the form of representative examples, and often contributors are formalizing directly from the relevant Zulip thread informal discussion than via the intermediate step of writing up a blueprint proof.

Currently we are simply entering in conjecture statements arising from informal proofs in Zulip chats in [Conjectures.lean](https://github.com/teorth/equational_theories/blob/main/equational_theories/Conjectures.lean) with a Lean comment giving a URL back to the relevant Zulip discussion; the intermediate blueprint seems to be unnecessary (one reason for this being that the individual proofs are somewhat decoupled from each other, so the blueprint dependency graph setup is not all that helpful here). Perhaps there is a more systematic way to do this, but at this point we only have 65 implications to go (modulo duality) and I think _ad hoc_ procedures that evolve as we go will be sufficient.