## Stream: general

### Topic: lean4

#### Chris Hughes (Mar 10 2018 at 16:24):

Just noticed this. https://github.com/leanprover/lean/commit/16f28315eeddf996f85bff96954cd31a94aa4562 Is this something happening imminently or ages away? How badly will this break mathlib?

#### Andrew Ashworth (Mar 10 2018 at 16:29):

heh, that's news to me. lean 3 had a good run

#### Andrew Ashworth (Mar 10 2018 at 16:31):

if-then-else moves from coercing from Prop to bool to traditional reflection using boolean-valued function

#### Andrew Ashworth (Mar 10 2018 at 16:37):

this design doc is very exciting, it seems to hold a lot of improvements for using lean as a programming language

#### Patrick Massot (Mar 10 2018 at 16:40):

Can anyone see anything which could be related to using Lean as a proof assistant in this design notes?

#### Simon Hudon (Mar 10 2018 at 16:42):

This looks really good :)

#### Andrew Ashworth (Mar 10 2018 at 16:42):

no, not in the sense the mathematicians in this channel are using lean, except for scott, since he uses many tactics

#### Simon Hudon (Mar 10 2018 at 16:42):

@Patrick Massot Not sure yet. I'll keep poring over it and let you know

#### Andrew Ashworth (Mar 10 2018 at 16:43):

obviously all of mathlib is going to break since lean4 isn't going to have an algebraic hierarchy

#### Andrew Ashworth (Mar 10 2018 at 16:43):

and that's just one of many big problems

#### Patrick Massot (Mar 10 2018 at 16:44):

Moving the algebraic hierarchy from core to mathlib rather sounds like good news

#### Patrick Massot (Mar 10 2018 at 16:44):

It was strange to see it in core

#### Patrick Massot (Mar 10 2018 at 16:45):

And it currently prevent us from changing anything there

#### Andrew Ashworth (Mar 10 2018 at 16:45):

well, i could understand why, having a model of integers and rational numbers is important for computing

#### Andrew Ashworth (Mar 10 2018 at 16:46):

it also means Leo is punting on redoing the algebraic hierarchy

#### Andrew Ashworth (Mar 10 2018 at 16:49):

ahhh, the new vm is going to support unboxed types...!

#### Sebastian Ullrich (Mar 10 2018 at 16:53):

@Andrew Ashworth You seem to have missed the "incrementally rebuild core lib" part :)

#### Andrew Ashworth (Mar 10 2018 at 16:55):

i did, but you've been holding out on this important piece of news!

#### Sebastian Ullrich (Mar 10 2018 at 16:56):

I did expect someone in here to find it soon enough

#### Patrick Massot (Mar 10 2018 at 16:56):

Was it different when going from Lean2 to Lean3?

#### Sebastian Ullrich (Mar 10 2018 at 16:57):

We don't want to change the language, esp. syntax, this time (apart from fixing things). I think.

#### Patrick Massot (Mar 10 2018 at 16:59):

Would I see any difference then?

#### Patrick Massot (Mar 10 2018 at 16:59):

Or is it only about Andrew-syle use of Lean?

#### Sebastian Ullrich (Mar 10 2018 at 17:02):

The parser will enable better tooling and mathy notation. Most other things will enable more powerful and faster tactics.

#### Patrick Massot (Mar 10 2018 at 17:02):

More math automation?

#### Andrew Ashworth (Mar 10 2018 at 17:03):

only if someone like mario or scott decides to write a tactic to do so, i imagine

#### Kevin Buzzard (Mar 10 2018 at 17:13):

Is any time frame known for Lean 4?

#### Sebastian Ullrich (Mar 10 2018 at 17:14):

Kinda hard to say since we haven't even started yet

#### Kevin Buzzard (Mar 10 2018 at 17:15):

So we can at least say that it will not happen, say, within 1 month. Is the idea just to stop working on Lean 3 completely?

#### Sebastian Ullrich (Mar 10 2018 at 17:18):

No, we'll probably start on Monday

:)

#### Patrick Massot (Mar 10 2018 at 17:19):

So you finish the monad stuff and stop working in Lean 3?

#### Sebastian Ullrich (Mar 10 2018 at 17:19):

I wouldn't expect many new features for Lean 3 at least. Well, the important ones are on the lean4 list anyway.

#### Patrick Massot (Mar 10 2018 at 17:20):

How long did it take last time you rewrote Lean from scratch?

