Zulip Chat Archive

Stream: general

Topic: CICM 2020


view this post on Zulip Rob Lewis (Jul 09 2020 at 13:51):

Registration for CICM 2020 is free and now open. The conference is July 27-30. You might see some familiar faces on the program. Check it out if you're interested!

view this post on Zulip Mario Carneiro (Jul 27 2020 at 12:31):

Kevin Buzzard will be speaking at CICM in 30 minutes: https://easychair.org/smart-program/CICM-13/2020-07-27.html#talk:155838

view this post on Zulip Patrick Massot (Jul 27 2020 at 12:59):

Is there any connection info?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 13:00):

I think you have to register

view this post on Zulip Patrick Massot (Jul 27 2020 at 13:02):

What about kindly asking someone who registered?

view this post on Zulip Patrick Massot (Jul 27 2020 at 13:03):

Many thanks to all three people who sent me independent PMs.

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:30):

Someone should really tell all those Isar zealots that there proofs actually aren't readable.

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:31):

I guess they would know this if they had ever tried to ask mathematicians, so probably they are not really interested in knowing.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 14:34):

You could say that on the slack chat

view this post on Zulip Mario Carneiro (Jul 27 2020 at 14:35):

I take serious issue with the idea that the tactic part should just be omitted

view this post on Zulip Mario Carneiro (Jul 27 2020 at 14:37):

it makes the reader dependent on the proof author since you can't dig beyond the level that the proof author thought was good enough. With sledgehammer the gaps can be quite big

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:38):

Which slack chat?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 14:38):

you would know if you registered :)

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:38):

Ok, I'll let you tell them.

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:39):

It's fascinating because proof assistants require such a degree of training that it becomes almost impossible to step back and calmly assess how unreadable everything is without proper training.

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:39):

I'm sure those people are sincere when they claim their Isar proofs are readable.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 14:40):

I think Kevin said it right - formal proofs are another language, you have to learn to read it

view this post on Zulip Jeremy Avigad (Jul 27 2020 at 14:49):

Mario, you were right to call me out for opposing "tactic proof" to "declarative proof" -- that's not what I meant. I really like Sébastien's proofs, and I count them as declarative.

But I think the point remains that there is a tension between writing short proofs and writing proofs that are easy for others to read. In Mathlib (as well as in the Mathematical Components library), the emphasis is mostly on being short and efficient, rather than on being verbose and explanatory. I am not complaining about that, only pointing out that there is a difference.

view this post on Zulip Jeremy Avigad (Jul 27 2020 at 14:50):

BTW, the Isabelle style relies heavily on automation. The goal is: "have A, by auto, have B, by auto, have C, by auto."

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:51):

Yes, this is why I wrote in the Zoom chat that what is missing is not Isar, it's automation.

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:52):

In the current state of technology, it doesn't seem realistic to me to have a single library which is good for large scale formalization and teaching. We can write readable proofs and use format_lean or something better in this spirit for teaching, but it won't be mathlib.

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:52):

And Kevin explained why this is unrealistic anyway: large scale formalization require too much mathematical sophistication for students.

view this post on Zulip Jeremy Avigad (Jul 27 2020 at 14:53):

Lean's assume, have, show, obtain, suffices, ... are all stolen from Isar, which in turn took them from Mizar. That was my point: we do have that in Lean.

view this post on Zulip Jeremy Avigad (Jul 27 2020 at 14:55):

I think that makes sense: separate exposition from the library. The key requirements on the library are efficiency and maintainability.

view this post on Zulip Patrick Massot (Jul 27 2020 at 14:55):

obtain is not stolen from Isar. I asked for it.

view this post on Zulip Johan Commelin (Jul 27 2020 at 14:55):

Are these talks recorded somewhere?

view this post on Zulip Jeremy Avigad (Jul 27 2020 at 14:56):

We had it in Lean 2 (as a proof term keyword). It went away in Lean 3, until you brought it back as a tactic.

view this post on Zulip Gabriel Ebner (Jul 27 2020 at 15:00):

@Johan Commelin Unfortunately presenters need to record their talks themselves (for legal reasons). And you're supposed to upload them to the conference slack, which is not public.

view this post on Zulip Jeremy Avigad (Jul 27 2020 at 15:02):

