Conor Mc Bride: intro

Stream: new members

[Conor Mc Bride]

Is this where new people say hello?

[suhr]

Yes.

[suhr]

By the way (pardon my blunt question), what brings a famous Agda enjoyer here?

[Shreyas Srinivas]

Yeah this is the right place

[Conor Mc Bride]

Curiosity, mostly. I see pros and cons in all sorts of systems, and am always looking for new directions.

[Kevin Buzzard]

@Freek Wiedijk once emphasized to me how much he sees the cons in all the available proof assistants. He'd love to use one but basically I got the impression that he hated all of them (but for each one he had a bespoke specific reason for hating it, it wasn't just annoyance with the area in general, it seemed to be that each one was problematic for him in a different way)

[Conor Mc Bride]

Sounds about right. Of course one should retain the capacity for (and habit of) critical thinking, even if one's engagement verges on enthusiasm. I am always on the lookout for obstructions to articulacy which prevent the merely systematic from becoming a system. Most proof assistants have plenty.

[Freek Wiedijk]

(Hi Conor!) "How much he sees the cons" sounds too strong, but yes, I'm a difficult person. I would like to "commit" to one system (like Kevin has to Lean 4, and I expect Conor has to Agda?), but I haven't been able to thus far. Which I hate, I like to have a vehicle for formal proof that makes me happy and that I know well. As Kevin also mentions, I love formalizing in any system, despites the various little irritations.

So let me try to analyse why I haven't been jumping on the Lean bandwagon yet, despite a strong feeling that it is the right thing for me to do. For one thing, installing it has been a turn off... but with some help I think I'm past that now, despite the fact that I still feel it's an impolite system, putting junk in all kinds of places.

But my two real issues are that I haven't bought into the way typeclasses are organised in mathlib. I have been watching @Michail Karatarakis work on something, and then there were two questions for which I don't see the "right" approach yet. One was whether some number that occurred in the proof should be in nat or in int (excuse me, I guess those actually were some unicode blackboard-bold symbols instead of these identifiers). I hate having to decide between that, it seems like it should be a non-issue to me. And the other was the way in which elements of the ring of integers of a number field related to the elements of the field itself. There were silly up-arrows in the terms. Again, I hate that kind of thing. (Really, I think these were the same issues.)

The other issue is that I don't know whether there is anything like "meson" or "metis" in Lean to not have to think about simple first order proofs, and also whether there is a "hammer" on top of this like in Isabelle. I can imagine that there is co-pilot that provides something like that, but having Sledgehammer is so nice in Isabelle...

And finally, not a real issue, but a matter of taste: in Isabelle/Isar one has "structured proofs", which I like better than tactic proofs. In Lean one can have those too, but I don't think it is used much, and I wonder why.

[Conor Mc Bride]

I'm not at all committed to Agda, although it has been my workhorse of late. I use my own rather sketchy proof assistant, ask, with my first years, and we use Agda with the fourth years, but me and my gang are always experimenting with prototypes which push beyond what the "production" systems currently support. My role is thinking about technologies, rather than whole systems, and trying to be a persuader for progress in the systems people already use. I suspect I have had some influence on Lean already.

[Freek Wiedijk]

I wish I could be like that. But I'm always a spectator/critic on the side lines, as @Kevin Buzzard observed. I hate that, but it's difficult to be different. For a while I really was into Mizar, but that has faded...

[Conor Mc Bride]

I really like Mizar's declarative take on proof. I kind of headed that way with ask, which has quite different presentations for things you prove and things you define. My major criticism of proof assistants based on dependent type theory is that in fifty years, we have (with a few honourable exceptions, none of which have cut through) thought no harder about normalisation of open terms than how to get stuck when a free variable gums up the machinery. We have been turning up to an algebra fight armed only with arithmetic.

[Freek Wiedijk]

But is normalisation for proof terms important too? My take on that is that proof terms are really like machine code for programming, it should be invisible/irrelevant to the user. And I love the fact that in Lean proof irrelevance is hard-wired in. When playing with Lean that felt so liberating! I still had the hidden worry about difference between proof terms causing trouble, and letting go of that worry was heaven.

