using Lean/mathlib for *doing* mathematics

Stream: general

[Alex Kontorovich]

Continuing from an earlier discussion, how do we actually get to the point where we can do exploratory research within Lean itself? I often have a situation that would look something like:

lemma DeligneBound (assumptions) :
exponentialSum << ?_ := by sorry

That is, I don’t know yet what bound I’ll get, but I know the rough shape of the lemma. Is there a reasonable way to use Lean for this mode of discovery? How could we get it to generate two goals, the first an unknown value for the RHS, and the second, a proof that the bound holds? (This is, by the way, how I often teach. I don’t state theorems; I state the beginnings of theorems and leave blanks to fill in once we know the outcome of the proof…) One could of course choose to put exponentialSum on the RHS and be trivially done, but the point isn’t to just close a goal, but to put something nontrivial there; so there’s a lot of flexibility…

[Siddhartha Gadgil]

One thing to be done in the above would be to use an exists statement. Often one knows that the bound should be in terms of some stuff only and the existence may be as a function of these.

[Siddhartha Gadgil]

But I do feel that the present workflow can easily be extended for mathematics in progress. For example, have a command conjecture where

conjecture riemann_hypothesis : ...

introduces the definition riemann_hypothesis.prop (not riemann_hypothesis as that should be a proof). Similarly, have a command

assume riemann_hypothesis

which translates to variable _ : riemann_hypothesis.prop for when one wants to work assuming the Riemann hypothesis.

[Siddhartha Gadgil]

It may be better to have typeclasses and scoped instances instead of types and variables. Things have to be designed well. But implementing something like this should not be hard.

[Siddhartha Gadgil]

I mean typeclasses especially where we are not speaking of a single statement but a property that conjecturally holds for all primes say. Then this holding for a class of primes will be an instance.

[Alex Kontorovich]

Indeed, I looked back at how Gomes and I formalized RH (not in mathlib; see: https://github.com/bhgomes/lean-riemann-hypothesis) many years ago, and it's a definition...

[Alex Kontorovich]

But ok, that's still a standard process in Lean; if I know what the conjecture is, I can state it as a def of type Prop; and then the theorem simply assumes that this Prop is true. What if I don't know a priori what the conjecture is - can I still work with it somehow?

[Johan Commelin]

I agree that we should explore these kind of workflows. And I don't think there is one obviously correct design. There's a lot of room for experimenting here.
A very low brow approach could start with

def DeligneBound (assumptions) :
    { bound // exponentialSum <= bound } :=
  constructor; sorry -- look two goals

While it works, it isn't exactly the UX and workflow that you are looking for.

[Yaël Dillies]

That's happening to me right now in LeanAPAP: The way @Thomas Bloom originally stated this lemma was wrong (he accidentally used two different notions of dissociation), so now I have a lemma with a constant I don't know, but I trust Thomas that it's true with some constant. Hence I've posited the existence of thomas_const and sorried the lemma until Thomas comes back to me with a fixed proof. Once I have the fixed proof, I will enter that exploratory mode you're looking for, where I have a guess for the value of thomas_const, but also a hunch that it's wrong, since it's a fiddly proof that a professional combinatoricist already got wrong once.

[Kevin Buzzard]

My instinct with Alex' question is that it's a very natural one but historically it's not the way theorem provers have been used and hence it's not well-understood yet. Right now I think you just say "exists B, Sum < B" and then you see what happens. This is what we did in LTE -- Scholze raised the question that various constants in the technical low-level lemma 9.4 were ineffective in the paper and asked if a formalisation could make them effective -- turned out it could.

[Rick de Wolf]

Speaking as a non-mathematician and Lean beginner, isn't the expected workflow to work out a sketch of a proof on paper first, and then go into Lean to formalize? (For now, at least) If you want to bring Lean in at a point where you're unsure what your final theorem will be, it may be interesting to give Lean some functionality that gives you promising options to explore?

[Mario Carneiro]

that depends on your comfort level with the proof assistant

[Mario Carneiro]

Generally speaking, yes you probably want to go in with a plan, if you know that the formalization will be the hard part

[Rick de Wolf]

I've been meaning to look into e graphs for this purpose. If I correctly understood the documentation of the e-graph implementation in Julia, it should be possible to find interesting expressions, where 'interesting' can be defined by some scoring function. It's not my wheel house for sure, but that seems like an interesting angle.

[Mario Carneiro]

But if you get good at the language and the library, you can get to the point where you can just sort of use it like a sketchpad and prove facts in a somewhat aimless fashion

[Rick de Wolf]

Mario Carneiro said:

that depends on your comfort level with the proof assistant

Definitely, and I agree that people will probably get more comfortable with it over time. Especially as more and more people get introduced to it early on in university.

[Mario Carneiro]

My answer to @Alex Kontorovich 's question would be to use a sorry'd definition for the bound and just delay unfolding it as long as possible (possibly creating sorry subproof goals when I find a required constraint). This usually works a bit better than an existential metavariable if this thing is going to stick around over many proofs

[Mario Carneiro]

and then hopefully once all the constraints are collected the solution is obvious, you can fill in the bound, prove the constraints, and then maybe cleanup by inlining stuff

[Matthew Pocock]

Siddhartha Gadgil said:

For example, have a command conjecture where

conjecture riemann_hypothesis : ...

I like this idea. It seems to me that it's useful to have a clear semantic distinction between the theorems you've been able to demonstrate, axioms that you assert, and conjectures that you are proposing. It would also open up a proof writing style where you set out at the beginning what you are working towards as conjectures, then provide the guts as theorems, and close with how that guts satisfies those conjectures.

[Siddhartha Gadgil]

Both for use in real mathematics, and for use in AI, I feel that what needs to get stronger is mechanisms to find counterexamples (maybe even integrating with SAT solvers etc). One big value a smart sketchpad can have is to tell a mathematician not to waste time proving something that is false.

[Adam Topaz]

We do have slim_check (I assume it’s ported to Lean4?) which does this as a tactic. Others have talked about automatically running certain tactics like exact? at all time, so they can fry eggs on their cpu. This could be another candidate.

[Siddhartha Gadgil]

I did mean in part refining slimcheck and adding power to it by many more instances of random stuff.

[Adam Topaz]

I think doing this would be quite cool actually. And I’m ready to sacrifice my cpu.

[Siddhartha Gadgil]

I have been trying running and my CPU has not been stressed so far:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Aesop.20etc.20in.20the.20background/near/378792005

Generally things like exact? or aesop? may not work so well for disproving as typically we need to instantiate with good candidates for disproving. This is fundamentally no harder than other tactics/automation in Lean. It is just that the cognitive focus has been on formalizing stuff with known proofs, so this side is far less developed.