Interesting. What are the legal reasons? All the talks at IJCAR were live streamed on YouTube and recorded. (Maybe the presenters needed to agree to that?)

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:02):

kevin recorded his talk, and they can be uploaded anywhere

view this post on Zulip Rob Lewis (Jul 27 2020 at 15:02):

Jeremy Avigad said:

Interesting. What are the legal reasons? All the talks at IJCAR were live streamed on YouTube and recorded. (Maybe the presenters needed to agree to that?)

They did.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:02):

Claudio said "a lot of paperwork"

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 15:20):

(No suffices in Isar though. That must come from ssreflect or something.)

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:22):

someone asked about what the equivalent of moreover ... ultimately is

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 15:27):

I suppose in practice it's simp with * etc

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:29):

how hard would it be to do a direct translation of isabelle syntax into lean syntax?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:30):

are there any isabelle proof structuring mechanisms that would need to be significantly reorganized to put in lean?

view this post on Zulip Patrick Massot (Jul 27 2020 at 15:33):

Our stuff looks much more flexible anyway.

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 15:34):

We would surely know by now if there was some "way that mathematicians wanted to express an argument" which was missing in Lean

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:34):

I mean a more literal kind of translation than that

view this post on Zulip Patrick Massot (Jul 27 2020 at 15:35):

Kevin, of course there is!

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:35):

i.e. something that a regex could do

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 15:35):

The Isar context is explicit (doesn't contain everything in scope) and ordered; that alone would probably necessitate implementing a complete different tactic framework for it

view this post on Zulip Patrick Massot (Jul 27 2020 at 15:35):

Things like "Cleary, we get that...", "Details are left to the readers", etc...

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:37):

how does one determine the context at a line? Is it just this have hence moreover dance or is there more?

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 15:40):

The fundamental ones are from and using IIRC (what even is the difference? I really don't remember). have does not adding anything to the context by itself. hence is short for from this have. moreover is like giving those facts temporary names, then passing them using from when ultimately is used.

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 15:42):

from goes before have etc., using goes after. It's a stylistic distinction.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:43):

I guess from is already taken, but we could have a tactic using [h1, h2] { tac } that deletes everything from the context except for h1,h2 and dependents before calling tac

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 15:46):

Basically for every proof step you select facts from the scope as your new, ordered context that tactics can access; but they can still access facts explicitly passed to them by name.

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 15:49):

There is also some implicit backtracking going on, around ; I believe

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 15:52):

A tactic in Isabelle (unlike in HOL4 etc.) produces a possibly infinite sequences of states. Normally users only see the first one. When you combine them, depending on which tactical (i.e., operator on tactics, such as ;) you use, the sequences will be combined differently. Thus you can write simple tactics that, say, explore both the left and the right branch of a disjunction, and so on. In practice, this is very little used, though.

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 15:52):

Most of it is available only at the ML (metaprogramming) level. ; is a fairly recent (~2014) addition, inspired by Coq.

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 15:53):

The backtracking also happens around , I believe.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:54):

backtracking only happens inside tactic parts, right? Not at the top level have/show stuff

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 15:55):

Right.

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 15:57):

I think Larry, who introduced it, used it quite a bit to implement various heuristic tactics -- maybe auto uses it. But now, with the move towards Isar and Sledgehammer, it's considered quite low level.

view this post on Zulip Johan Commelin (Jul 27 2020 at 16:00):

I don't think I've ever used "ultimately" in an informal proof. I'm not sure what it means... is it just another have?

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 16:03):

It means "from all the facts I tagged with moreoever, it follows that..."

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:07):

does this also untag the moreover facts?

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 16:08):

Yes. Every moreover belongs to exactly one ultimately.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:08):

can you put other things between the moreovers and the ultimately?

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 16:09):

I don't think so, IIRC

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 16:11):

calc-like chaining is done via also ... also .... finally, btw. A little confusing to beginners, as you might imagine.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:15):

is there a cheat sheet for all this heretofore stuff?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:17):

https://isabelle.in.tum.de/doc/isar-ref.pdf has a quick reference in appendix A

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:18):

what does proof m1 qed m2 mean?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:18):

are m1 and m2 tactics, proof structure commands, or statements?

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 16:20):

Tactics, at least in the Lean lingo...? I believe the special thing about putting m2 there was that it will not backtrack to m1.

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:21):

