Zulip Chat Archive

Stream: general

Topic: lean4


view this post on Zulip 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?

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 16:29):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Mar 10 2018 at 16:42):

This looks really good :)

view this post on Zulip 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

view this post on Zulip Simon Hudon (Mar 10 2018 at 16:42):

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

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 16:43):

and that's just one of many big problems

view this post on Zulip Patrick Massot (Mar 10 2018 at 16:44):

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

view this post on Zulip Patrick Massot (Mar 10 2018 at 16:44):

It was strange to see it in core

view this post on Zulip Patrick Massot (Mar 10 2018 at 16:45):

And it currently prevent us from changing anything there

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 16:46):

it also means Leo is punting on redoing the algebraic hierarchy

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 16:49):

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

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 16:53):

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

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 16:55):

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

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 16:56):

I did expect someone in here to find it soon enough

view this post on Zulip Patrick Massot (Mar 10 2018 at 16:56):

Was it different when going from Lean2 to Lean3?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 10 2018 at 16:59):

Would I see any difference then?

view this post on Zulip Patrick Massot (Mar 10 2018 at 16:59):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 10 2018 at 17:02):

More math automation?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 17:13):

Is any time frame known for Lean 4?

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 17:14):

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

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 17:18):

No, we'll probably start on Monday

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 17:18):

:)

view this post on Zulip Patrick Massot (Mar 10 2018 at 17:19):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 10 2018 at 17:20):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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?

view this post on Zulip Andrew Ashworth (Mar 10 2018 at 17:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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! :)

view this post on Zulip Mario Carneiro (Mar 10 2018 at 19:59):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 12 2018 at 14:44):

And we can still use Lean 3 in the mean time

view this post on Zulip 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

view this post on Zulip 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" :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:29):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?".

view this post on Zulip Simon Hudon (Mar 12 2018 at 23:34):

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

view this post on Zulip 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"

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:36):

I have mixed feelings about DIjkstra ^^.

view this post on Zulip 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

view this post on Zulip 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! :)

view this post on Zulip Simon Hudon (Mar 12 2018 at 23:37):

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

view this post on Zulip Simon Hudon (Mar 12 2018 at 23:37):

:D

view this post on Zulip Simon Hudon (Mar 12 2018 at 23:37):

I love his handwriting :D

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:38):

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

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:38):

For example "the humble programmer".

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:38):

Humility was probably his weakest point :P.

view this post on Zulip 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

view this post on Zulip 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 :(.

view this post on Zulip Simon Hudon (Mar 12 2018 at 23:43):

No, where can I find it?

view this post on Zulip Simon Hudon (Mar 12 2018 at 23:43):

By "his ideas" do you mean Backus?

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:44):

Nono, I mean Dijsktra.

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:44):

https://medium.com/@acidflask/this-guys-arrogance-takes-your-breath-away-5b903624ca5f

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:44):

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

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:47):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:52):

But perhaps Kevin or Patrick would be of different opinion.

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 23:54):

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

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 23:58):

Nope, not as far as I know.

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 23:59):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:00):

This particular theorem is super-interesting!

view this post on Zulip Simon Hudon (Mar 13 2018 at 00:00):

How enlightening was the proof for you?

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:01):

Not one bit.

view this post on Zulip Simon Hudon (Mar 13 2018 at 00:02):

What is so interesting about the theorem?

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:04):

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

view this post on Zulip 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?

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:05):

I think something to do with assigning variables to registers.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:05):

To avoid spilling perhaps?

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Mar 13 2018 at 00:06):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:09):

Lean would of course not.

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:10):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:13):

How would one formulate this kind of proof in Lean?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:19):

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

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 00:20):

Not any more.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 00:20):

Not in mathematics.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:20):

It's not?

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:20):

Oh, nice.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 00:20):

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

view this post on Zulip 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"

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:20):

Ufffff...

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 00:21):

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

view this post on Zulip 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"

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:21):

That doesn't sound reassuring.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 00:22):

so there's a certain amount of trust involved.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:26):

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

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:27):

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

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:27):

Checking proofs is apparently hard.

view this post on Zulip Kevin Buzzard (Mar 13 2018 at 00:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Simon Hudon (Mar 13 2018 at 00:44):

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

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:45):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Moses Schönfinkel (Mar 13 2018 at 00:51):

I really need to sleep. Bai.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Mar 13 2018 at 17:52):

Uh? There is no planned change to match.

view this post on Zulip Simon Hudon (Mar 13 2018 at 18:00):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Simon Hudon (Mar 13 2018 at 23:03):

I think LLVM is off the table now

Yes? What disqualified it?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Mar 13 2018 at 23:24):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 13 2018 at 23:32):

I think it's just being used for inspiration

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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