What are Lean's biggest issues?

Stream: general

[Jannis Limperg]

When I'm done with my current project (if it ever gets done...), I'll have the rest of my PhD to do more or less anything that makes Lean, and interactive theorem proving in general, better. So, since I have a lot of people using Lean in anger here: what are the issues standing in the way of Lean world domination?

[Scott Morrison]

If not for COVID, we could all go have a beer in a moment and plot.

[Anne Baanen]

Fixing these instance diamonds would be really nice:

import ring_theory.ideals

example {R : Type*} [comm_ring R] {I : ideal R} (hI : I.is_maximal) {x : I.quotient} (hx : x ≠ 0) : is_unit x := begin
  haveI : field I.quotient := ideal.quotient.field I,
  convert is_unit_iff_ne_zero.mpr _,
  -- integral_domain.to_domain I.quotient = division_ring.to_domain
  swap,
  convert hx,
  -- group_with_zero.to_monoid_with_zero I.quotient = semiring.to_monoid_with_zero I.quotient
end

[Anne Baanen]

There was a paper at IJCAR about this

[Johan Commelin]

Bah, those look painful )-;

[Anne Baanen]

Ah never mind the specific case, it turns out I should have used letI instead of haveI. :upside_down:

[Johan Commelin]

ooh, good catch

[Jeremy Avigad]

I think better general automation, like a really good sledgehammer, would put us halfway to world domination. We have lots of tricks to mitigate the tedium of searching for things in the library, but it is still tedious, and a distraction from the mathematics. I know Lean 3 is not the right place to do it and Lean 4 isn't quite ready, but I'd be excited to see anything that moves in that direction, like preliminary experiments with Lean 4 or better data on what the pain points are in Lean 3. (But the challenge then is to make that into a sensible dissertation project.)

Scott's talk on the first day of the conference, where library_search and suggest worked so well, was really compelling. If formalization was always so nice, we'd have lots more users.

[Scott Morrison]

• more people --- it's clear that the frontier of mathlib is large relative to the people working on it (and, just as importantly, I think at the moment we have capacity to bring more people up to mathlib-speed)
• better automation --- we really want mjolnir :hammer: and friends
• surviving the transition to Lean4 --- it's going to be great, but getting mathlib across will be epic

[Scott Morrison]

(Sounds like I agree with Jeremy!)

[Scott Morrison]

(Regarding my talk on the first day, earlier iterations of this talk had cheated and used a prototype back (short for "backwards reasoning") tactic that I've been working on on and off forever. It's never been good enough for use in the wild, but I think it could be. The general strategy is just to do a tree search applying lemmas from the library against the active goal, but working more generally than either solve_by_elim (which just does depth first, on a specified set of lemmas) or library_search, which does a single step from the entire library, followed by solve_by_elim with local hypotheses. For back, I maintain a priority queue of different branches of the search, and try to get the priority function right. Heuristics like "anytime you get to use a local hypothesis is good" and "more subgoals is worse than less" and "goals that depend on other goals via metavariables are bad" get you some of the way. Idiotic heuristics like "use lemmas with short names instead of long names" are surprisingly helpful.)

[Jannis Limperg]

back sounds very similar to auto, which is Coq's main workhorse. Afaik they even use some of the same heuristics.

[Scott Morrison]

Yes. We really should just port auto. As far as I know there's no real obstacle to following what they do.

[Scott Morrison]

I have been reinventing the wheel for no defendable reason whatsoever. :-)

[Jeremy Avigad]

I originally wrote finish with auto in mind, but I relied on some not-very-widely-used SMT-like gadgets that Leo has implemented in C++ to find useful instantiations for quantifiers. They didn't do exactly what I wanted, and at that point I was stuck: I didn't have the energy or expertise to write my own C++ versions, and they would have been too slow in metaprogramming. But now that leanprover-community has Lean 3, that's a reasonable option.

[Jeremy Avigad]