for some reason makarius is touchy about calling "proof methods" tactics, but larry paulson always calls them tactics

view this post on Zulip Sebastian Ullrich (Jul 27 2020 at 16:27):

Oh, but after m1 you can insert some more Isar steps, i.e. have etc. So it's "I prove this fact using this initial tactic (e.g. induction), then I do some other steps, then I solve the remainder using this final tactic (e.g. slaying boring induction cases with auto)".

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:29):

so you would normally use proof ... qed where a lean proof would use brackets in subgoals?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:30):

wait, how are subgoals passed back from the tactic in a declarative proof structure?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:34):

oh, is next like swap?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 16:44):

Does anyone know where I can find the grammar of proof methods?

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 19:29):

  1. moreover and ultimately: You certainly can point to other facts as usual.

  2. proof m1 ... qed m2. This is like begin ... end in Lean, but m1 (a proof method) is applied before entering, as the first step. This makes it possible to do a bit of massaging using a proof method in an Isar proof. Similarly, the rarely used m2 after qed can kill whatever cases are left. It's useful when you do structural induction: You deal with mm of nn cases explicitly and write qed auto to kill the remaining nmn - m.

  3. A tactic is an ML (metaprogramming) concept. A proof method is an "interactive" tactic in Lean lingo, one that is registered as available in Isar. Since there's always a tactic behind a proof method, the distinction is not so relevant to most users.

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 19:31):

Wow, I had never looked at the Isar reference manual in my life. It's at least seven times longer than I expected.

view this post on Zulip Jasmin Blanchette (Jul 27 2020 at 19:32):

Hm, it has my name on the cover. Maybe I've "looked" at it before after all. ;)

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 19:46):

Me talking to a summer project student the other day: "do we have theorem X in mathlib?". The reply: "yes, because you PR'ed it a week ago". Of course I could have told this story here already :-/

view this post on Zulip Rob Lewis (Jul 28 2020 at 11:12):

FYI, there are two Lean talks today at CICM.

  • 14:15: Peter Koepke, Adrian De Lon and Anton Lorenzen, Interpreting Mathematical Texts in Naproche-SAD (and: From LaTeX to Lean with a controlled natural language)
  • 16:30: Floris van Doorn, Gabriel Ebner and Robert Lewis, Maintaining a Library of Formal Mathematics

As well as plenty of interesting non-Lean talks of course.

view this post on Zulip Johan Commelin (Jul 28 2020 at 11:18):