#### Patrick Massot (Mar 10 2018 at 17:21):

I'm asking only out of curiosity, I'm very very far from having exhausted Lean 3 possibilities for math

#### Sebastian Ullrich (Mar 10 2018 at 17:23):

I'd have to check, I didn't participate in the Lean 3 rewrite. I still had a thesis to write in Lean 2.

#### Kevin Buzzard (Mar 10 2018 at 17:25):

This is only tangentially related, but would it be possible to get more devs from somewhere? Will MS pay for more? Can people apply for grant money for more? Or is there some problem of the form "Leo doesn't trust anyone enough to mess with his code"?

#### Kevin Buzzard (Mar 10 2018 at 17:26):

Also only tangentially related, but is there any chance of some sort of "stable release" i.e. announce that what we currently have is called Lean 3.4?

#### Andrew Ashworth (Mar 10 2018 at 17:28):

is that helpful for you if mathlib continues to keep up with nightly lean?

#### Sebastian Ullrich (Mar 10 2018 at 17:30):

Yes, there will be a stable release before branching. I don't know if mathlib wants to stick with that or the new nightlies for random bug fixes.

#### Kevin Buzzard (Mar 10 2018 at 17:31):

That's great news about the stable release. I will be using Lean as part of my course

#### Kevin Buzzard (Mar 10 2018 at 17:31):

in October, and if Lean 4 is still quite chaotic it will be very easy to explain to the students to use Lean 3.4

#### Kevin Buzzard (Mar 10 2018 at 17:31):

There is enough in mathlib and Lean 3 for me to be able to do what I want to do

#### Andrew Ashworth (Mar 10 2018 at 17:59):

This is only tangentially related, but would it be possible to get more devs from somewhere? Will MS pay for more? Can people apply for grant money for more? Or is there some problem of the form "Leo doesn't trust anyone enough to mess with his code"?

I am curious about how MSR allocates funding for internal projects; I don't know how it works when you're self-funded by a large company

#### Moses Schönfinkel (Mar 10 2018 at 18:28):

@Sean Leather Heh... so my comment about Lean4 turns out to be prophetic rather than funny! :)

#### Mario Carneiro (Mar 10 2018 at 19:59):

IIRC the lean 3 rewrite took about a year, maybe a bit more

#### Mario Carneiro (Mar 10 2018 at 20:01):

The lean 4 plan there is basically the union of all the large scale lean projects currently under consideration. I expect it will take at least 6 months as a low estimate

#### Mario Carneiro (Mar 10 2018 at 20:02):

As far as "will it break mathlib", I would say probably yes, but in a good way - moving things out of core lib is music to my ears

#### Kevin Buzzard (Mar 10 2018 at 20:57):

I honestly think that writing maths again from scratch might be a lot of fun. I have never seen mathematics grown from the axioms before. There are still huge chunks of mathlib that I haven't read properly. Has anyone in the world read the Matiysevich stuff, for example? I am a number theorist and I know the theory, and I know exactly what the statement of the main theorem is, but I have no idea how he is proving it. Some of the later code looks quite unlike anything I've seen before in Lean. If I had to code up that mathematics it would take me months. Is there a chance that that high-powered stuff will have to be substantially rewritten to port it to Lean 4, or might it just be a case of redoing the basics?

#### Scott Morrison (Mar 10 2018 at 21:06):

My very uninformed guess from reading Leo's roadmap is that the high-powered stuff may not actually need a complete rewrite. I'm glad you see it as "an opportunity, not a problem".

#### Sean Leather (Mar 12 2018 at 14:16):

Eish! I go away for a few days (family visiting) and return to find the Lean world flipped upside down again. At what point do we get past the always-started-never-finished phase? That is, I've understood Lean 3 to be “experimental” since it began, and now Lean 4 is being started, but Lean 3 never officially dropped the label. Why not just continue incrementally developing Lean 3 using the same goals instead of starting over?

#### Patrick Massot (Mar 12 2018 at 14:43):

I don't understand anything about the C++ code of Lean, but I think there is not much news here. We knew big changes were coming (at least #1601, #1674, #1692). I don't see how one could rewrite the parser from scratch without going through an unusable state. So there is clearly a need for a separate branch doing that. Why not calling it Lean4? Also @Sebastian Ullrich told us the syntax should not change much this time. On top of that we learn that Mario and Johannes will be given complete freedom do handle mathlib instead of having some part of it stuck in core lib. It looks like the ideal solution to enjoy the greatness of all those people without the recent tension.

