Zulip Chat Archive

Stream: general

Topic: CICM 2020

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!

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

Patrick Massot (Jul 27 2020 at 12:59):

Is there any connection info?

Mario Carneiro (Jul 27 2020 at 13:00):

I think you have to register

Patrick Massot (Jul 27 2020 at 13:02):

What about kindly asking someone who registered?

Patrick Massot (Jul 27 2020 at 13:03):

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

Patrick Massot (Jul 27 2020 at 14:30):

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

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.

Mario Carneiro (Jul 27 2020 at 14:34):

You could say that on the slack chat

Mario Carneiro (Jul 27 2020 at 14:35):

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

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

Patrick Massot (Jul 27 2020 at 14:38):

Which slack chat?

Mario Carneiro (Jul 27 2020 at 14:38):

you would know if you registered :)

Patrick Massot (Jul 27 2020 at 14:38):

Ok, I'll let you tell them.

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.

Patrick Massot (Jul 27 2020 at 14:39):

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

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

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.

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."

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.

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.

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.

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.

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.

Patrick Massot (Jul 27 2020 at 14:55):

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

Johan Commelin (Jul 27 2020 at 14:55):

Are these talks recorded somewhere?

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.

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.

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?)

Mario Carneiro (Jul 27 2020 at 15:02):

kevin recorded his talk, and they can be uploaded anywhere

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.

Mario Carneiro (Jul 27 2020 at 15:02):

Claudio said "a lot of paperwork"

Jasmin Blanchette (Jul 27 2020 at 15:20):

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

Mario Carneiro (Jul 27 2020 at 15:22):

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

Sebastian Ullrich (Jul 27 2020 at 15:27):

I suppose in practice it's simp with * etc

Mario Carneiro (Jul 27 2020 at 15:29):

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

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?

Patrick Massot (Jul 27 2020 at 15:33):

Our stuff looks much more flexible anyway.

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

Mario Carneiro (Jul 27 2020 at 15:34):

I mean a more literal kind of translation than that

Patrick Massot (Jul 27 2020 at 15:35):

Kevin, of course there is!

Mario Carneiro (Jul 27 2020 at 15:35):

i.e. something that a regex could do

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

Patrick Massot (Jul 27 2020 at 15:35):

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

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?

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.

Jasmin Blanchette (Jul 27 2020 at 15:42):

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

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

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.

Sebastian Ullrich (Jul 27 2020 at 15:49):

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

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.

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.

Jasmin Blanchette (Jul 27 2020 at 15:53):

The backtracking also happens around , I believe.

Mario Carneiro (Jul 27 2020 at 15:54):

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

Jasmin Blanchette (Jul 27 2020 at 15:55):

Right.

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.

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?

Sebastian Ullrich (Jul 27 2020 at 16:03):

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

Mario Carneiro (Jul 27 2020 at 16:07):

does this also untag the moreover facts?

Sebastian Ullrich (Jul 27 2020 at 16:08):

Yes. Every moreover belongs to exactly one ultimately.

Mario Carneiro (Jul 27 2020 at 16:08):

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

Sebastian Ullrich (Jul 27 2020 at 16:09):

I don't think so, IIRC

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.

Mario Carneiro (Jul 27 2020 at 16:15):

is there a cheat sheet for all this heretofore stuff?

Mario Carneiro (Jul 27 2020 at 16:17):

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

Mario Carneiro (Jul 27 2020 at 16:18):

what does proof m1 qed m2 mean?

Mario Carneiro (Jul 27 2020 at 16:18):

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

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.

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

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)".

Mario Carneiro (Jul 27 2020 at 16:29):

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

Mario Carneiro (Jul 27 2020 at 16:30):

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

Mario Carneiro (Jul 27 2020 at 16:34):

oh, is next like swap?

Mario Carneiro (Jul 27 2020 at 16:44):

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

Jasmin Blanchette (Jul 27 2020 at 19:29):