Today I would have some time to attend (-;

view this post on Zulip Johan Commelin (Jul 28 2020 at 11:19):

Can I still register somewhere?

view this post on Zulip Rob Lewis (Jul 28 2020 at 11:20):

https://forms.gle/oS5BVGDf6LgDGDiK8

view this post on Zulip Johan Commelin (Jul 28 2020 at 11:21):

That asks me for a google account...

view this post on Zulip Johan Commelin (Jul 28 2020 at 11:36):

Dear all, thanks for the PMs!

view this post on Zulip Patrick Massot (Jul 28 2020 at 12:06):

Are the Zoom secrets the same as yesterday?

view this post on Zulip Floris van Doorn (Jul 28 2020 at 15:03):

Nice talk, Gabriel! Too bad the questions were completely unrelated to the talk.

view this post on Zulip Johan Commelin (Jul 28 2020 at 15:03):

Yup... the talks was nice!

view this post on Zulip Johan Commelin (Jul 28 2020 at 15:04):

It's not clear to me why someone cares about teaching undergraduate mathematics students with "readable" proof assistants, and care about intuitionism enough to have it be your first question on a random talk...

view this post on Zulip Johan Commelin (Jul 28 2020 at 15:04):

Anyway, you did a good job answering the questions (-;

view this post on Zulip Patrick Massot (Jul 28 2020 at 15:08):

I'm a bit sad that I had to answer the last question myself. I guess it simply means I should start using twitter, but somehow I cannot force myself to do this. So let me at least repeat it here: Kevin has done a lot of great stuff, but when it comes to seriously using Lean to teach undergrad math during official lectures, not as a club for volunteer students, then I think I'm still the only one to do it.

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 15:28):

@Patrick Massot Sorry for forgetting about you. It's hard to compete against Kevin's prolific media presence.

view this post on Zulip Patrick Massot (Jul 28 2020 at 15:35):

I know, and I didn't want to complain about you. I'm simply a bit tired of this.

view this post on Zulip Kevin Buzzard (Jul 28 2020 at 16:17):

I have so far persuaded my university to let me teach a lean course in Jan to March 2021 for graduate students as part of some multi-university (Oxford, Warwick, Bath, Bristol, Imperial) taught course centre, and after that I'll propose an optional undergraduate lean course, but the lean component of my first year course is optional.

view this post on Zulip Patrick Massot (Jul 28 2020 at 20:44):

I have a question which is actually related to Gabriel's talk: could we have a clear message when the linter has nothing to say? Each time I run #lint I spend 20 seconds searching for a failure among all the OK messages. I'd like to see a single OK. And If there are errors then I'd like to see no OK messages.

view this post on Zulip Rob Lewis (Jul 28 2020 at 20:45):

#lint- if you're using it in VSCode.

view this post on Zulip Jalex Stark (Jul 28 2020 at 20:47):

i have had the same frustration as patrick. I wonder if it's better to rename the current#lint-to #lint and the current #lint to #lint+?

view this post on Zulip Patrick Massot (Jul 28 2020 at 20:50):

This is much better, although I wouldn't mind having some congratulation message instead of nothing (but only one such message, not 15).

view this post on Zulip Patrick Massot (Jul 28 2020 at 20:51):

And indeed I don't see why this is not the default setting.

view this post on Zulip Mario Carneiro (Jul 28 2020 at 21:18):

I don't really see why OK messages even exist?

view this post on Zulip Mario Carneiro (Jul 28 2020 at 21:18):

I guess it's nice to know all those linters exist but it seems a bit gratuitous

view this post on Zulip Rob Lewis (Jul 28 2020 at 21:19):

#lint- is silent so you can write it at the bottom of your file and leave it there. It's loud when something goes wrong and makes no message when it succeeds.

view this post on Zulip Rob Lewis (Jul 28 2020 at 21:20):

The OK messages are there so you know it's working. If it's your first time using #lint and you happened to get everything right, you might wonder if something was broken when there was no output.

view this post on Zulip Mario Carneiro (Jul 28 2020 at 21:20):

How about #lint acts the same as #lint- except that if there is no output then it says all lints pass or something like that

view this post on Zulip Rob Lewis (Jul 28 2020 at 21:22):

I think that's exactly Patrick's suggestion, which sounds fine to me, except for ruining the silent lint at the end of the file. But I'm not sure anyone uses that.

view this post on Zulip Mario Carneiro (Jul 28 2020 at 21:25):

You can still use #lint- if you want silent lint

view this post on Zulip Rob Lewis (Jul 28 2020 at 21:26):

Oh, I see what you mean. Yeah, that sounds fine.

view this post on Zulip Patrick Massot (Jul 28 2020 at 21:30):

Yes, this is what I meant.

view this post on Zulip Floris van Doorn (Jul 28 2020 at 22:57):

sounds good to me

view this post on Zulip Jason Rute (Jul 29 2020 at 00:03):

Tomorrow's afternoon's session is on Machine Learning and Theorem Proving. If you don't read the Machine Learning for Theorem Proving stream, I made a thread with a list of the talks, and links to where we've already talked about these papers on this Zulip. (I'm not saying we have to move any discussion away from this thread, but just wanted to provide this info if anyone finds it useful.)

view this post on Zulip Mario Carneiro (Jul 29 2020 at 11:23):

My talk on Metamath Zero starts in a few minutes

view this post on Zulip Johan Commelin (Jul 29 2020 at 11:27):

I'm starting the final countdown tune (-;

view this post on Zulip Jeremy Avigad (Jul 29 2020 at 12:04):

Mario, great talk!

view this post on Zulip Johan Commelin (Jul 29 2020 at 12:05):

Unfortunately I couldn't stay for the questions... we have our local seminar right now...

view this post on Zulip Johan Commelin (Jul 29 2020 at 12:06):

But I wish you lots of luck with the remainders of MMC and verifier.mmb

view this post on Zulip Johan Commelin (Jul 29 2020 at 12:07):

(This local seminar also means that I will miss the talk by Szegedy :sad:)

view this post on Zulip Patrick Massot (Jul 29 2020 at 12:09):

Arg, I come too late for Mario's talk. I should have set alarms for the whole day.

view this post on Zulip Mario Carneiro (Jul 29 2020 at 12:10):

It was recorded and I will get it up on the tubes soon

view this post on Zulip Mario Carneiro (Jul 29 2020 at 13:31):

https://youtu.be/CxS0ONDfWJg

view this post on Zulip Dan Stanescu (Jul 29 2020 at 13:37):

Is there also a record of @Gabriel Ebner's talk anywhere?

view this post on Zulip Mario Carneiro (Jul 29 2020 at 13:40):

It was posted on the conference slack, but it's not on youtube (yet?)

view this post on Zulip Gabriel Ebner (Jul 29 2020 at 13:43):

I don't have a youtube account, can I upload it to the leanprover-community one?

view this post on Zulip Rob Lewis (Jul 29 2020 at 13:43):

The user/password are what you expect!

view this post on Zulip Gabriel Ebner (Jul 29 2020 at 13:50):

https://youtu.be/5HDlgsjO8-w

view this post on Zulip Gabriel Ebner (Jul 29 2020 at 13:52):

(deleted)

view this post on Zulip Johan Commelin (Jul 29 2020 at 15:03):

Can anyone summarize Szegedy's talk? Unfortunately I had to miss it.

view this post on Zulip Johan Commelin (Jul 29 2020 at 15:03):

(Or does anyone know if it has been recorded, and if the recording will be available?)

view this post on Zulip Alex J. Best (Jul 29 2020 at 15:04):

According to the slack it wasn't recorded but there are slides, are you on the slack?

view this post on Zulip Johan Commelin (Jul 29 2020 at 15:04):

Nope :expressionless:

view this post on Zulip Mario Carneiro (Jul 29 2020 at 15:05):

A-Promising-Path-To-Autoformalization-and-General-AI.pdf

view this post on Zulip Johan Commelin (Jul 29 2020 at 15:12):

Hmmm... the slides don't really help. (Which doesn't say anything... good slides can be minimalistic.)

view this post on Zulip Johan Commelin (Jul 29 2020 at 15:14):

But it's not at all clear whether we should expect a math-prover oracle over at Mountain View some 10 years from now. All I see is a bunch of generic diagrams and some tables with numbers.
So I will have to hope for an actual recording to get the "vibe" of the talk :stuck_out_tongue_wink:

view this post on Zulip Floris van Doorn (Jul 29 2020 at 15:55):

Has Kevin's talk been uploaded anywhere? Unfortunately I missed it.

view this post on Zulip Jason Rute (Jul 29 2020 at 16:10):

@Johan Commelin I think @Christian Szegedy presented a very hopeful message basically saying that modern AI is showing amazing results and and computation is growing quite fast, but he was fairly tight lipped about what he is working on with specifics (excepted for already published papers). I think he said something non-specific about research level mathematics being formalized in the 10 years, but again I think this was more hopeful than a specific 10-year plan on his part. Is there something you are looking for specifically from the talk?

view this post on Zulip Jason Rute (Jul 29 2020 at 16:22):

I think @Lasse's Tactician system (which is similar to TacticToe) which was presented, is a very practical system if you are looking for machine learning built into a theorem prover (Coq) right now. I think the only thing stopping one from building it in Lean is a large amount of engineering. :smile:

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 16:26):

