Leo's talk in Oxford

Stream: general

[Kevin Buzzard]

https://easychair.org/smart-program/FLoC2018/FM-2018-07-16.html

How does that work? Can I just walk in and watch it, or do I have to pay £150 for the right wristband or whatever?

[Patrick Massot]

Will this talk be recorded?

[Luca Gerolla]

https://easychair.org/smart-program/FLoC2018/FM-2018-07-16.html

How does that work? Can I just walk in and watch it, or do I have to pay £150 for the right wristband or whatever?

It seems like you can only register for the whole Floc conference block (https://www.floc2018.org/register/)

[Kevin Buzzard]

Yeah but what if you don't register at all and then just sneak in? At a maths conference this would be trivial. My partner is a doctor and at a medical conference that would be completely impossible. Hence my question.

[Leonardo de Moura]

I believe you can just walk in. People usually do not check badges in CS conferences. They usually only check it for entering the banquet and other social events.

[Simon Hudon]

Do you know if the talk will be put online?

[Kevin Buzzard]

I believe you can just walk in. People usually do not check badges in CS conferences. They usually only check it for entering the banquet and other social events.

He was right :-)

[Johan Commelin]

It's the first rule of Lean:

Leo is always right.

[Patrick Massot]

Is it recorded?

[Gabriel Ebner]

Only the keynotes are recorded, I believe. But you can look at Leo's slides here: http://leanprover.github.io/talks/FM2018.pdf

[Mario Carneiro]

Ooh, a new MS project: https://github.com/Microsoft/AliveInLean

[Sebastian Ullrich]

For some context, this was Juneyoung Lee's intern project while at MSR Cambridge: sf.snu.ac.kr/juneyoung-lee/ (under "Experience")

[Sean Leather]

mathlib

[Gabriel Ebner]

Yeah, I'm not sure if Johannes is happy about "University of Amsterdam".

[Johan Commelin]

Haha, I didn't even catch that one yet.

[Patrick Massot]

What's the problem? Is it because there are several universities in Amsterdam?

[Johan Commelin]

Yes, and one is called "Universiteit van Amsterdam" and the other "Vrije Universiteit"

[Johan Commelin]

Johannes is based at the second.

[Patrick Massot]

Lean 4
• Leo and Sebastian Ullrich (and soon Gabriel Ebner)

:tada:

[Kevin Buzzard]

So I met Leo! He was super-nice and super-happy to talk and listen -- we spoke for over an hour. It was a real eye-opener. He has a very practical viewpoint of things, he could see exactly which of my ideas should work and which would need several million pounds to maintain :-) He was very positive about using lean to teach (this was an example of something which would not cost several million pounds to maintain). He said that in theory it would be possible to have VS Code installed on one PC and accessing an instance of Lean running on another PC -- it would be a bore to write but would definitely be possible. I wonder whether one day this would be another viable solution to the issue of Lean + mathlib + compilation etc being a pain for a generic maths student with a Windows machine.

I would summarise the talk but Gabriel posted the slides already :-)

[Patrick Massot]

What would cost million pounds?

[Patrick Massot]

About Lean and VScode, I wonder what kind of manpower would be available to develop the vscode extension. There are several things I would like to see there, some seem very easy, some seem harder. On the very easy side, one could create a set of snippets. Currently my ~/.config/Code/User/snippets/lean.json contains

{
    "Sorry": {
        "prefix": "sor",
        "body": [
          "{ $0",
          "  sorry },"
        ],
        "description": "Sorry block"
    },
    "Proof": {
        "prefix": "proof",
        "body": [
          "begin",
          "  $0",
          "  sorry",
          "end"
        ],
        "description": "Proof tactic block"
    }
}

but I'm sure there are many more that could save some time and focus. Slightly harder: I often wish there would be shortcuts to toggle options like trace or pp options. Potentially harder: implement subwindows dedicated to #check or #print or #find, with somewhat persistent output. I often use these commands and wish I could still see the result while editing my code, without freezing the message window because I need to see the current proof state.

[Mario Carneiro]

I think a snippet for theorem would be nice

[Patrick Massot]

what would it write for you?

[Mario Carneiro]

also set_option takes too long to type, and I get no vscode help until I get to the options themselves