#### Patrick Massot (Mar 12 2018 at 14:44):

And we can still use Lean 3 in the mean time

#### Sebastian Ullrich (Mar 12 2018 at 14:47):

Well said. Maybe we'll decide to call it Lean 3.5 after all in the end if there aren't many breaking changes

#### Sebastian Ullrich (Mar 12 2018 at 14:48):

Though I'm not sure when "let's temporarily shrink core lib" became "let's remove the algebraic hierarchy from core lib forever" :)

#### Sean Leather (Mar 12 2018 at 15:21):

@Patrick Massot I have nothing against anything you're saying. I just wonder if it's not possible to remove stuff, rather than start over and add it back. But @Sebastian Ullrich certainly knows better.

#### Kevin Buzzard (Mar 12 2018 at 15:40):

@Sebastian Ullrich -- Leo has made it completely clear that he felt that "now" was not the time to be developing mathlib. Of course what he cannot control is the fact that you guys have made a system in which doing mathematics is quite fun, and hence it is simply inevitable that there will be people doing mathematics in Lean. I hope to have students publishing simple papers in undergraduate mathematics journals about how they have used Lean, for example, and this is not going away whatever Leo's opinion is [in fact I think this fits well with Leo's views because Leo likes one-off projects, and writing a small paper saying "this compiles with Lean commit X and mathlib commit Y" means Leo doesn't have to worry about breaking it]. The happy medium which I think we're currently trying to seek is that Mario and his team continue to develop mathlib but (a) try extremely hard not to bother Leo with requests, even reasonable ones such as "please fix ^, it would take 2 minutes" and (b) don't complain when Leo breaks stuff.

#### Kevin Buzzard (Mar 12 2018 at 15:41):

On the other hand, if Lean 4 appears with a temporarily-shrunken core lib then I am almost sure that a bunch of people will immediately just add what has disappeared to mathlib and then there's every chance that they will edit it to make it what one might call "better". In my mind there is no doubt that Mario's opinion on how to write a mathematics library is an opinion well worth listening to and to be quite frank I suspect he knows more about this subject than Leo. Or, at least, one might argue that Mario knows how to write a library which mathematicians can use better than Leo does (although this is probably not a question Leo is even interested in).

#### Kevin Buzzard (Mar 12 2018 at 15:42):

But at some point the question "is Leo ready for mathlib yet?" will come around again. For example, on the day Lean 4 is released. Will he be?

#### Sebastian Ullrich (Mar 12 2018 at 17:08):

I believe the only reason the algebraic hierarchy is in the core lib right now is that it's used by the C++ implementation of norm_num. So yes, in Lean 4 it may actually be realistic to move it to mathlib because it should be possible to build a high-performance norm_num in Lean.

#### Simon Hudon (Mar 12 2018 at 19:21):

Regarding the planned change to decidability and ite, are we going to keep dite with access to the assumption that the condition is true / false?

#### Mario Carneiro (Mar 12 2018 at 23:00):

The changes to decidable and ite are the ones I am most dubious of. I do not think it would actually be better to define decidable as a bool plus a proof of b = tt <-> p, and the concerns that make this reasonable in Coq don't apply directly in lean (in particular because we don't use kernel computation as much). For ite, we already have cond, ite and dite and these three functions are needed regardless of any notations attached to them. But I don't see any obvious alternate way to interpret if h : p then t else e other than using dite, and anything that uses bool here will be too cumbersome. For the nondependent if p then t else e, it's not really a big deal if this is interpreted as cond or ite, but there should not be any relative performance penalty between the two in any case, and if there is this is a fault of the code generator not the functions.

#### Mario Carneiro (Mar 12 2018 at 23:02):

Note: if you want to write a decidable p program by defining a bool program and prove it is correct, you can do this by using decidable_of_iff (my_bool = tt <-> p) <proof> with essentially no performance penalty. There is no need to change the definition for this.

#### Simon Hudon (Mar 12 2018 at 23:04):

In this situation, I think we can identify two changes: ite taking a bool instead of a decidable proposition and decidable being redefined. I think regardless of the definition of decidable, we can keep if _ then _ else _ the same. In the non dependent case, I can see how a boolean condition would make the condition easier to rewrite.

#### Moses Schönfinkel (Mar 12 2018 at 23:18):

