The pieces of proofs

Stream: new members

[Lucas Allen]

Hello, I'd like to be able to reduce proofs in Lean to SAT. In order to do this I want to understand what the pieces of proofs are and how they fit together.

So far what I have is that given a L : list name of lemma names which we can use in a proof, we can get a list expr of corresponding exprs with types which look like Π (a₁:α₁) ... (aₙ:αₙ), P(a₁,...,aₙ). From here we can use open_pis and open_pis_metas from tactic/binder_matching.lean to get a pair ([?m_1,...,?m_n], e) where the ?m_k are metavariables corresponding to the Π binders and e is the remaining expr.

For each metavariable in [?m_1,...,?m_n] which is of type Prop we can do a similar thing as above to get ([h_1,...,h_n], ?m_k'). And for each of the h_i which are of type Prop we need to do the whole thing again, i.e. we need to treat it as if it's another lemma we can use, but with the caveat the we can only use this lemma in the scope of the metavariable from where it came.

If we index each lemma with a ℕ and each metavariable of a lemma with another ℕ, then we can construct a function D : ℕ → ℕ → list ℕ which takes the index of a lemma i and the index of one of its metavariables j and returns the list of indices of lemmas k such that the remaining expr e of lemma k unifies with the expr ?m_j of lemma i.

Then a proof would be like a function P : ℕ → ℕ → ℕ where we apply lemma P(i,j) at the jth goal after applying lemma i, in such a way that there are no stray metavariables at the end. I'm hoping we can ignore all the non-propositional goals because Lean fills them in itself. We also need someway of keeping track of which lemmas are in scope, i.e. when we can use lemma P(i,j). And which lemmas can be applied to the original goal.

Is this correct so far? And if so, could all proofs using only the lemmas in L be found this way? Or am I missing something?

[Kevin Lacker]

what exactly are you trying to do - are you trying to fill in lean proofs using a sat solver? that seems pretty neat, I had had the impression it was intractable, but I would love to be wrong

[Kevin Buzzard]

Isn't this exactly what a hammer tries to do? I think Gabriel had one working in a hacked Lean 3 but it was a highly nontrivial endeavour.

[Kevin Lacker]

sounds pretty neat. which gabriel - ebner? (looking at the user list.)

[Kevin Buzzard]

He spoke about it at the Pittsburgh meeting in Jan, it'll be on YT somewhere

[Patrick Massot]

I think we have only one Gabriel, those people are not Kevins.

[Kevin Buzzard]

Or Patricks!

[Heather Macbeth]

https://www.nytimes.com/2015/03/03/upshot/fewer-women-run-big-companies-than-men-named-john.html

[Kevin Buzzard]

I saw this article a while ago and it made me sad :-(

[Heather Macbeth]

But we have very few Johns!

[Rob Lewis]

@Heather Macbeth Oh! I just realized, my nemesis H. is in your department, isn't he?

[Heather Macbeth]

Funny, I never made the connection! He retired just before I arrived so I don't really know him.

[Heather Macbeth]

Did you ever meet him (or pass on a misdirected email)?

[Rob Lewis]

We met at a conference a few years ago, it was just as confusing as you'd think.

[Rob Lewis]

I saw Robert Lewis was scheduled to give a talk about something, like, a step away from things I had been thinking about recently. And I got scared I had submitted an abstract in my sleep or something

[Heather Macbeth]

@Scott Morrison has perhaps the worst case of this problem.

[Yury G. Kudryashov]

http://phdcomics.com/comics/archive.php?comicid=1890

[Lucas Allen]

Kevin Lacker said:

what exactly are you trying to do - are you trying to fill in lean proofs using a sat solver? that seems pretty neat, I had had the impression it was intractable, but I would love to be wrong

Yeah, the dream is to give some tactic a number n and and have it reduce the problem of finding a proof which uses n or less applies to SAT. I think it's theoretically possible by Cook's theorem. I wanted to make sure what I have is correct before devoting more brain energy to the rest of the problem, but I don't think it's a Zulip friendly question.

[Lucas Allen]

Kevin Buzzard said:

He spoke about it at the Pittsburgh meeting in Jan, it'll be on YT somewhere

Is this the one?
Gabriel Ebner: Integration of General-Purpose Automated Theorem Provers in Lean
https://www.youtube.com/watch?v=WydyJJYKyTs

[Kevin Lacker]

I think the TLDR on this sort of approach is, it's possible, people generally use automated theorem provers (ATPs) rather than SAT solvers, it's kind of one layer of abstraction closer

[Kevin Lacker]

it's more common in e.g. Isabelle with "sledgehammer", see https://people.mpi-inf.mpg.de/~jblanche/iwil2010-sledgehammer.pdf for example. In Lean we don't have an approach like this working right now, basically IIUC the mechanisms for communicating with external processes in Lean 3 are too janky and hopefully Lean 4 is better there

[Lucas Allen]

Cool, Thanks. I'll check out the link. How good is sledgehammer in Isabelle? Is it used a lot? And is it quick more or less?

[Kevin Lacker]

I don't know, I have only read papers about it, not used it directly

[Mario Carneiro]

It is used quite a lot by some authors. @Jasmin Blanchette is probably best able to speak on the topic since he is one of the authors of sledgehammer and also uses it in his proofs IIRC

[Mario Carneiro]

"quick more or less" means 5-30 seconds

[Mario Carneiro]

We often use tidy in the same way an isabelle user uses sledgehammer. It's good when you don't really want to think about the goal and value the computer's time less than your own

[Kevin Lacker]

I pretty much always value the computer's time less than my own

[Mario Carneiro]

in that case you will like sledgehammer

[Mario Carneiro]

a "prove my theorem for me" button is very attractive

[Kevin Lacker]

maybe if it's fast enough and integrated nicely with VSCode, there won't even have to be a button ;-)

[Mario Carneiro]

it's not

[Mario Carneiro]

however you might conceivably be able to set it up to run asynchronously in the background

[Kevin Lacker]

if there were a sledgehammer-like tool for lean, i would investigate getting async stuff to work, but it seems like gabriel's work is pending on lean 4. it might even make sense to do the heavy lifting on a server - latency of a server might be ok given the time scale is not so fast

[Mario Carneiro]

It's not really worth it to send to a server, that's extra latency for little gain, unless you have a really bad computer

[Mario Carneiro]

the standard framework for hammers already involves translating things out of the lean process, and as gabriel mentioned that's the bottleneck

[Julian Berman]

I'd assume you run that "out of band", is the idea?

[Julian Berman]

No need to synchronously wait for your sledgehammer to hit, just put some problems somewhere and let a server spend some time finding the right proof term and come back later and fill them in

[Mario Carneiro]

sure, but that's already happening with the usual model

[Kevin Lacker]

to me the value of the server is more like ease of installation. like if you have some c++ or rust binary, and theres a bunch of people using lean, but they dont have a consistent environment for compiling c++ themselves, or they aren't going to use your branch or update it frequently. if you run it as a service then the only thing you need to get into their local environment is some socket + communication stuff. but it's all kind of a moot point since there is no existing hammer

[Kevin Lacker]

also, at least in my experience, lean frequently pegs the CPU. if processing is remote you could do something like, the server looks for a proof. if it doesn't find one, fine. if it does, then there's a little blue squiggle or other UI icon that appears at the function level that provides an affordance to auto expand the proof. that way people could start using it without explicitly being too aware of how it works. but again all this theory is moot without working hammer code

[Rob Lewis]

Sledgehammer in Isabelle does support remote provers, I think via TPTP. No clue how commonly that's used compared to local installs.

[Johan Commelin]

Mario Carneiro said:

sure, but that's already happening with the usual model

But if I update my file, then tidy starts running again, right? It doesn't report back to me 10s later, saying. "Ooh, btw, whatever shape your proof has 10s ago, I could finish it from there."

[Mario Carneiro]

I mean the isabelle sledgehammer model

[Mario Carneiro]

lean doesn't support this very well

[Jasmin Blanchette]

Lucas Allen said:

Cool, Thanks. I'll check out the link. How good is sledgehammer in Isabelle? Is it used a lot? And is it quick more or less?

I have some logs from myself and other users showing that Sledgehammer is called up to 100 times a day and succeeds in about 30-40% of cases in the wild. We've done a bigger evaluation in one of my papers (https://www.cs.vu.nl/~jbe248/mash2.pdf, see Section 7) that somewhat corroborated these results. Sledgehammer runs asynchronously. By default, most provers are run locally, which is faster than using a server. Often it finds a proof within 1 second -- there's very little overhead. It runs asynchronously, but many users wait 30 second (the default timeout) because they can't think while it's running.

[Jasmin Blanchette]

Some users (e.g. Johannes Hölzl) don't use it much, but others use it all the time. It's perhaps less useful for mathematicians than computer scientists. Hard to tell.

[Jasmin Blanchette]

Here's a message from Manuel Eberl, who's mostly a math formalizer (reproduced with permission):

Just fyi, I won the Proof Ground 2020 yesterday, this time without Peter. I was the only participant to solve all the problems and two of them were /very/ last minute. This time, I sledgehammered like crazy, using it both as an oracle to see whether I'm going in the right direction and to simply save time on proofs.

One particular subproblem (afternoon problem 2, task 2) was completely solvable by "induction, auto, sledgehammer" and I did that without even taking any time to understand what the theorem statement actually said. I later tried to prove it by hand and couldn't really figure out how to do it in a simple way, so I left the crucial step to sledgehammer even for the cleaned-up version.

So how's that for an endorsement? ;)

Manuel

[Jasmin Blanchette]

At the same time, Sledgehammer is very weak on HO goals -- e.g. it will almost always fail if the goal talks about a set comprehension. We're working on this as part of my project Matryoshka.

[Jasmin Blanchette]

We ship binaries for all the main ATPs (E, SPASS, Vampire, Z3, CVC4, ...) with Isabelle for all three platforms. Users don't have to compile anything. Sledgehammer works out of the box. It also works when I'm sitting in the metro (where I used to do lots of proving during my PhD, on my way to work).

[Jasmin Blanchette]

One of the nice things about running provers locally is that you can perform time slicing: run them repeatedly for time slices of, say, 3 s, with different options, axioms, encodings, etc. This really boosts the success rate but is hardly practicable with a remote server.

[Johan Commelin]

But on a server with (say) 32 cores, you could run all those slices in parallel...

[Johan Commelin]

I have my own server in my basement. I run lean on it all the time, because my laptop (well, let's not talk about my laptop :rofl:)

[Sebastien Gouezel]

Do you use the server remotely (i.e., from the laptop) or directly?

[Johan Commelin]

I go to the basement about once per month (-;

[Johan Commelin]

So I work from my laptop, yes

[Sebastien Gouezel]

I wasn't aware that there was a working setup for this. Is VScode running on the server or the laptop?

[Johan Commelin]

VScode runs on the server, using X forwarding

[Johan Commelin]

Since VScode uses electron, it should in principle be possible (and maybe not even hard) to decouple the editor from the lean server. But I haven't bothered about this.

[Sebastien Gouezel]

ok. So, no fancy interaction between vscode on the laptop and a Lean server running remotely. Which would be nice but indeed, as you point out, not needed at all for your use case.

[Johan Commelin]

Basically, the server is just a cheap and noisy replacement for a high-end desktop

[Johan Commelin]

(If you boot it, it sounds like an airplane taking off :grinning: )

[Yakov Pechersky]

I've used VSCode Remote SSH with DigitalOcean droplets, and I use VSCode Remote WSL as well

[Yakov Pechersky]

So the lean server is running on a droplet somewhere, or on my WSL VM, but the VSCode is on my plain old windows

[Yakov Pechersky]

And the vscode-lean extension has been fixed so that widgets etc work

[Adam Topaz]

I just heard about this:
https://github.com/cdr/code-server

[Johan Commelin]

Yakov Pechersky said:

So the lean server is running on a droplet somewhere, or on my WSL VM, but the VSCode is on my plain old windows

How did you configure VScode so that it talks to the remote lean server?

[Yakov Pechersky]

There is a VSCode running on the remote server too, and it handles communication between the two different VSCodes

[Yakov Pechersky]

but a vscode server, not the gui, of course

[Yakov Pechersky]

Is that what you meant by your X forwarding example?

[Yakov Pechersky]

My workflow doesn't look any different when I open VSCode on my home machine and point it to WSL or a droplet or anything, it sees the files on that machine. But the GUI and VSCode setup is shared across the different points accessed.

[Johan Commelin]

Yakov Pechersky said:

Is that what you meant by your X forwarding example?

Nope, with X forwarding I mean the plain old ssh -X, that allows you to run any gui on the remote, and have it display locally.

[Johan Commelin]

Yakov Pechersky said:

but a vscode server, not the gui, of course

Is that the code-server that Adam mention above?

[Julian Berman]

Both of those sound less ideal than just talking to the lean server over SSH

[Julian Berman]

As far as I've seen lean server just expects input on stdin (and ssh forwards stdin)

[Julian Berman]

So if VSCode supports you telling it what command line to use to run lean, just changing that to be ssh remoteserver lean --server whatever should likely work from your local VSCode

[Julian Berman]

(Probably I should try that before saying it, but yeah that should work...)

[Yakov Pechersky]

No, it's not the code-server, it's just the Remote-SSH functionality of VSCode. Julian's lean server forwarding is probably the best option (might be fastest in terms of updating views), but requires manual configuration.

[Adam Topaz]

Will the following in .bashrc(or .profile) work?

alias lean="ssh remoteserver lean --server"

[Julian Berman]

Probably not (sorry I don't have a VSCode setup I can try this on handy otherwise I'd just tell you what to do)

[Julian Berman]

but uh, you can't use an alias because it'll try to run that whole thing as one argument

[Julian Berman]

and also, you probably can't put that in your bashrc because VSCode probably doesn't run lean in a login / interactive shell

[Yakov Pechersky]

It'd probably be a config set in VSCode: image.png

[Adam Topaz]

Ok. I guess you can also make a small shell script

[Julian Berman]

Yeah.

[Yakov Pechersky]

But to first approximation, setting up SSH-Remote is the easiest, IMO.

[Julian Berman]

nod

[Julian Berman]

Yeah if you want to make it even nicer/well supported we add an envvar

[Julian Berman]

E.g., the most underutilized docker feature that no one seems to know about is DOCKER_HOST

[Julian Berman]

which does this for docker, so if you set that to e.g. DOCKER_HOST=ssh://server:whatever, then when you run docker commands on localhost, they use dockerd on the remote host

[Johan Commelin]

Yakov Pechersky said:

But to first approximation, setting up SSH-Remote is the easiest, IMO.

Would you mind writing a 7-line howto guide that tells me which steps I need to take to do this?

[Adam Topaz]

Ping @Matthew Ballard who told me about this code-server

[Matthew Ballard]

https://github.com/cdr/code-server/blob/v3.6.2/doc/guide.md this helpful?

[Adam Topaz]

I think what @Julian Berman is suggesting is to pipe stdin/out via ssh so lean itself would run in the cloud (or Johan's basement), and vscode would run locally.

[Kevin Lacker]

it's more and more common in industry nowadays to do the remote ssh thing, where your codebase lives remotely and you just ssh in. vscode supports it pretty well in general - https://code.visualstudio.com/docs/remote/ssh

[Kevin Lacker]

i can't speak to julian's strategy, maybe that ends up being simpler, but the remote ssh method will work for pretty much any programming language environment that you'd use vscode for

[Kevin Lacker]

there's no real reason for Johan's desktop machine to be so noisy though ;-) i wonder if it's so old the inside is caked with dust and so the fan runs at max speed all the time

[Matthew Ballard]

I wanted to runs things, eg Latex, Lean, etc.., on an iPad which hamstrings me further. Code-server was the only way in iPadOS I could find to make it happen (other than MS codespaces). With more control over the OS, I would probably go the ssh route.

[Kevin Lacker]

i see. yeah, it seems like code-server solves the problem of "My local machine can't even run VSCode." If your local machine can run VSCode fine (ie its not an ipad) then probably a better solution is one of the others.

[Matthew Ballard]

My local machine cannot ssh, run vs code, ...etc

[Matthew Ballard]

(But I can teach a class and write notes on it fairly well)

[Julian Berman]

@Johan Commelin I can likely put something together, will spend a bit of time getting something working. I can already get a POC working somewhat easily, if it helps, here's what I did quickly:

I put this in a file called ~/.local/bin/lean-remote:

#!/usr/bin/env python3
import os
import shlex
import sys
argv = ["ssh", "Home.lan", "--", "/Users/Julian/.local/bin/lean"] + [shlex.quote(arg) for arg in sys.argv[1:]]
os.execvp(argv[0], argv)

and this similar contents in a file called ~/.local/bin/leanpkg-remote:

#!/usr/bin/env python3
import os
import shlex
import sys
argv = ["ssh", "Home.lan", "--", "/Users/Julian/.local/bin/leanpkg"] + [shlex.quote(arg) for arg in sys.argv[1:]]
os.execvp(argv[0], argv)

(Obviously modify with your own server's hostname and your own server's path to Lean). Then chmod +x ~/.local/bin/lean{,pkg}-remote.

Then I changed the settings @Yakov Pechersky screenshotted to say lean-remote and leanpkg-remote in VSCode.

It works as-is already in that the server comes up, but probably leanpkg.path is now confused because it doesn't resolve anything (similar to when it can't find mathlib locally), so I'll have to investigate that. For now though I have to jump back to meetings, will look later.

[Julian Berman]

(The shlex.quote nastiness is because of lean --server getting passed *undefined* by default, which because SSH always runs a shell, you have to escape, which is annoying. That's what, telling lean server what path to assume we're talking about? If so, probably a better solution is just passing a different path there that doesn't have shell-escape-needing chars.)

[Julian Berman]

(Not sure if you even were asking about "my way" or instructions with the other way, but yeah, hopefully something there helps or if not that someone else chimes in.)

[Julian Berman]

@Kevin Lacker and yeah what's there obviously works well, it's an "old" / "trusted" technique, but personally I like it better if you just have to shuttle files back and forth... if you have to also communicate with a process, I find it a bit clunky personally, but definitely if it works for folks who am I to say.

[Johan Commelin]

@Julian Berman thanks! I'm now looking into code-server first. But will definitely also keep this in mind.

[Lucas Allen]

Thanks Jasmin for the explanation. Sledgehammer looks cool, but I wonder, instead of bringing in sledgehammer to lean, would it be easier to write an ATP in Lean? Or are the ATP's to large and complex?

[Kevin Lacker]

the ATP's aren't written in Isabelle either - they're written in some fast language like c++. lean is another step again slower than languages like python, which are themselves a lot slower than c++ for cpu-bound things like ATPs, so it's just impractical to build a whole atp in lean

[Kevin Lacker]

sledgehammer is basically a translation layer between the interactive theorem prover ie lean or similar system, and the ATP

[Mario Carneiro]

Actually, isabelle has an ATP, and it's a big player in practical isabelle usage: auto

[Mario Carneiro]

ATPs are as large and complex as you want them to be

[Mario Carneiro]

the general problem is undecidable so it's just a question of how many bells and whistles you want to build into it

[Mario Carneiro]

Isabelle is implemented in Isabelle/ML, which is a compiled functional programming language

[Mario Carneiro]

Most isabelle tactics are written in the ML part

[Mario Carneiro]

there is some trick for being able to evaluate ML blocks in an isabelle file, but I'm not exactly sure how it is accomplished (and I say this despite having spent several hours diving into the code that does this. The architecture is very complex and mostly undocumented)

[Mario Carneiro]

I think it amounts to runtime interpretation like the lean VM but don't quote me on that

[Kevin Lacker]

i thought auto was considered a tactic, like library_search or finish, rather than an ATP

[Mario Carneiro]

it is a tactic, which is to say it's implemented inside isabelle, but it is an ATP

[Mario Carneiro]

finish is an ATP written in lean

[Mario Carneiro]

if your definition of ATP requires that it not be implemented in the tactic framework then of course there aren't going to be any

[Jasmin Blanchette]

Lucas Allen said:

Thanks Jasmin for the explanation. Sledgehammer looks cool, but I wonder, instead of bringing in sledgehammer to lean, would it be easier to write an ATP in Lean? Or are the ATP's to large and complex?

super by @Gabriel Ebner is an ATP in Lean. Unfortunately the metaprogramming framework is way too slow in Lean 3.

[Jasmin Blanchette]

And ATPs are large and complex. The Sledgehammer architecture is the simplest way to benefit from all of that.

[Jasmin Blanchette]

It does rely on an ATP for proof reconstruction, called metis.

[Jasmin Blanchette]

(I wouldn't call auto an ATP although that's just terminology. It's really simp on steroids.)

[Jasmin Blanchette]

In a first approximation, metis = super but maybe 100 times faster.

[Jasmin Blanchette]

Most ATPs are designed around a logical calculus optimized for proof search, don't depend on user hints, and are complete. Again, it's not black and white, and I'm a big fan of the notion that ITP and ATP are a gradient -- but I've never heard anybody call auto or simp an ATP before. ;)

[Kevin Buzzard]

When we were in NL last year I remarked to Floris that rfl was a "high-powered AI" and he said he'd never thought of it like that before.

[Kevin Buzzard]

But I give talks in schools where I prove that 2+2=4 with a six line sequence of definitional rewrites (2+2=2+S(1)=S(2+1)=...) and then I show that the computer, despite having only just seen the definition of 2 and + (I define everything from first principles), can figure out the proof immediately.

[Jasmin Blanchette]

The other day, I tried to show the amazing power of refl on the example 5 + 5 = 25. It failed. I came up with some excuses about the unpredictability of tactics and went on for another five minutes at least.

[Jasmin Blanchette]

That's the problem when don't teach in front of physical students. ;)

[Mario Carneiro]

@Jasmin Blanchette IIRC auto is a combination of simp and a tableau theorem prover, no?

[Mario Carneiro]

or maybe I'm confusing it with blast

[Kevin Buzzard]

My live refl fail story is the following. After one school talk I was talking to some students about internal storage of naturals, and I said that the Peano approach was of course very inefficient so nothing worked with big numbers. I demonstrated this by showing them that example : 1000000000+1000000000=2000000000 := rfl failed. But it succeeded, really quickly :D . I now use example : 1000000000+2000000000=3000000000 := rfl, which does indeed time out.

[Jasmin Blanchette]

@Mario: Yes, that's the steroids part.