talk on ATP and ITP

Stream: general

[Jeremy Avigad]

I finished a draft of a talk on automated reasoning and interactive theorem proving, which I will deliver next week. The talk is here:
http://www.andrew.cmu.edu/user/avigad/Talks/london.pdf
An associated repository is here:
https://github.com/avigad/arwm
I am grateful to everyone who has shared their thoughts and experiences.

[Daniel Donnelly]

@Jeremy Avigad thanks for the announcement. Will you be delivering a live video that I can join?

[Jeremy Avigad]

I don't think the talks at the conference will be recorded or live-streamed. But preparing it was more work that I thought it would be, and I'll be happy to repeat the performance at any time.

[Floris van Doorn]

typo around slide 21: so far Jesse and I only showed that \neg CH is consistent with set theory (i.e. CH is unprovable from ZFC).

[Jeremy Avigad]

Oops, sorry. Thanks for catching that. I'll put a fixed version online tomorrow.

[Jesse Michael Han]

we are close to finishing, though---modulo the construction of aleph one, the forcing argument for the consistency of CH is done

[Jeremy Avigad]

Way cool!

[Johan Commelin]

@Jeremy Avigad And on the slide before that (p.20) there is an n too much in my name :stuck_out_tongue_wink:

[Johan Commelin]

Tangentially related: https://www.hillelwayne.com/post/theorem-prover-showdown/

[Patrick Massot]

Still about people, I guess Scott will be surprised to learn he does "quantum field
theory", which is a part of physics or mathematical physics. He studies topological quantum field theories, a part of topology very remotely related to physics :smiley:

My description is accurate but surprisingly specific compared to others. If you want to be as vague as what you use for Johan and Kevin you can write "Differential topology and geometry"

[Scott Morrison]

(I agree that I don't do quantum field theory. I do regularly go to conferences about topological phases, with physicists. :-)

[Jason Rute]

Small pedantic grammar typo: “more white squares than black squares”

[Jeremy Avigad]

Thanks for all these corrections! They should all be fixed now.

[Alistair Tucker]

More pedantry :slight_smile: : on page 54 isn't that a statement of uniform continuity?

[Simon Hudon]

@Jeremy Avigad I think you misspelled @Johan Commelin's name on page 20

[Jeremy Avigad]

@Simon Hudon Isn't it fixed now? http://www.andrew.cmu.edu/user/avigad/Talks/london.pdf.
@Alistair Tucker No, it's regular continuity, since the delta is chosen for a fixed y. (The instance I used is the y from two slides back, and also a particular epsilon.)

[Simon Hudon]

My bad! I didn't see that someone reported it already

[Ulrik Buchholtz]

Just read the slides; very nice! Just two comments: p. 7: "can our should",
p. 56: we've reached the "Speculation" part of the recap, but the slide title is "Conclusions."
I agree that the basic “plumbing” of elaboration, instance search, implicit arguments, etc., including bundling/unbundling, is some of the most important pieces of automation, and it's important that it's fast and predictable. I haven't played with Lean 3 yet, but from what I've gathered from lurking and skimming the discussions here, there's still some ways to go before we (in the ITP community) figure that out, although Lean 2 was already pretty good.

[Jeremy Avigad]

@Ulrik Thanks! I am in London now, returning home tomorrow. The talk was well received. I'll fix the typo when I get back.

[Kevin Buzzard]

I'm really sorry I missed it Jeremy. I'm at MSR visiting Leo -- I also spoke today. Did they video your talk?

[Jeremy Avigad]

No, it was not recorded, but I didn't say anything that wasn't on the slides. (I did get through most of the slides, though I had to skip one or two.)

I hope you recognize that everyone here is much more interested in hearing about your visit. Please do send a report when you can find the time.

[Kevin Buzzard]

I can report here and now if you like. I learnt far less about stuff like Lean 4 than some of you were probably hoping. I just asked stupid questions: "When will Lean 4 be ready?" I asked -- and the answer was "It's ready already! The repository is public!". The tactic framework is coming, hopefully within the next month or two; Leo is currently highly motivated to get it done because Selsam needs it for the IMO project.

Type class inference is really complicated and Leo again actively urges us users to tell him about explicit examples where Lean 3's type class inference is struggling. Someone mentioned mv_polynomial but I've never used that stuff; Leo wants to see some far more specific explicit examples of type class inference or coercions failing rather than us just pointing him to modules with unspecified problems. He is interested in examples of the abstract syntax tree and why Lean 3's algorithms are not working well on it. Let me say this again explicitly. Leo does not have some amazingly clever answer to type class inference and coercions which is guaranteed to solve all of our problems and he is asking for our input in a very precise way here. He seemed to be genuinely interested in this question -- extending Prolog to this dependent type domain -- as an algorithmic challenge, and I believe he wants to work on it. He does not read the chat though. I showed him Johannes Hoelzl's write-up of the int -> nat timeout thing and he had not seen this before, as far as I know. He wants more stuff like this.

Things which are probably already known but which I hadn't really realised -- when you run Lean 4 on a Lean file it turns it into a C file. Apparently this is important because Lean can now be compiled instead of interpreted. I am a complete amateur here and version 1 of this post might be a load of old twaddle -- please take with a pinch of salt. Let me try and explain three reasons which I think they tried to explain to me about why this might be important. I think.

1) Let's say I'm just doing some simple stuff with the integers, except I want to use the ring tactic a lot. If I import ring then a whole bunch of other stuff gets imported which I don't even need. Apparently now it will be more easy to somehow just run ring independently and just keep the proof term without having to import all the modules which ring imports at all.