Coq is a lot more cumbersome in this regard. You end up writing something like if Z_lt_dec a b instead of if h : a < b; the later is naturally a lot more readable (where Z_lt_dec is unsurprisingly something like {a < b} + {~a < b} which is just Coq notation for sumbools). There is a weird notation-al dissonance between props and their "boolean" (decidable) alter-egos in Coq

#### Simon Hudon (Mar 12 2018 at 23:25):

Yeah that's true. It's a really cool thing about Lean. It seems like just writing an obvious program is so much easier and that way of defining if _ then _ else _ has something to do with it.

#### Moses Schönfinkel (Mar 12 2018 at 23:28):

Notation is just too important, regardless of the amount of bikeshedding blame ending up being bestowed upon those partaking in the discussion :P. (I guess Iverson would agree!)

#### Moses Schönfinkel (Mar 12 2018 at 23:29):

Which is twice as amusing because then what on Earth was he thinking with APL.

#### Simon Hudon (Mar 12 2018 at 23:30):

That's what I was about to ask. I only know Iverson from APL and APL is only an example of how to make a miserable mess of your syntax

#### Moses Schönfinkel (Mar 12 2018 at 23:33):

Well his Turing award lecture was named Notation as a tool of thought so one would think that he of all people would understand the importance.

#### Moses Schönfinkel (Mar 12 2018 at 23:33):

And then he goes on to explain what makes good notation with some very valid points.

#### Moses Schönfinkel (Mar 12 2018 at 23:34):

And then he proceeds to use APL to demonstrate those valid points and at this point everyone is like "are you serious?".

#### Simon Hudon (Mar 12 2018 at 23:34):

Interesting. I haven't read it. I'll have a look.

#### Simon Hudon (Mar 12 2018 at 23:35):

My reference for mathematical notation is Dijkstra and his idea of "letting the symbols do the work"

#### Moses Schönfinkel (Mar 12 2018 at 23:36):

I have mixed feelings about DIjkstra ^^.

#### Simon Hudon (Mar 12 2018 at 23:36):

He wrote a note on his notational choices in EWD 1300: https://www.cs.utexas.edu/users/EWD/index13xx.html

#### Moses Schönfinkel (Mar 12 2018 at 23:37):

Why am I not one bit surprised that it's hand-written. He would also write computer programs in English... argh! :)

#### Simon Hudon (Mar 12 2018 at 23:37):

Yeah you can take all his opinions as holy writ. What bothers you in his ideas?

:D

#### Simon Hudon (Mar 12 2018 at 23:37):

I love his handwriting :D

#### Moses Schönfinkel (Mar 12 2018 at 23:38):

It's more like his personality and actions not coinciding with what he actually says.

#### Moses Schönfinkel (Mar 12 2018 at 23:38):

For example "the humble programmer".

#### Moses Schönfinkel (Mar 12 2018 at 23:38):

Humility was probably his weakest point :P.

#### Simon Hudon (Mar 12 2018 at 23:39):

Haha! Yeah but the humility he speaks of in that is something he did: he did assume his problems were too hard to just approach head on so he worked on reducing their intellectual demands

#### Moses Schönfinkel (Mar 12 2018 at 23:43):

Have you seen his correspondence with Backus? For some reason my personal feelings towards Dijsktra make me like even his ideas less :(.

#### Simon Hudon (Mar 12 2018 at 23:43):

No, where can I find it?

#### Simon Hudon (Mar 12 2018 at 23:43):

By "his ideas" do you mean Backus?

#### Moses Schönfinkel (Mar 12 2018 at 23:44):

Nono, I mean Dijsktra.

#### Moses Schönfinkel (Mar 12 2018 at 23:44):

Backus would talk about functional programming and liberation from von-neumman architecture and thinking in bytes.

#### Moses Schönfinkel (Mar 12 2018 at 23:44):

And Dijstrka would unleash a flurry of what is difficult to describe :).

#### Moses Schönfinkel (Mar 12 2018 at 23:46):

It's a fairly long chain of replies tho, which makes me dislike Dijsktra from a really silly personal standpoint.

#### Moses Schönfinkel (Mar 12 2018 at 23:47):

Putting personal feelings aside tho, objectively Dijsktra was an excellent computer scientist.

#### Simon Hudon (Mar 12 2018 at 23:48):

That's interesting. I started off taking Dijkstra's word as holy gospel and followed his approach for my master's. It's been very enlightening for me to learn to disagree with him and to stop tearing down projects that I would not personally undertake