I heard Christian quoting this ten year figure last year so it should be nine years now

view this post on Zulip Jason Rute (Jul 29 2020 at 16:27):

We need one of those big countdown clocks. :clock:

view this post on Zulip Kevin Buzzard (Jul 29 2020 at 16:27):

A recording of my talk is on my laptop which is currently in a field and out of batteries

view this post on Zulip Johan Commelin (Jul 29 2020 at 16:32):

@Jason Rute Thanks for the summary. I don't really have more specific questions.

view this post on Zulip Floris van Doorn (Jul 29 2020 at 20:04):

Every future big development in AI is always 10 years away.

view this post on Zulip Pedro Sánchez Terraf (Aug 06 2020 at 21:24):

Jeremy Avigad said:

But I think the point remains that there is a tension between writing short proofs and writing proofs that are easy for others to read. In Mathlib (as well as in the Mathematical Components library), the emphasis is mostly on being short and efficient, rather than on being verbose and explanatory. I am not complaining about that, only pointing out that there is a difference.

I think this deserves attention. Also, maintainability could later depend on someone trying to understand the proof later. Here, a (more) declarative style might help.

view this post on Zulip Mario Carneiro (Aug 06 2020 at 21:28):

In lean, we work from the presumption that the proof context at all intermediate points is available. This is in common with Coq, and a significant difference from Isabelle where the expectation is that the proof text should be readable on its own. So lean tooling goes into making sure that you can see the tactic state (even if you are on a browser or something), rather than redundantly (and insufficiently) copying bits of the tactic state into lots of have and show lines.