Jasmin has seen my exploration of what sort of automation would be helpful:
http://www.andrew.cmu.edu/user/avigad/Talks/london.pdf
https://github.com/avigad/arwm
The last 10 slides of the talk are my take-home message.

[Jannis Limperg]

Thank you Jeremy, those slides were very interesting. I'll look more into possible topics in automation. It seems clear to me that abstracting from tedious details is extremely important for any sort of mainstream adoption, but I don't yet have any good idea of how to advance that goal.

Actually, let me run an idea by you all. It's like half an hour old, so no details, but the gist is to make automation interactive. Currently, all these search procedures are essentially black boxes: you call them and they either succeed or fail; if they fail you have to figure out, usually without any help, what lemmas or proof steps were missing. There are also often performance concerns where the heuristic picks the wrong branch of a search tree and ends up wasting an eternity on an unprovable goal. These concerns, and maybe more, could be alleviated by just asking the user:

• "I've spent N ms on this goal without being able to solve it. Do you think it should be provable?"
• "I could apply this lemma to solve the goal if this precondition was true, but I can't prove it. Is it true?"
• "Applying this technique is risky because it may blow up the search space. Would you like me to try anyway?"
• "I could make progress by breaking through some abstraction barrier. Is that a good idea?"
• "There are different possible solutions for this typeclass instance. Which one should I choose?"

Obviously, there are a lot of technical questions here, but does this sound like something worth trying?

[Johan Commelin]

@Jannis Limperg Yes, this sounds like exactly the kind of thing that I would love to use.

[Jeremy Avigad]

I agree. One of the things I like about Isabelle's auto is that you can use it sort-of interactively. You try it, look at the mess it leaves, and then say, "oh, it just needs this simp lemma" or "it just needs this fact." That doesn't always work: sometimes, it does some unpacking and then doesn't know how to instantiate some quantifier, and then there is no way to specify that from the start. ("When you get to the part when you have introduced an arbitrary epsilon and want to use the continuity hypothesis, use epsilon / 2.") It would be great to find ways of conveying that information. Typically the user has a general idea why the inference is true, and will be happy to provide additional guidance.

By the way, my understanding is that stuff like this is one of the motivations for turning syntax into first-class objects in Lean 4. Imagine what we could do if the simplifier returned a trace as a structured object that a tactic could traverse. You could use a GUI to navigate the tree and figure out where it is going wrong, and then add an annotation to steer it in the right direction.

Another thought: it is generally easier for users (especially mathematicians) to give terms and statements rather than theorem names. We want to say "at some point, use p > 0" rather than "at some point, use nat.prime_pos." We want to think about the mathematically relevant stuff, not the names of theorems or the way they are expressed in the library.

[Simon Hudon]

@Jeremy Avigad Making syntax a first class citizen will not improve the interaction between tactics, I believe because they already have the option of exchanging bits of syntax. Case in point, I wrote squeeze_simp, then @Scott Morrison modified it so that tidy could access the results and now tidy can return a piece of advice that contains an explicit list of simp lemmas.

What I think will change is the style of interaction with the user. When complicated types don't quite match in subtle ways, having the syntax tree allows emacs / VS code to do a structural comparison and bring the user's attention to what is actually relevant to them.

[Jeremy Avigad]

Thanks! I stand corrected.

[Kevin Kappelmann]

Jeremy Avigad said:

... That doesn't always work: sometimes, it does some unpacking and then doesn't know how to instantiate some quantifier, and then there is no way to specify that from the start. ("When you get to the part when you have introduced an arbitrary epsilon and want to use the continuity hypothesis, use epsilon / 2.") It would be great to find ways of conveying that information. Typically the user has a general idea why the inference is true, and will be happy to provide additional guidance.

Another thought: it is generally easier for users (especially mathematicians) to give terms and statements rather than theorem names. We want to say "at some point, use p > 0" rather than "at some point, use nat.prime_pos." We want to think about the mathematically relevant stuff, not the names of theorems or the way they are expressed in the library.