#### Simon Hudon (Mar 12 2018 at 23:50):

Specifically, I had to eventually dismiss his "Computer Science is no more about computers than astronomy is about telescopes" comment. Z3 is actually what led me there. Having fast computers makes such a difference in building large formal proofs. I had to rethink my views in the field

#### Moses Schönfinkel (Mar 12 2018 at 23:51):

I think we also often somehow disregard that there exist proofs that are "computational" in their nature, which the 4-colour theorem is a prime example of. I am guessing they arise when your "domain" is constrained but still colossal.

#### Moses Schönfinkel (Mar 12 2018 at 23:52):

But perhaps Kevin or Patrick would be of different opinion.

#### Simon Hudon (Mar 12 2018 at 23:54):

That kind of proof still bother me a bit. I think they are a valid certificate for their claim but I wonder if they limit the amount of insight that one can gain from reading it.

#### Moses Schönfinkel (Mar 12 2018 at 23:54):

Does an alternative that doesn't need to check <many> cases exist yet?

#### Kevin Buzzard (Mar 12 2018 at 23:58):

Nope, not as far as I know.

#### Kevin Buzzard (Mar 12 2018 at 23:59):

Although I think <many> went down from the original 2000 or so

#### Simon Hudon (Mar 12 2018 at 23:59):

Not that I know of. My point is that I'm hesitant to accept the computational nature of the proof. I'm not sure how useful that particular fact is but a proof that is inscrutable proves one fact but if the proof can show people how to do mathematics or computer science, it does so more to advance the field. Admittedly if the theorem is referenced all the time but the proof is uninteresting, it still moves the field forward

#### Kevin Buzzard (Mar 13 2018 at 00:00):

I don't know much about proofs which are computational in nature, the proofs I know are all about building elaborate structures.

#### Moses Schönfinkel (Mar 13 2018 at 00:00):

This particular theorem is super-interesting!

#### Simon Hudon (Mar 13 2018 at 00:00):

How enlightening was the proof for you?

Not one bit.

#### Simon Hudon (Mar 13 2018 at 00:02):

What is so interesting about the theorem?

#### Moses Schönfinkel (Mar 13 2018 at 00:04):

Its applications. People optimize compilers with it, people use it to cover areas with signal with it. It's a useful, therefore interesting??? theorem.

#### Moses Schönfinkel (Mar 13 2018 at 00:04):

It's not some claim about perfectoid spaces :P.

#### Simon Hudon (Mar 13 2018 at 00:05):

I was not aware of that. That's pretty cool :) Do you know how it helps with compilers?

#### Moses Schönfinkel (Mar 13 2018 at 00:05):

I think something to do with assigning variables to registers.

#### Moses Schönfinkel (Mar 13 2018 at 00:05):

To avoid spilling perhaps?

#### Moses Schönfinkel (Mar 13 2018 at 00:06):

@Simon Hudon At one point in the past Kevin told me he's not very fond of proofs that rely purely on human understanding of the world (such as commutativity of multiplication being explained "geometrically" by counting soldiers rows first / cols first and noting that their number doesn't change) - any observations in this regard?

#### Simon Hudon (Mar 13 2018 at 00:06):

That makes sense. I'm still not sure where the planarity of the graph intervenes though

#### Andrew Ashworth (Mar 13 2018 at 00:08):

the trouble is intuition will only get you so far, and that's why appeals to informal proofs like counting soldiers is not ideal

#### Moses Schönfinkel (Mar 13 2018 at 00:08):

That's a similar argument to Kevin's. I just wonder if you would accept "simple" proofs like that as proofs.

#### Moses Schönfinkel (Mar 13 2018 at 00:09):

Lean would of course not.

#### Simon Hudon (Mar 13 2018 at 00:09):

Interesting, yes I do. I don't like proofs by analogy, not in technical texts anyway. I have no problems with proofs that purely shuffle symbols around. But I like them to be arranged in way that is obvious so that most of the proof is of the sort "there is only one thing you can do now" with as little surprises as possible. To me, it boils down to this: do you want to impress your audience or do you want to teach them something beyond this particular fact.

#### Moses Schönfinkel (Mar 13 2018 at 00:10):

But it's still a proof... for a human, right?

#### Andrew Ashworth (Mar 13 2018 at 00:10):

i would prefer something that does both? a well written paper interspersed with reasoning and formal proof

#### Moses Schönfinkel (Mar 13 2018 at 00:12):