[Conor Mc Bride]

Normalisation for proofs of mere propositions is not remotely important, except as one means to argue consistency. Definitional proof irrelevance is a delight when it's available. One should be mindful of when it's not, but one should not give it up lightly when it is.

[Freek Wiedijk]

Of course in Lean it causes trouble with subject reduction/normalisation/transitivity of definitional equality. But for me those are not the kind of "cons in proof assistants" that @Kevin Buzzard was talking about. As long as the system is consistent and I can nicely express my proofs, I'm happy.

[suhr]

And finally, not a real issue, but a matter of taste: in Isabelle/Isar one has "structured proofs", which I like better than tactic proofs. In Lean one can have those too, but I don't think it is used much, and I wonder why.

By the way, this is a strong reason to prefer Lean over Coq.

But is normalisation for proof terms important too?

A guided reduction of proofs would be very welcome. I even made a topic askin for it: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Controlled.20reduction.20of.20proofs

[suhr]

Using a proof assistant without guided reduction is like having a symbolic simplifier but not being able to use it.

[Kevin Buzzard]

Regarding structured proofs: my impression is that this might be part of some kind of culture clash here. Lean's maths library mathlib is full of tens of thousands of proofs and the vast majority are completely mathematically trivial; in particular the details of how they are proved are of absolutely no interest to me, they are just there because the mathlib community has understood that making a really solid and general API has lots of great advantages. And sometimes I speak to computer scientists and they start going on about forward proofs and backward proofs and structured proofs and proofs with lots of have statements in and readability etc etc and ask for my opinions, and my honest answer is that I have no opinions and I find the entire question completely boring and irrelevant because who cares in practice about the details of how the proof is implemented? The details have nothing to teach anybody. They are forgotten by the system after the proof is processed, the mathematical content is almost certainly at a trivial level (this is becoming less true but it's still true that the vast majority of statements in mathlib are statements which are completely standard and well-known to mathematicians). I am still quite bewildered by why it even matters what proofs look like. If you want to see a readable proof or a proof in your favourite style then just go and read a regular book. Right now the problem is that mathlib is still proving theorems which were known 100 years ago or which are completely trivial. The objective is to get the job done.

[suhr]

Are these standard proofs obvious to undergraduates too? Could they easily reproduce one themself?

[Freek Wiedijk]

This maybe is also an artifact of the lack of meson/metis/sledgehammer I was complaining about. The idea is that you only want to write the steps as they are meaningful to you, and let the "trivial level" be handled by the automation. But you are right, that currently the proof scripts are "proof irrelevant" on a human level too.

Still, as a user, with declarative/structured proof I feel more in control. At least, that's how it was when I switched from Coq to Mizar twenty-five years ago. Instead of searching for the appropriate tactic, it's searching for the appropriate statement that corresponds to the next step in the proof.

It would be very interesting to confront how you feel about this with what Larry Paulson has to say about this. Maybe if the "99 theorems" workshop ever happens, we can have a panel discussion about this? :grinning_face_with_smiling_eyes:

It's a bit like saying that in computer programming, once you have implemented something, what the code looks like doesn't matter anymore. I'm sure not all programmers will agree to that!

[Conor Mc Bride]

I find "guided reduction" a contradiction in terms. I want a clear distinction between what machines can do for humans and what humans must do for themselves, together with the means for humans to explain how whole classes of task can be mechanized. I want computers to compute! In every (highly non-vacuous) system I've ever implemented with definitional proof irrelevance, I've ensured that proof reduction is entirely unnecessary (at least for proof checking).

[suhr]

I don't want to expand definitions manually and would like to ask a computer to do it and see the result.

[Conor Mc Bride]

In the fundamental "is peg same shape as hole?" problem, I would like computers to compute without me having to ask them. Some things should just work, without being kicked. Addition is associative.

[Freek Wiedijk]