view this post on Zulip Pedro Sánchez Terraf (Aug 06 2020 at 21:31):

I understand it is a different philosophy. This makes sense if you also aim to have a readable context.

view this post on Zulip Mario Carneiro (Aug 06 2020 at 21:32):

Kevin has said on many occasions (to the agreement of many here, I believe) that he finds tactic proofs more readable than "declarative" isar style term proofs because the tactic state provides a tremendous amount of context and clarity to the proof. (We have since lowered the gap a bit by making the proof context be visible in term proofs too.)

view this post on Zulip Pedro Sánchez Terraf (Aug 06 2020 at 21:32):

(I must insist that I have to experiment much more with Lean to have a more complete picture)

view this post on Zulip Pedro Sánchez Terraf (Aug 06 2020 at 21:33):

I also agree with @Patrick Massot that many Isar proofs you find in the wild are not readable

view this post on Zulip Mario Carneiro (Aug 06 2020 at 21:34):

I get the general sense that these term mode proofs are from the old days when lean copied isabelle, and we have since found a style of our own that is primarily backward reasoning with occasional have steps and emphasis on block structure

view this post on Zulip Pedro Sánchez Terraf (Aug 06 2020 at 21:39):

You bring an interesting point. When I first learned Isabelle, I only knew the backwards approach. I got used to it and happily used it until I realized that I was starting to think backwards. And that's not the way you want to present a proof (again, thinking in terms of a potential reader).

view this post on Zulip Kevin Buzzard (Aug 06 2020 at 22:31):

I am the worst person to talk to about these things because I can never remember what all these different kinds of proofs are. I am always surprised that there are people who see proofs in this way, asking how they fit together. Mathematicians sometimes argue forwards and sometimes backwards, and if it's in tactic mode with comments then you can normally find your way around it, whichever way it's going

view this post on Zulip Scott Morrison (Aug 06 2020 at 23:00):

One mental straightjacket that theorem provers impose is you have to prove theorems in the order that you state them. While within a tactic block you can work "forwards" and "backwards", on a bigger scale you're forced into working "forwards".

view this post on Zulip Scott Morrison (Aug 06 2020 at 23:00):

In a good maths paper, the author will tell me the big result they want me to care about, then tell me the "big ideas" of the proof (whether or not this is done inside a \begin{proof} ... \end{proof} LaTeX environment, and then spend the rest of the paper preparing promised ingredients, cleaning up loose ends, doing computations, etc. It's great to read papers like this, because you have the easy option of "Oh, Section 4 is going to prove Lemma B, and I can see how that would work, so I'm going to skip it."

view this post on Zulip Scott Morrison (Aug 06 2020 at 23:00):

Especially because long proofs tend to be slow to elaborate, in Lean, and I suspect all other theorem provers, we tend to take a much more pedagogical style of building everything up in little increments. Obviously there are some big advantages here --- no one like having to wonder if an argument has become circular, which is always a possibility once it's "non-linear". And if you're a student needing to learn all the detailed mechanics, it's no problem reading it from the beginning.

view this post on Zulip Scott Morrison (Aug 06 2020 at 23:00):

But eventually it's a bit of a hassle. :-). I can imagine a theorem prover with a new keyword promise, where you just get to state a lemma, without proving it. You then use it happily, but have to come back to it by some specified boundary. Some linearity could easily be enforced (when it's time to prove a promise, the environment is "rolled back" to the moment it was stated, perhaps).

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:02):

The idea of laying out definitions out of order is not new to computers. Consider function definition order in most programming languages

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:02):

even if you have some requirement of acyclicity it's not hard to do a topological sort

view this post on Zulip Scott Morrison (Aug 06 2020 at 23:03):

Exactly -- so why don't we have it? :-)

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:04):