If I were to tell you that you can count soldiers from "either perspective" to get the same result, would you be convinced that this is the case for an arbitrary number of soldiers?

#### Moses Schönfinkel (Mar 13 2018 at 00:13):

How would one formulate this kind of proof in Lean?

#### Simon Hudon (Mar 13 2018 at 00:13):

But it's still a proof... for a human, right?

Yes exactly. So you should have a calc block that spans pages and pages even if it's valid. You're losing people's attention. On the other hand don't, for the sake of being intuitive, jump into the rabbit hole that is the breaking down of equivalences into mutual implication or the analysis of multiple cases. I like efficiency in (human) formal reasoning

#### Simon Hudon (Mar 13 2018 at 00:14):

How would one formulate this kind of proof in Lean?

I wouldn't even try but I'm curious about what you'd come up with

#### Moses Schönfinkel (Mar 13 2018 at 00:15):

I am not sure. In general, if I were to call this a "geometrical proof", how would one begin in a mechanized / formalized setting.

#### Simon Hudon (Mar 13 2018 at 00:17):

I would venture the opinion that it is impossible because its justification is not in any set of axiom but in an experience of space that is common to most humans.

#### Kevin Buzzard (Mar 13 2018 at 00:18):

I think the only proof of the "counting soldiers in a rectangle" which I can accept is induction on one of the sides. I was ranting about this in the finite sequences thread though -- I don't know whether the statement "partition X into m disjoint subobjects each of size d -> size of X is m*d" should be a theorem about finite sets, finsets or fintypes. In reality it's a theorem about objects in a rectangle

#### Simon Hudon (Mar 13 2018 at 00:18):

And it is a big weakness. It's a bit of stage magic: you make it appear like you solved the problem but the only criterion is that "people agree"

#### Moses Schönfinkel (Mar 13 2018 at 00:18):

Sounds very reasonable. Could one formulate a model of such intuitive understanding that would be consistent with our perception thereof? Like ZFC but... with more hand-waving :P.

#### Kevin Buzzard (Mar 13 2018 at 00:18):

and I think it's a bit weird that one theorem in maths / reality threatens to become three in Lean.

#### Moses Schönfinkel (Mar 13 2018 at 00:19):

Right. But that's what proofs are, by definition. "People agree."

Not any more.

#### Kevin Buzzard (Mar 13 2018 at 00:20):

Not in mathematics.

It's not?

Oh, nice.

#### Kevin Buzzard (Mar 13 2018 at 00:20):

I think it's going too fast. That's why I'm here.

#### Kevin Buzzard (Mar 13 2018 at 00:20):

I think what is commonly accepted as a proof in mathematics is "the experts look at the techniques and figure that they should be enough"

Ufffff...

#### Kevin Buzzard (Mar 13 2018 at 00:21):

and then the rest of the people just say "well the experts seem to believe it"

#### Simon Hudon (Mar 13 2018 at 00:21):

I would venture the opinion that it's moving towards "people agree on a fixed number of rules and once they agreed, you have to decide whether the rules have been followed"

#### Moses Schönfinkel (Mar 13 2018 at 00:21):

That doesn't sound reassuring.

#### Kevin Buzzard (Mar 13 2018 at 00:22):

Patrick goes on about Scholze. But the number of people who have read all of his recent work is probably 0 (other than Scholze) now, because he's been branching out a bit. On the other hand, he has form, and some people have checked some of his stuff very carefully

#### Kevin Buzzard (Mar 13 2018 at 00:22):

so there's a certain amount of trust involved.

#### Kevin Buzzard (Mar 13 2018 at 00:22):

But he is not perfect even though he's a genius, and this is what makes me scared.

#### Kevin Buzzard (Mar 13 2018 at 00:23):

because mathematics is being done at a ludicrously quick rate at the minute, with it being so easy to knock up a pdf and stick it on ArXiv

#### Moses Schönfinkel (Mar 13 2018 at 00:26):

Of course there's "perfectoid space" on Scholze's wiki page.

#### Moses Schönfinkel (Mar 13 2018 at 00:27):

So I guess you guys are, and this is a terminus technicus, "in a pickle".

#### Moses Schönfinkel (Mar 13 2018 at 00:27):

Checking proofs is apparently hard.

#### Kevin Buzzard (Mar 13 2018 at 00:28):

Well, I think that people don't think we are in a pickle.