I think my (too strong) sense of aesthetics gets into the way of buying into @Kevin Buzzard's "just get things done" attitude. Yes, that's how you get somewhere. But I don't want to get somewhere, I just want to be in a place that I like. So, my complaint about having to choose between nat and int (sorry, I still don't know how to type unicode here :blush:) is of the same nature, I'm sure.

It's like the discussion about whether zero is a natural number or not. One attitude about that is "who cares?" With Humpty Dumpty, you can define natural numbers any way you like. But I feel strongly that having zero be a natural number is the "right" thing to have.

[Conor Mc Bride]

Working, as I do, on the thirteenth (numbered from one) floor of a Glasgow office block, I have been known to point out the window and shout "COUNT THE FISH!".

[Freek Wiedijk]

In the C committee mailing list there recently has been a huge discussion about whether a[17] should be called the 17th or the 18th element of the array :blush:

(I forgot the actual number, if you look up the mail discussion, replace 17 by what was talked about if you like.)

[Conor Mc Bride]

17 will do just fine. I was only saying to my students, the other day, "Mathematicians, especially those of us who work with computers, count like ZERO, ONE, TWO, WHY AM I DOING THIS?"

[Freek Wiedijk]

Oh my god, I'm jealous! I would love to be on a thirteenth floor! (Malkovich, Malkovich :blush:)

[Edward van de Meent]

"count the fish"???

[Freek Wiedijk]

Thm 4.2.7: The number of polar bears at an italian funeral is always even :blush:

[Edward van de Meent]

:huh: <- for some reason, the emoji "huh"

[Conor Mc Bride]

It was the twelfth floor when I started, but we were expensively renumbered. Around about the same time, Health Scotland started a campaign to persuade people to take the stairs instead of the lift, with signs that said "If you walk to here every day instead of taking the lift you'll have climbed N munros." (A munro is a hill in Scotland at least 3000 feet high.) Quite apart from it being pedantically a blatant untruth, because the whole point of munros is that the feet are connected spatially and in vertical sequence, the signs had very big digital representations of N and were intended as floor indicators. Thus, for us, the N=1 sign was placed on the ground floor, recently renumbered 1. I remember thinking "This is exactly the sort of off-by-one error which was bound to happen." as I unilaterally moved all the posters up one floor, thus attracting some frankly innumerate graffiti to which I was politely but lethally scathing in return.

[Freek Wiedijk]

0: Naming things
1: Cache invalidation
2: Off-by-one errors

(Sorry, for the silly jokes, please ignore.)

[Conor Mc Bride]

Quite the reverse. And from the same people who brought you...

There are three things which go wrong in a packet-switching network:
\3. Packets arriving in the wrong order.
\2. Packets being duplicated.
\2. Packets being duplicated.

[Freek Wiedijk]

I just reread @Kevin Buzzard's original comment that drew me in to this discussion: it's not just that I would love to use a proof assistant, I actually do love to use each and every proof assistant. Formalising is one the best things in life, even with all the "ifs" and "buts".

[Conor Mc Bride]

Right! And when we're grumpy, it's with the motivation of making good things better.

[Ruben Van de Velde]

I don't know what a structured proof is, so maybe that's why I don't miss it :)

[Ruben Van de Velde]

I do think we could put more effort in making proofs easier to follow, but somehow mathlib hasn't made that a priority

[suhr]