moreover and ultimately: You certainly can point to other facts as usual.
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 $m$ of $n$ cases explicitly and write qed auto to kill the remaining $n - m$ .
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.

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.

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. ;)

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 :-/

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.

Johan Commelin (Jul 28 2020 at 11:18):

Today I would have some time to attend (-;

Johan Commelin (Jul 28 2020 at 11:19):

Can I still register somewhere?

Rob Lewis (Jul 28 2020 at 11:20):

https://forms.gle/oS5BVGDf6LgDGDiK8

Johan Commelin (Jul 28 2020 at 11:21):

That asks me for a google account...

Johan Commelin (Jul 28 2020 at 11:36):

Dear all, thanks for the PMs!

Patrick Massot (Jul 28 2020 at 12:06):

Are the Zoom secrets the same as yesterday?

Floris van Doorn (Jul 28 2020 at 15:03):

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

Johan Commelin (Jul 28 2020 at 15:03):

Yup... the talks was nice!

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...

Johan Commelin (Jul 28 2020 at 15:04):

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

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.

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.

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.

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.

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.

Rob Lewis (Jul 28 2020 at 20:45):

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

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+?

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).

Patrick Massot (Jul 28 2020 at 20:51):

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

Mario Carneiro (Jul 28 2020 at 21:18):

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

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

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.

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.

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

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.

Mario Carneiro (Jul 28 2020 at 21:25):

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

Rob Lewis (Jul 28 2020 at 21:26):

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

Patrick Massot (Jul 28 2020 at 21:30):

Yes, this is what I meant.

Floris van Doorn (Jul 28 2020 at 22:57):

sounds good to me

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.)

Mario Carneiro (Jul 29 2020 at 11:23):

My talk on Metamath Zero starts in a few minutes

Johan Commelin (Jul 29 2020 at 11:27):

I'm starting the final countdown tune (-;

Jeremy Avigad (Jul 29 2020 at 12:04):

Mario, great talk!

Johan Commelin (Jul 29 2020 at 12:05):

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

Johan Commelin (Jul 29 2020 at 12:06):

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

Johan Commelin (Jul 29 2020 at 12:07):

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

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.

Mario Carneiro (Jul 29 2020 at 12:10):

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

Mario Carneiro (Jul 29 2020 at 13:31):

https://youtu.be/CxS0ONDfWJg

Dan Stanescu (Jul 29 2020 at 13:37):

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

Mario Carneiro (Jul 29 2020 at 13:40):

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

Gabriel Ebner (Jul 29 2020 at 13:43):

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

Rob Lewis (Jul 29 2020 at 13:43):

The user/password are what you expect!

Gabriel Ebner (Jul 29 2020 at 13:50):

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

Gabriel Ebner (Jul 29 2020 at 13:52):

(deleted)

Johan Commelin (Jul 29 2020 at 15:03):

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

Johan Commelin (Jul 29 2020 at 15:03):

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

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?

Johan Commelin (Jul 29 2020 at 15:04):

Nope :expressionless:

Mario Carneiro (Jul 29 2020 at 15:05):

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

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.)

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:

Floris van Doorn (Jul 29 2020 at 15:55):

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

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?

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:

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

Jason Rute (Jul 29 2020 at 16:27):

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

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

Johan Commelin (Jul 29 2020 at 16:32):

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

Floris van Doorn (Jul 29 2020 at 20:04):

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

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.

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.

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.

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.)

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)

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

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

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).

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

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".

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."

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.

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).

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

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

Scott Morrison (Aug 06 2020 at 23:03):

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

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

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

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

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.

Mario Carneiro (Aug 06 2020 at 23:09):

what is the scope of the forward declaration?

Mario Carneiro (Aug 06 2020 at 23:09):

and can you refer to it in proofs

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)

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.

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

Mario Carneiro (Aug 06 2020 at 23:17):

but wow there are so many ways that can go wrong

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).

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? ).

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).

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.

Kevin Buzzard (Aug 10 2020 at 21:09):

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

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.

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: Dec 20 2023 at 11:08 UTC