#### Kevin Buzzard (Mar 13 2018 at 00:28):

and I am kind-of concerned that we might find out too late that some important thing was wrong and then everyone will have egg on their face.

#### Mario Carneiro (Mar 13 2018 at 00:28):

Here's my kind of formalization of soldiers-in-a-rectangle proof of commutativity:

• Why should we believe that counting from one direction or another should give the same number?
• because it's the same soldiers
• But why should counting the same soldiers in a different order give the same number?
• Because that's what we mean by the "same number" (alternatively, you can push on this intuition but I will stick to conventional cardinality)
• But how do we know we aren't double counting or something? That would clearly mess up the count
• Because we are sweeping from one side to another in the count in some definite order, which prevents a double count

At this point, I see the formal proof clearly: it is a bijection between fin m x fin n and itself that counts lexicographically in two different ways

#### Kevin Buzzard (Mar 13 2018 at 00:30):

On the other hand I am open to the opinion that I am just getting old. I am happy that FLT is proved but then again I had time to read the proof (I was a post-doc and it was in my area so I had to read it). But ever since then I've felt less and less convinced that people have been checking all the details of absolutely everything, however perhaps I'm just more paranoid and slower now.

#### Kevin Buzzard (Mar 13 2018 at 00:32):

Meh but when you write down the bijection between fin m x fin n and fin (m x n) ... oh no you're right, you don't seem to need induction!

#### Kevin Buzzard (Mar 13 2018 at 00:32):

But now you have to prove that if fin x and fin y are in bijective correspondence then x=y.

#### Kevin Buzzard (Mar 13 2018 at 00:33):

Mario's proof is the categorification proof. Don't prove a * b = b * a in nat, prove A x B bijects with B x A in the category of sets.

#### Simon Hudon (Mar 13 2018 at 00:34):

I'm just more paranoid and slower now.

That sounds like a good thing to have in an audience. If the smartest of the smart are the ones reviewing the FLT proof, what will be left of that understanding once those people will have died? Will you need people dedicated to learning and understanding that particular proof and transmitting that understanding from generation to generation?

#### Moses Schönfinkel (Mar 13 2018 at 00:43):

Remember Fermat had a beautiful proof that just barely didn't fit the margin in his notebook or what was it ;). Surely we can easily understand 17th century mathematics!

#### Simon Hudon (Mar 13 2018 at 00:44):

I think that's mathematician code for "... and then magic happens ..."

#### Moses Schönfinkel (Mar 13 2018 at 00:45):

What sounds better is: Magician's code for "... and then mathematics happens ...".

#### Moses Schönfinkel (Mar 13 2018 at 00:47):

Oh man, I'll be getting like 4 hours of sleep. Yey... off to bed, nite.

#### Mario Carneiro (Mar 13 2018 at 00:47):

But now you have to prove that if fin x and fin y are in bijective correspondence then x=y.
Mario's proof is the categorification proof. Don't prove a * b = b * a in nat, prove A x B bijects with B x A in the category of sets.

The goal with that proof was to try to establish what formal proof underlies the confidence in the result given from the "geometric proof" of this theorem. But most of this is actually just pinning down what we mean when we say things. When I say there are 10 soldiers in a line, what does that mean? I guess I should be able to count up 10 times while naming the soldiers, but then 10 is defined in terms of itself which isn't good. Perhaps we have some internal conception of 10 as a number, and then we map this internal representation onto the soldiers; in that case it looks like we're talking about bijecting our set A of soldiers with fin n where n : nat is our abstract conception of numbers.

So where is fin n = fin m -> n = m hiding? I would argue it is in the intuitive notion that there are a well defined number of soldiers in the line in the first place, which is generally unchallenged. One may worry at this point that this is an empirical fact, that it just so happens that in our universe every time we count the same thing twice we get the same number (which obviously is false for a variety of reasons like miscounting), but we can push the theorem back to the platonic realm by counting our own abstract numbers, i.e. forming a bijection {1,...,n}->{1,...,m} and showing that always n=m in this case.

#### Moses Schönfinkel (Mar 13 2018 at 00:50):

^ This follows the "intuitive" notion of how cardinality is extended beyond finite. Just form a bijection with something nice (such as natural numbers) and then put your faith in the nice set.

#### Moses Schönfinkel (Mar 13 2018 at 00:51):

I really need to sleep. Bai.

#### Sean Leather (Mar 13 2018 at 07:12):

Some questions on the design notes:

