## Stream: general

### Topic: Leo's talk in Oxford

#### Kevin Buzzard (Jul 06 2018 at 22:09):

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 (Jul 07 2018 at 07:55):

Will this talk be recorded?

#### Luca Gerolla (Jul 07 2018 at 08:30):

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 (Jul 07 2018 at 08:34):

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 (Jul 07 2018 at 10:35):

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 (Jul 07 2018 at 16:26):

Do you know if the talk will be put online?

#### Kevin Buzzard (Jul 16 2018 at 07:51):

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 (Jul 16 2018 at 07:51):

It's the first rule of Lean:

Leo is always right.

Is it recorded?

#### Gabriel Ebner (Jul 16 2018 at 09:14):

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 (Jul 16 2018 at 09:22):

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

#### Sebastian Ullrich (Jul 16 2018 at 09:26):

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

mathlib

#### Gabriel Ebner (Jul 16 2018 at 09:35):

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

#### Johan Commelin (Jul 16 2018 at 09:38):

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

#### Patrick Massot (Jul 16 2018 at 09:47):

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

#### Johan Commelin (Jul 16 2018 at 09:48):

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

#### Johan Commelin (Jul 16 2018 at 09:48):

Johannes is based at the second.

#### Patrick Massot (Jul 16 2018 at 10:04):

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

#### Kevin Buzzard (Jul 16 2018 at 11:20):

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 (Jul 16 2018 at 11:55):

What would cost million pounds?

#### Patrick Massot (Jul 16 2018 at 12:03):

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 (Jul 16 2018 at 12:04):

I think a snippet for theorem would be nice

#### Patrick Massot (Jul 16 2018 at 12:04):

what would it write for you?

#### Mario Carneiro (Jul 16 2018 at 12:04):

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

#### Kenny Lau (Jul 16 2018 at 12:05):

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

#### Mario Carneiro (Jul 16 2018 at 12:05):

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

#### Kenny Lau (Jul 16 2018 at 12:05):

it suddenly feels so familiar

#### Kenny Lau (Jul 16 2018 at 12:05):

(sorry off-topic)

#### Sean Leather (Jul 16 2018 at 12:05):

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

#### Mario Carneiro (Jul 16 2018 at 12:06):

I've always felt that was not a good choice

#### Patrick Massot (Jul 16 2018 at 12:06):

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

#### Mario Carneiro (Jul 16 2018 at 12:06):

the reasoning is that the # is for temporary lines

#### Sean Leather (Jul 16 2018 at 12:06):

Oh. That never would have occurred to me.

#### Patrick Massot (Jul 16 2018 at 12:07):

most set_option commands I use are temporary

#### Mario Carneiro (Jul 16 2018 at 12:07):

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 (Jul 16 2018 at 12:08):

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

#### Kevin Buzzard (Jul 16 2018 at 12:21):

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 (Jul 16 2018 at 12:22):

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

This doesn't cost a million pounds

#### Mario Carneiro (Jul 16 2018 at 12:23):

It requires people who care

#### Johannes Hölzl (Jul 16 2018 at 12:33):

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 (Jul 16 2018 at 12:40):

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 (Jul 16 2018 at 12:59):

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 (Jul 16 2018 at 13:33):

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 (Jul 16 2018 at 13:34):

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 (Jul 16 2018 at 13:35):

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

Last updated: May 18 2021 at 16:25 UTC