auto2 supports some (or all?) of these ideas. I am no expert, but I am about to integrate it in a project of mine, so I could tell you more about how it works out in practice hopefully soon.

There was also some work on a proof planner in Isabelle: IsaPlanner. But it seems quite dead.

[Jeremy Avigad]

I am a big fan of Bohua Zhan. Yes, please do let me know what you think of auto2.

[Sebastian Ullrich]

Simon Hudon said:

Jeremy Avigad Making syntax a first class citizen will not improve the interaction between tactics, I believe because they already have the option of exchanging bits of syntax. Case in point, I wrote squeeze_simp, then Scott Morrison modified it so that tidy could access the results and now tidy can return a piece of advice that contains an explicit list of simp lemmas.

But you still have to copy and insert the suggestion manually, don't you? I know there is a hole command, but then you still have to insert the hole first. When you can generate and manipulate actual syntax trees and not just strings, automatically rewriting the tactic proof itself becomes absolutely possible.

I don't think you need Syntax for improving unification error messages; the terms are produced from the pretty printer anyway, which can annotate the output in any way it wants. Is that not exactly what @Edward Ayers is doing, just not with pairs of terms (yet)?

[Edward Ayers]

But you still have to copy and insert the suggestion manually, don't you?

It should now be possible to use widgets to insert the suggestion if you click a button made by a widget made by squeeze simp.

[Edward Ayers]

The new pretty printer tagging thing effectively gives lean pretty printed strings source maps. So I think you would need a bit more work to get it to output structured data for other procedures like simplification, particularly the C++ implemented ones.

[Oliver Nash]

Speaking of the pretty printer, one issue I’d love to see resolved would be to have the pretty printer round trip.

[Johan Commelin]

Edward Ayers said:

But you still have to copy and insert the suggestion manually, don't you?

It should now be possible to use widgets to insert the suggestion if you click a button made by a widget made by squeeze simp.

Or press Alt - V

[Scott Morrison]

Simon Hudon said:

Case in point, I wrote squeeze_simp, then Scott Morrison modified it so that tidy could access the results and now tidy can return a piece of advice that contains an explicit list of simp lemmas.

I don't think we actually did this! We definitely talked about it, but at least the tidy end doesn't do this yet.

[Jasmin Blanchette]

Bohua got extremely far using auto2 in his own formalizations. I was curious to see the workflow and asked him, in Cambridge, to prove an easy lemma live, so I could see it. Unfortunately, it didn't convince me, quite the opposite. Maybe I picked the wrong lemma.

There was no information or guidance on failure, a bit like Sledgehammer, and when you use it it's the only tactic available (it comes with its own Isar-like structured proof language but more implicit and where every goal is proved by auto2). Many of the ideas are good, but I'm not sure about the lack of labels (even pen-and-paper proofs track dependencies more closely than auto2), and the impossibility to plug in your own tactic in the middle is bound to put off people who know a few tactics and want to use them.

[Kevin Kappelmann]

Those are good points Jasmin, thanks for pointing them out. I will take notes about them when experimenting with auto2

[Simon Cruanes]

Could also be because it's his own tooling so he didn't bother too much with debuggability. The question is whether these problems would still be there with a few additional person-years of work :slight_smile:

[Jasmin Blanchette]

There was also some work on a proof planner in Isabelle: IsaPlanner. But it seems quite dead.

Not only it's quite dead, it was never alive. I'm not aware of any users, and its user manual's most impressive example automated a proof that could have been achieved with the one-liner by (induct x) auto, I seem to recall.

[Jasmin Blanchette]

Answering to Simon C.: Some of it is tooling for sure, some of it is design choices I would question, but I agree all of this is fixable, and there's probably a lot to learn from auto2.

[Jasmin Blanchette]

In principle, auto2 the tactic (as opposed to the structured proof language built on top of it) is very similar to Lean's smt mode: it propagates equalities a bit like cc, heuristically instantiated quantifiers, etc. But it seems to work much better, at least for Bohua. I really wonder why.