if-then-else using bool instead of Prop. As soon as we started programming with Lean (version 3), it became clear that if-then-else with Prop creates more problems that it solves.

Can anyone elaborate on the problems created?

The elaborator already has support for a coercion from Prop to bool (for decidable propositions). The dependent if H : p then t else e may look cute, but it is unnecessary now that we have match.

Doesn't the “now that we have match” statement apply equally well to the non-dependent if-then-else? Stated another way: why would you want if-then-else for non-dependent propositions if you don't want if-then-else for dependent propositions? (I'm not arguing one way or another, just trying to understand the logic.)

#### Simon Hudon (Mar 13 2018 at 17:51):

I'm worried about those statements too. I wouldn't want to see those two if-then-else- disappear. More worrisome still is the introduction of match in the expression language. In Coq, they tend to make expressions larger than necessary. I really like that we're using auxiliary definitions instead

#### Sebastian Ullrich (Mar 13 2018 at 17:52):

Uh? There is no planned change to match.

#### Simon Hudon (Mar 13 2018 at 18:00):

Glad to hear it! So what does Leo mean what he says those things?

#### Joe Hendrix (Mar 13 2018 at 22:51):

In the "SSA or SIL" question in the design notes referring to LLVM IR vis Swift IL?

#### Mario Carneiro (Mar 13 2018 at 22:52):

SIL indeed stands for swift IL, SSA is static single assignment form in general. I think LLVM is off the table now

#### Simon Hudon (Mar 13 2018 at 23:03):

I think LLVM is off the table now

Yes? What disqualified it?

#### Mario Carneiro (Mar 13 2018 at 23:09):

It's very complicated with its own gotchas, and it's unlikely to produce better results than just having our own IL

#### Mario Carneiro (Mar 13 2018 at 23:10):

Leo works with Nuno Lopes, who has done formalization of LLVM and I think is the source of this view

#### Simon Hudon (Mar 13 2018 at 23:11):

That's interesting. I thought having that kind of formalization might be a good reason to use it

#### Mario Carneiro (Mar 13 2018 at 23:12):

I think it's more like once you've formalized a big language you know all the little suboptimalities in it. Like how I now have a better understanding of lean's theory to see why non-transitive definitional equality is a problem

#### Mario Carneiro (Mar 13 2018 at 23:14):

plus we're not talking a formalization in a proof assistant, I think it comes in the form of papers and compiler optimization checking tools

#### Simon Hudon (Mar 13 2018 at 23:24):

Ah ok. I thought you were talking of someone from the Vellvm project

#### Joe Hendrix (Mar 13 2018 at 23:31):

If you target Swift IL, then you are implicitly saying that you are fine with LLVM IR since SIL is translated to LLVM.

#### Mario Carneiro (Mar 13 2018 at 23:32):

I think it's just being used for inspiration

#### Joe Hendrix (Mar 13 2018 at 23:51):

GHC's compilation is essentially "System F core -> STG -> Cmm -> (native | LLVM)". I would expect a similar flow would work well for Lean.

#### Simon Hudon (Mar 14 2018 at 00:13):

@jhx Do you think it will be problematic to use Haskell techniques in Lean even though Lean is strict by default?

#### Joe Hendrix (Mar 14 2018 at 07:35):

It's true. I could imagine Lean maps a system F like core directly to a low-level Cmm representation. My understanding is that STG is provides a uniform closure representation and is where strictness analysis is performed prior to Cmm generation.

#### Johannes Hölzl (Mar 14 2018 at 08:10):

Glad to hear it! So what does Leo mean what he says those things?

Leo didn't write to get rid of match, in the (unpolished) document he writes that dependent if-then-else(dite) is not necessary anymore due to having match now. But I hope that we can implement if h : p then a else b with the parser in Lean4 ourself.

#### Mario Carneiro (Mar 14 2018 at 08:12):

I don't understand that comment either. AFAIK lean has had match since lean 1, what's new?

#### Johannes Hölzl (Mar 14 2018 at 08:25):

My guess is that in later Lean versions match got improved support for the dependent case? But I also don't see how match should replace the dependent if case. The later also includes the construction of the decidable predicate.

#### Joe Hendrix (Mar 14 2018 at 16:30):

Assuming the decidable changes are implemented, should the h in if h : p then a else b syntax ensure h has type p (resp. not p)? That syntax would then hide the underlying representation choice.

Last updated: May 11 2021 at 22:14 UTC