2) constant a : A doesn't work any more. You either supply a proof of existence (constant a : A := <construction of term of type A which will be opaque, classical.some is fine>) or give it some C code which you already checked will produce a term of this type if asked (e.g. a compiled version of the construction which you only had to compile once); you pass the C code in via an attribute.

3) Computer scientists might want to use Lean to write formally verified code, because its performance is now better in certain situations than Haskell or C++. Here is an example of something that can be done. Computer scientists do not actually need that code is formally proved correct. They just need that it is extremely likely to be correct, because if a machine says it's correct then this is evidence that any actual bugs in the system would be extremely hard to exploit. Computer scientists are apparently not keen on unary addition, they seem to prefer something called gmp.c or something. But Leo is going to let refl have the option that if it runs into nat.add it will just call some arbitrary c code to do the addition. So example: 1000+1000=2000:= by rfl will be instant if you are using some sensible software, and it would also I guess be trivial to write a small c program which you could point addition to and then prove 2 + 2 = 5 by rfl. Same with nat.mul.

Perhaps as a consequence of (2), or perhaps this is some unrelated thing -- nothing needs to be meta any more. I don't really understand why. Expr is not meta. meta is now called unsafe. It's very hard to find any Lean code in the kernel which is marked as unsafe. unsafe_cast was one of the few examples.

Another thing which was stressed to me was that porting mathlib to Lean 4 will be extremely difficult. They have changed the elaborator and loads of the core Lean 3 files
have hundreds of errors when you throw them into Lean 4. Porting will be hard work. On the other hand Leo seemed to think that someone like Sebastian would be able to write some sort of import/export functionality which would mean that we could use Lean 3 olean files as imports into Lean 4 files. The technical problem with this is that there are some fundamental things like nat whose internal storage changed between Lean 3 and Lean 4 so there would have to be some hackery to get this working -- to get the terms to be accepted.

But honestly we spent most of the time I was there talking about how humans do IMO problems.

[Jeremy Avigad]

Thanks for the report. It sounds like an interesting and fruitful meeting, including the discussion of how humans do IMO problems. Maybe I'll get you to reconstruct some of that one day in person.

[Andrew Ashworth]

Do you know if (3) is a thing right this moment in the Lean 4 repository? If so I'd like to start exploring it.

[Kevin Buzzard]

I'm afraid I have no idea.

[Reid Barton]

(2) is interesting, we were discussing exactly this this morning, in regards to the real numbers (@Mario Carneiro)

[Chris Hughes]

I made a repository of examples of type class failures in Lean 3. Most of them depend on using some old commit of mathlib. The respository is here

[Scott Morrison]

Another thing which was stressed to me was that porting mathlib to Lean 4 will be extremely difficult. They have changed the elaborator and loads of the core Lean 3 files
have hundreds of errors when you throw them into Lean 4. Porting will be hard work. On the other hand Leo seemed to think that someone like Sebastian would be able to write some sort of import/export functionality which would mean that we could use Lean 3 olean files as imports into Lean 4 files. The technical problem with this is that there are some fundamental things like nat whose internal storage changed between Lean 3 and Lean 4 so there would have to be some hackery to get this working -- to get the terms to be accepted.

Is this something that we can be working on already? This would be a complete game-changer --- I've been assuming until now that migrating was going to require going over files lines by line, hopefully with some automatic assistance. The prospect of just renaming everything to a .lean3 file and being able to import is pretty exciting.