I think it is good that most theorem provers don't do this. It would make it much less obvious how the argument goes

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:06):

I already find dependency ordering somewhat confusing at the file level, where lean is already textual-order-independent

view this post on Zulip Reid Barton (Aug 06 2020 at 23:08):

There are non-language specific solutions to this problem, such as literate programming (possibly somewhat language-specific) and just using multiple files indeed

view this post on Zulip Jannis Limperg (Aug 06 2020 at 23:08):

Agda has forward declarations, so you can do something like

lemma X : T

[other stuff]

lemma X := ...

Don't know how hard it would be to support this in Lean.

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:09):

what is the scope of the forward declaration?

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:09):

and can you refer to it in proofs

view this post on Zulip Reid Barton (Aug 06 2020 at 23:10):

(Using multiple files is just pushing back the problem to "how do I understand this pile of files" but now it's at least not language dependent)

view this post on Zulip Jannis Limperg (Aug 06 2020 at 23:13):

X is in scope everywhere below X, just like a regular definition. Cyclic dependencies are allowed and induce an implicit mutual block. (Lean obviously wouldn't do that.) I forget what Agda does about defeq, i.e. whether X reduces when it's used before its definition.

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:16):

If it's an implicit mutual, then you should be able to reduce it before its definition, because it already scanned forward to know the definition

view this post on Zulip Mario Carneiro (Aug 06 2020 at 23:17):

but wow there are so many ways that can go wrong

view this post on Zulip Pedro Sánchez Terraf (Aug 07 2020 at 00:52):

Scott Morrison said:

In a good maths paper, the author will tell me the big result they want me to care about, then tell me the "big ideas" of the proof (whether or not this is done inside a \begin{proof} ... \end{proof} LaTeX environment, and then spend the rest of the paper preparing promised ingredients, cleaning up loose ends, doing computations, etc.

I also enjoy this style of writing, and it is another sample of the fact that processing formal languages does not come in our genes. But we do not need to stretch the “readable sources” up to this point. In fact, formalized mathematics could be regarded as the (long) labor done to establish a result, and the write up always happens afterwards (which I imagine obtained by post-processing the sources and could cross-reference them at appropriate places).

view this post on Zulip Utensil Song (Aug 10 2020 at 15:30):

@Kevin Buzzard 's invited talk at CICM 2020 is also available on YouTube as Formalising Undergraduate Mathematics in case anyone missed it (for various reasons I just watched it today and found it really awesome and much much more informative than The Future of Mathematics? ).

view this post on Zulip Utensil Song (Aug 10 2020 at 15:30):

It's also posted on Coq's Zulip here and Coq people are also wondering if the slides are available (It's available on the CICM 2020 Slack but I don't know if it's available as a public URL too).

view this post on Zulip Utensil Song (Aug 10 2020 at 15:42):

There're also lots of interesting discussions that happened on the CICM 2020 Slack. Two questions that @Kevin Buzzard and @Mario Carneiro have spent quite some time to answer are (essentially) :

  • Why should mathematicians care about (systematic) formalization?
  • Why Lean might be a better choice for mathematicians?

The related answers are posted here as a gist here if anyone is interested.

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 21:09):

I put a link up to the slides on the YT page

view this post on Zulip Patrick Massot (Aug 10 2020 at 21:42):

I quickly read Mario and Kevin's stuff. I agree with a lot of what I see there, but I think the discussion about why Lean works better for mathematicians misses an important piece: the community help. I hope new users here stay around because they like the fact that many people spend a lot of time answering questions in the new members stream. We can spend ages describing everything that is nice in Lean, and compare it to what we think we know about the other proof assistants. But the actual reason why Kevin and I are here is that we came to Gitter (that we used to chat before Zulip) and Johannes Hölzl and especially Mario Carneiro spent days answering all our dumb questions until we started to understand something. We both tried Coq before, and it lacked a Mario.

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 22:16):

Yeah, without the community (which at that time was much smaller but was somehow still sufficiently big) Patrick and I would never have got going. Mario, Simon, Johannes and Reid were key players here -- when I was getting bogged down with the basics Mario was essential, and when I was getting bogged down with technicalities of type theory when doing schemes, and the realisation that R[1/fg] was not equal to R[1/f][1/g], Reid was invaluable.


Last updated: May 09 2021 at 19:11 UTC