Mathlib proofs are semi-structured (there's have, suffices, blocks and even some type annotations), so you indeed don't miss it. It could be better (see Isabelle/HOL) but also could be much worse (see Coq).

[suhr]

A comparison of styles:

• Isabelle/HOL proof style: https://www.isa-afp.org/sessions/padic_ints/#Padic_Integers
• Mathlib proof style: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/NumberTheory/Multiplicity.lean
• Coq proof style (without SSReflect): https://github.com/thery/coqprime/blob/master/src/Coqprime/PrimalityTest/Lagrange.v

[suhr]

Coq with SSReflect allows to achieve the state of the art of proof unreadability. Which is impressive, since Coq proofs are already unreadable.

[Conor Mc Bride]

which is ironic, given Microsoft's key role in the obscurity of SSReflect. Sometimes ghastly hacks are the best you can do because you're not allowed to improve the machinery.

[Kevin Buzzard]

It's a bit like saying that in computer programming, once you have implemented something, what the code looks like doesn't matter anymore. I'm sure not all programmers will agree to that!

But I don't think that it is like that. This is a proof, not a program. People who think these are the same thing have been brainwashed. Proofs are run once and then literally forgotten, they are erased at runtime (disclaimer: I have no idea what that phrase means or what runtime is, I just heard someone else say it and I learnt it by heart). The way mathematics works is that you can use other people's theorems and you don't need to care about how the proofs worked or even whether they were 10 lines or 10000 lines; such issues have literally 0 effect on your work. This is very different to using someone else's function, where you might care a lot about what happens if e.g. you input a 10000-digit number.

[suhr]

In other words, everything that is already proven is trivial. Yet for some reason textbooks contain proofs of already known things.

[Ruben Van de Velde]

Mm, I think there's ideas of "clean" or "well-structured" programs that go further than the kind of concerns you're referring to here, Kevin

[Kevin Buzzard]

The question is whether one wants to learn from the proofs (which is the role of a textbook) or just use the proofs (which is case for me when I am writing Lean code which uses other people's work). Similarly I am not expecting other people to learn anything from the Lean code I write in the FLT proof. The only thing I require from that code is that it is easy to maintain as Lean and mathlib move on. If people want to learn what I am doing in the proof of FLT I'm formalizing, they should read the blueprint. This is a human-readable document intended to teach the mathematical ideas which I am formalizing. The Lean code is playing an entirely different role.

[Kevin Buzzard]

Computer scientists have said to me "are you formalizing FLT because you think it's wrong?" and my response is "absolutely not: I'm formalizing it because I know it's right". Mathematicians will learn nothing nontrivial from my work and I don't expect them to. All of the mathematical ideas are already in the references and are well-understood by experts. My motivation is to expand mathlib in the direction of modern number theory and thus get the library closer to modern research. The internal structure of the proofs is hence of no relevance to me.

[Conor Mc Bride]

Proofs and programs may be made of the same stuff, but they are not, either culturally or psychologically, the same thing. For a start, there is the huge difference between arguing that a type is inhabited at all and selecting from amongst the variety of a type's inhabitants.

I can understand the motivation to reduce the gap between the formalised canon and the canon by any means available. But it is also worth looking back at what was too much like hard work, especially for the early stuff that one imagines should be "trivial", in order to make the means available more effective in future.

I seldom think that individuals who use the word "trivial" not in quotation have spent enough time thinking about what that word might mean in practice.

[suhr]

Lean code has two advantages over static text: it is complete (no details are missing), and navigable (you can do "go to definition" as far as you wish). It is not a bad source for learning if proofs are readable.

[Kevin Buzzard]

Yeah I am using trivial in the arrogant way that mathematicians use it (i.e. anything they understand is now trivial because they have now forgotten what their brain felt like when they didn't understand it).

[Kevin Buzzard]

I am not convinced that the current mathlib design philosophy aligns at all with this idea that you should be able to learn why a theorem is true from its proof in mathlib. Right now the philosophy seems to be "crush the theorem in as few characters as possible and hang readability, because this thing is going to be compiled hundreds of times per day and we want to save electricity. Just worry about maintainability."

[suhr]

But since Mathlib proofs do not look like Coq proofs but look like something between Coq and Isabelle/HOL, there's some convergence between readability and maintainability. Which could be developed further.

[Conor Mc Bride]

Yes, this is the arrogant way in which mathematicians use "trivial". As an Irish person who interacted with that community and ran away, and as a person hugely squicked by overly masculine modes of doing business, I can only beg "Could youse not?".

[Kevin Buzzard]

[Conor trigger warning: arrogant usage of trivial occurs several times in this post]

I think also that the policy might be in need of an overhaul. It was impressed on me in the 2010s that everything in the library was trivial and hence the proofs did not need to be readable because there was nothing to read; everything was either (a) obvious or (b) fighting with dependent type theory. But back then everything in mathlib was obvious: it contained no theorems which weren't in a standard undergraduate mathematics degree and most of the theorems were of an even more trivial nature (e.g. hundreds of lines of stuff like "two subgroups which are equal as subsets are equal as subgroups" or whatever, which would not even be stated in a mathematics course because the statement is completely vacuous mathematically; most mathematicians would have their trouble even putting their finger on what needs to be said here, because their concept of a subgroup is more fluid than formal).

However things have moved on since then. For example we have got a bunch of graduate level algebraic geometry now, and some of the proofs are not at all trivial. In my mathlib work on topologies on modules (which is original research in the sense that I don't know a reference, although it is completely trivial in another sense (i.e. I understand it and moreover any mathematician worth their salt would be able to work out the details themselves)) I have been liberally commenting the proofs so that they are human-readable, but this is really because I cannot refer the reader to a textbook and I don't want to put them through the chore of having to figure out the proofs themselves when I've already done this work for them (or, in many cases, copied the proofs from Will Sawin's answer in the associated mathoverflow post ). But I didn't think "how best to write this Lean code", I just wrote the Lean code in the standard impenetrable style, and then wrote the comments afterwards to explain what was happening.

[Conor Mc Bride]

Thank you for the warning. Show me the comments. Today's comments are tomorrow's programs, when I get to work.

[Kevin Buzzard]

I should warn you that the file I linked to with the comments is very much the exception rather than the rule around here, and as I say I was only motivated to do this because that file is just developing some theory for which the community could find no reference in the dead tree literature.

[Conor Mc Bride]

It's a huge thing for me. What do people say to each other that they can't (yet) say to the machines? I have only to hang out to get fuel.

[Michael Rothgang]

suhr said:

Lean code has two advantages over static text: it is complete (no details are missing), and navigable (you can do "go to definition" as far as you wish). It is not a bad source for learning if proofs are readable.

I think that medium-term, an automated informaliser is a much more readable way of browsing mathlib proofs. There is a current prototype at https://kmill.github.io/ (scroll down to "informalisation).

[Ruben Van de Velde]

I'm looking forward to that a lot, but I imagine that would benefit even more from having more structure in the proof itself (though mathlib often tends to structure proofs by splitting out lemmas)

[Sébastien Gouëzel]

Let me say that we do not all agree with Kevin here. For me, proof readability is important both for maintainability and adaptability: if you want to prove a new result whose proof has similarities to the proof of a result already in mathlib, there is a much higher chance you can reuse and adapt this proof if it has been written with the reader in mind, not only the machine. And having nicely written proofs is also much nicer to your reviewer!

[Anh Nguyễn]

Hello

[Anh Nguyễn]

Am I allowed to ask questions here?

[Huỳnh Trần Khanh]

go ahead

[Matt Diamond]

@Anh Nguyễn You should start your own thread if your questions are unrelated to the conversation above

[Notification Bot]

3 messages were moved from this topic to #new members > can lean express any kind of mathematics? by Matt Diamond.

[Freek Wiedijk]

I see I missed a lot of discussion. As for @Kevin Buzzard's "once it's proved, it's done", isn't keeping the library working when the system changes an issue here? Or when there's a lemma that can be "improved", shouldn't one adapt the proof to that too?

[Ruben Van de Velde]

1. yes, that's an issue, though Kevin also mentioned it above ("that it is easy to maintain as Lean and mathlib move on"). We do have some requirements and linters on code within mathlib, at least (e.g. non-terminal uses of simp must use simp only, so newly added simp lemmas can't be applied unexpectedly, and when a tactic creates multiple goals, we require the use of the focusing dot to see where each subgoal should be fixed), as well as a deprecation system to help libraries downstream of mathlib. Also, in mathlib, whoever breaks a proof also has to fix it, so that helps :)
2. "should" - maybe not, but certainly "could". That tends to be relatively low priority though, unless there's a specific reason to go back to touch an existing proof

[Freek Wiedijk]

So I'm not saying declarative proof is "better" in any sense, just that I preferred it in the past myself. De gustibus non est disputandum, I guess.