autogenerate the boring lemmas

Stream: general

[Johan Commelin]

As you all know, I'm a newbie wrt ATP etc. Please let me pick your brains.
Are there good examples/experiments/research papers that deal with autogenerating a bunch of boring lemmas, given some new definition.
Let me put it this way. We teach Lean what a semigroup is, and it generates semigroup.lean. We teach Lean what a monoid is and it generates monoid.lean, and then group.lean and semiring.lean etc...
The system could just go crazy and try to combine the axioms in all sorts of ways, and flood the file with all the trivialities it comes up with. It could score the lemmas by length of the statement, and keep the ones that are shortish. Autogenerating a name must be possible. It gets bonus points if it reuses previously proved lemmas in the proofs.

Of course this is all not very interesting for the files that we already have. But we'll have to write lots of such files in the future. I certainly wouldn't mind if the system would have generated valuation/basic.lean for us.
Note that I'm really speaking of a one-time thing. It generates the file once, not every compile. So speed is not really an issue.
And if we teach it the naming scheme, then the result should be pretty usable. Next step would be to recognize simp-lemmas, etc.

Just some random thoughts. Looking forward to yours.

[Koundinya Vajjha]

May be relevant:
https://en.wikipedia.org/wiki/Automated_Mathematician

[Koundinya Vajjha]

(Although this was quite controversial when it came out.)

[Rob Lewis]

It's a tough problem. You only want to see correct and interesting conjectures, so you need to both sniff out the good stuff and be able to prove it. I know of some work on lemma generation for inductive theorem proving (http://www.cse.chalmers.se/~jomoa/papers/hipspec-atx.pdf). And there's some work on conjecturing guided by machine learning, http://ceur-ws.org/Vol-1785/W23.pdf comes to mind but I'm pretty sure there are others.

[Wojciech Nawrocki]

From what I heard, the hard part is not necessarily generating lemmas, but generating interesting lemmas. Equivalently, pruning the space of true statements to contain only useful laws and not a bazillion variants of rewriting by associativity or some such. Both of these, being human-centric notions, sound difficult to teach a computer, but are potentially a good fit for heuristics and then machine learning.

For benchmarking equality decision procedures, I wrote a short Python script that can generate as many commutative ring equalities as you might want, exercising hopefully many of the axioms (although I had to limit it slightly for some technical reasons I can't remember at the moment). I would hardly call any of these interesting though. Example: (x14+x6) = (0+(x6+(1*x14))). This one only contains two variables, so I would call it shortish, but there already are quite a few of these (exponential explosion etc), potentially making the file huge. So I think one initial step could be to pick out the axioms which generate more interesting statements. In this case, by omitting 0+x=x and 1*x=x.

An interesting alternative is to scrap the lemmas altogether and instead hand-code a proven simplification procedure which can exercise the laws when needed.

[Johan Commelin]

@Wojciech Nawrocki What do you mean with your last sentence?

[Kevin Buzzard]

Johan don't you think that we found out by ourselves, using experience and examples and so on, what lemmas to put in those valuation files, via quite a bit of hard work? Here's the current state of our file: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuation/basic.lean . Stuff about the support of a valuation being a prime ideal, or facts like v(x+y)=max(v(x),v(y)) if v(x) isn't v(y) -- I would imagine a computer program generating thousands and thousands of random facts before they ran into these useful (for us) ones. The support of a valuation is a definition -- the stuff that gets mapped to zero. How can the system come up with definitions? For every good idea there are ten bad ones, don't you think? The notion of equivalence of valuations is a great example of something really important but probably extremely difficult to find if you're just wandering around some search space.

[Johan Commelin]

Aah, let me be clear. I don't expect it to generate the definitions

[Wojciech Nawrocki]

@Johan Commelin This is just a wild guess, but a sufficiently sophisticated tactic could potentially use the current goal and context in a sort of guided search. The lemmas would be generated on-the-fly as intermediate steps in order to simplify or otherwise "make-nicer" (heuristic) the goal. It seems defining interesting might be easier in the context of a sensible (human-provided) target. Since generated statements wouldn't have to be stored on disk, this partly alleviates the exponential explosion issue when they are very specific/long. But then again, maybe such a tactic is just "by general_intelligence".

[Johan Commelin]

Put all the 10 or so definitions in that file all the way at the top. And have the computer generate all the boring lemmas.

[Johan Commelin]

It might miss some of them. But it could still provide a good start...

[Kevin Buzzard]

We've seen examples where the definitions can't be formalised until you've proved a whole bunch of the lemmas though ;-)

[Kevin Buzzard]

There is some subtle interplay

[Johan Commelin]

Sure... the definitions that can't be formalised unless you have a bunch of lemmas first should then move to a new file...

[Gabriel Ebner]

It's a tough problem. You only want to see correct and interesting conjectures, so you need to both sniff out the good stuff and be able to prove it. I know of some work on lemma generation for inductive theorem proving (http://www.cse.chalmers.se/~jomoa/papers/hipspec-atx.pdf).

Moa and her group did a lot of work in this area, hipspec is just the application of the general framework to inductive theorem proving. The theory exploration tool itself is called hipster (https://arxiv.org/abs/1405.3426). They even have a working Isabelle integration where you can say "give me theorems [just equations] about list.append, list.reverse, and list.nil" and then after a few minutes you get a working Isabelle file: https://github.com/moajohansson/IsaHipster

[Johan Commelin]

Cool! That looks really interesting.

[Edward Ayers]

There is a tool called Mathsaid that has some interesting heuristics for picking out interesting lemmas: https://link.springer.com/article/10.1007/s10489-017-0954-8

[Johan Commelin]

One thing that Hipster does could be summarised as "playing around with examples". I think that is something that human mathematicians do a lot. But currently there is no way to register such information in Lean.
We could have something like

register_example nat 0
register_example nat 1
register_example nat 37

register_example int -1

register_example rat 2/3

register_example real real.pi

register_example (∏ (G : Type), group G) \<int, infer_instance\>
register_example (∏ (G : Type), group G) \<zmod 6, infer_instance\>

register_example (∏ (X : Type), topological_space X) \<real, infer_instance\>

[Johan Commelin]

I think such a database could potentially be really useful for tactics that try to prove or find counterexamples. And as Hipster shows, it's also useful for generating conjectures/boring lemmas.

[Johan Commelin]

(Hipster generates the examples on the fly. But I think that will quickly break down if you are not working with lists/trees or other CS-y data types.)

[Alex J. Best]

Yeah I like the sound of this a lot, I've started using @Simon Hudon's slim_check and even if it has issues its really very handy to tell you when you've forgotten a trivial case in a statement, or accidentally got your tactic state into an unprovable situation. But like Johan says handmade examples would be needed for non-trivial structures (how does it handle groups I wonder). It would be great to include these or equivalent tactics!

[Simon Hudon]

Nice! I’m glad you can make use of it. I haven’t touched it in a while and feel like I left it in an incomplete state. What are the issues you encounter?

[Simon Hudon]

Maybe I should merge it into mathlib