[Kenny Lau]

"sor" is exactly how we say "sorry" in Hong Kong lol

[Mario Carneiro]

might be nice if there was some kind of autocomplete from e.g. #all to set_option pp.all true

[Kenny Lau]

it suddenly feels so familiar

[Kenny Lau]

(sorry off-topic)

[Sean Leather]

I've wondered why put the # in #check but not in set_option.

[Mario Carneiro]

I've always felt that was not a good choice

[Patrick Massot]

I start with #set_opt... at least half time

[Mario Carneiro]

the reasoning is that the # is for temporary lines

[Sean Leather]

Oh. That never would have occurred to me.

[Patrick Massot]

most set_option commands I use are temporary

[Mario Carneiro]

and even though set_option is used for temporary lines 99% of the time (in my experience), I guess leo was thinking about some permanent options like set_option old_structure_cmd true

[Mario Carneiro]

I'd prefer if these were separated into two sets of options

[Kevin Buzzard]

What would cost million pounds?

Putting Lean into the high school curriculum. Proving a hard theorem and then keeping it proved -- maintaining the code. I also met Gonthier. Leo asked him about maintaining the odd order proof and Gonthier said that on average every second release of Coq breaks the proof and he has to fix it, but he never used simp, he only used dsimp, so it usually doesn't break badly. Leo stressed that it's not just about writing code, maintaining it is very boring, hard work, and costs money. He observed that Hales was going to run into this issue. He was extremely positive about Hales' FABStracts (is that how it's spelt nowadays?). He mentioned it in the talk, but he said that he believed that the project was achievable (he said something like it was on the "boundary of what could be achieved", which in my opinion is a really good place to be -- perhaps the best place to be) -- however he stressed the need to maintain it, and he stressed that this was not a trivial thing. Maths papers don't need maintaining -- perhaps this was why he chose to hammer this point home to me several times. It is not only true, but it's important and non-trivial -- one has to continue to get people to write the cheques, or else the project dies.

[Mario Carneiro]

Proving a hard theorem and then keeping it proved -- maintaining the code

This doesn't cost a million pounds

[Mario Carneiro]

It requires people who care

[Johannes Hölzl]

With Lean's current pace, it is not possible to maintain large projects. It will be a lot of work to port mathlib from Lean3 to Lean4. Two changes I already know:

• no end for match
• inductive will remove a difference between Prop and Sort: the produced recursor for for inductive predicates will also be dependent.
  We will see what else will change. The syntactic changes are easy, changes to the elaborator will be harder. I hope we will find a good way to soften the translation from Lean3 -> Lean4.

[Johannes Hölzl]

Changes to the simplifier are usually not as problematic as it seams. But this strongly depends on the proof style. If you do a lot of tactic / ssreflect like proofs, changes can be very bad. For Isabelle's declarative proofs usually it isn't a too big of a problem. The AFP contains a lot of simp proofs: I would guess in Isabelle each second proof step depends on the simplifier, and the simplifier setup changes regularly. Yet, the AFP is growing and the Isabelle community manages to keep pace.

[Gabriel Ebner]

About Lean and VScode, I wonder what kind of manpower would be available to develop the vscode extension.

From my point of view, what we're missing atm is not manpower but ideas. I'm willing to bring help anyone who wants to work on the vscode extension.

[snippets]

I think we can include them in the extension. Feel free to submit a PR. This could be a controversial addition, people were already up in arms about :tada: :shrug:

[extra windows for #check, etc.]

This will probably have to wait for Lean 4. I talked with Johannes and Rob about some hacky workarounds when I was in Amsterdam, but stuff like "find the next empty line, insert #check, wait for the output, then delete it again" doesn't excite me too much.

[Patrick Massot]

Ok, this is what I thought. I added more stuff to my snippets file, following Mario's suggestions in particular. I'll work with them for a while to see if they are useful, and then I'll PR.

[Johannes Hölzl]

Another Lean4 change, important for writing tactics: Leo told me that the local_const constructor will loose the attached type, we will need to manage the typing context more explicitly. Also expr looses macro but gains a constructors to represent projections, and to represent literals.

[Mario Carneiro]

that's probably a good thing, currently the type attached to a local_const is wrong half the time anyway so you have to use the local context