Zulip Chat Archive

Stream: maths

Topic: ICM talk


Kevin Buzzard (Dec 01 2021 at 23:07):

I finally wrote an ICM talk. It's here. The deadline to get it to the organisers is...erm (checks notes)...was... 1st October, so if anyone has comments could they get back to me by around...erm...8th December? If people want to encourage me to write some more I still have some pages spare, but I didn't want to go on for too long. I tried to give a lot of people a mention, which was probably an unwise idea but there we go. If there's anyone I forgot who did a cute thing which made it into mathlib then let me know and I'll squeeze them in somehow, I'm sure I'll have forgotten someone. I have no doubt been characteristically slap-dash with my history, I will try to get some experts to read the sections which I'm least sure about...

Alex J. Best (Dec 02 2021 at 00:17):

Wow nice article Kevin :smile:
Some comments:

  • I feel like their is a weird emphasis on "pure" mathematics, why not just say mathematics throughout, certainly your running example of nonabelian Iwasawa theory and other examples are to show that you aren't talking about numerical analysis, and what we are doing here seems to encompass a wide spectrum of mathematical reasoning (is probability "pure" maths?)
  • Likewise I wouldn't personally say its breakthroughs in "Theoretical" computer science that have recently pushed the domain of proofs assistants forward, just computer science in general, theoretical computer science is quite a bit more mathematical than actually designing proof assistants. But maybe you have something more specific in mind?
  • formally the four colour conjecture -> formerly the four colour conjecture :grinning:?
  • The adjective loopless in the statement of the four colour theorem seems a bit redundant
  • The sentence "if one is embarking on a gigantic formalisation project, one has to decide how to internally store the data one is going to be manipulating, and this is where the computer scientists come in; they are experts in practical data management" makes it sound a lot like the choice of embedding all groups into a common parent is a choice only to manage memory somehow, rather than a way to avoid treating multiple possible group actions on the same type (Ok tbh I don't know the reasons here either, but the sentence doesn't give the right impression I think).
  • Massot developed a theory of cinompletions -> Massot developed a theory of completions
  • "As Carneiro once said, you can’t stop progress" is a great ender :grinning:

Scott Morrison (Dec 02 2021 at 00:30):

I'm not particularly convinced by the sentence "Note that here the computer was being used to compute, rather than to prove." regarding the 4CT.

It's true that it wasn't building a proof inside some formal system with a verifier. But as far as I understand in order to completely believe the Appel-Haken proof, one has to treat some of their programs as if they are tactics, being run in a world with only a human verifier. Thus either the human reader has to read the programs to see that they follow the intended behaviour, or one has the treat the output as a proof script that must be read. (In practice I understand that the former is intended.) In either case, I think this is more than merely computing.

Scott Morrison (Dec 02 2021 at 00:32):

Gonthier’s write-up “a computer-checked proof

needs a capital A.

Jeremy Avigad (Dec 02 2021 at 00:44):

It's a very nice article. I wonder whether it is a good idea to emphasize propositions as types and implications as functions? It makes it sound like there is something weird and dubious going on. You can equally well present it as nothing more than notation: function types and implications are written with the same arrows, and the same notation is used to apply a lemma to arguments, apply a lemma to hypotheses, and apply a function to arguments.

Jeremy Avigad (Dec 02 2021 at 01:05):

P.S. Regarding history, according to these notes (https://www.andrew.cmu.edu/user/avigad/Papers/pntnotes.pdf) the PNT formalization was completed on September 6, 2004. IIRC, Georges announced the verification of the four-color theorem a month or two after that, and Tom finished the Jordan curve theorem in early 2005. It was interesting that the three were clustered so closely together.

Scott Morrison (Dec 02 2021 at 02:01):

octonians --> octonions

Scott Morrison (Dec 02 2021 at 02:06):

When you state Mario's result about equivalence of the logical foundation, perhaps better to say "ZFC plus countably many inaccessible cardinals" rather than "ZFC plus countably many universes", which is mixing up languages.

Scott Morrison (Dec 02 2021 at 02:12):

The example in Section 3.5 makes me sad. Before you actually get to the proof you have to have this digression about division on natural numbers, and even the theorem statement is artificially awkward because of the coercion. This would be much more pleasant if you started with just the statement in nat, and only once you embark on the proof do you push things into rat. Even if this comes at the expense of an extra proof obligation that the division is the same, it seems better than to have your main example mainly about how horrible working with division of natural numbers is. :-(

Scott Morrison (Dec 02 2021 at 02:15):

If you want to stick with this example, then at least when you write "Thus we coerce", I think you could be clearer about what is going on. Maybe instead say explicitly: "Really, we'd like to just state this theorem about natural numbers, and even though division on the natural numbers is badly behaved, in this case it is actually fine. Nevertheless, in order to have to avoid even thinking about division in the natural numbers, we intentionally state a slightly different version of the result, in the rationals."

That is, if you're going to include an example that involves this issue, I think you should be explicitly sad about it, and be explicit that you are doing something artificial to avoid pain. Otherwise it is just confusing.

Johan Commelin (Dec 02 2021 at 02:41):

• on page 3: "putting together hundreds ... together"

Johan Commelin (Dec 02 2021 at 02:55):

From page 8: "Furthermore, we learn that the kinds of things which humans do when communicating with each other, such as identifying (G/H)/(K/H) with G/K when H ⊆ K are two normal subgroups of G (despite the fact that these groups are not actually equal from a foundational perspective), are no longer a problem."

I still find this very annoying in practice. So I would say it is still somewhat a "problem".

Johan Commelin (Dec 02 2021 at 03:21):

• When you talk about inductive eq, you mention the "induction principle", but in the general chat about inductive types you talk about the eliminator. Maybe add a "(the eliminator)" after "induction principle"?

Johan Commelin (Dec 02 2021 at 03:24):

Also, the eliminator is in fact for more general, right? You don't need an equivalence relation.

Johan Commelin (Dec 02 2021 at 03:33):

• In 4.1, "mathematical documents", maybe worth mentioning Alectryon? And Lamport's cascading proofs?

Johan Commelin (Dec 02 2021 at 03:39):

(• "Some computer scientists have argued that mathematicians are sloppy, and our literature has errors in". Some authors of this ICM paper have done the same thing in the past :rofl:)

Johan Commelin (Dec 02 2021 at 03:43):

• About the Mochizuki bit: "the proof must be clear on paper before it is possible to formalise in a theorem prover"
I don't think that's the issue. We figured out the proof of 9.4 along the way in LTE. It wasn't clear to me at all, before we started working on the formalisation.

I think the issue is that if you get stuck while formalising 3.12, then what? Is Lean stupid? Is the person formalising the proof stupid? Or is there a non-proof. The Mochizuki clan will simply say "you're stupid, and you should try harder".

Johan Commelin (Dec 02 2021 at 03:45):

• "Once these systems become easier for mathematicians to use, students can experiment for themselves with well-chosen examples supplied by a lecturer and begin to understand what is going on."

Isn't this already possible right now? I think that for these "learn how proofs works" type of applications, Lean should be more than ready to handle it.

Mario Carneiro (Dec 02 2021 at 03:54):

  • "most modern proof assistants have no problems with the law of the excluded middle, the axiom of choice, and other classical axioms."

I would replace "classical" -> "nonconstructive"; this use of "classical" is jargon which I don't think is used by most pure mathematicians

Mario Carneiro (Dec 02 2021 at 04:16):

"cinompletions" -> "completions"

Mario Carneiro (Dec 02 2021 at 04:27):

  • "The induction principle for equality, automatically added as an axiom to the system, is the assertion that if R is an equivalence relation on the type X and if R(a,a) is true for all a, and if a = b, then R(a,b) is true."

"equivalence relation" should be "predicate" or "relation" here. Of course we can't talk about equivalence relations yet since this is defining equality, and it's not what we want anyway.

Thomas Browning (Dec 02 2021 at 04:41):

Any reason for the 32 stars at the end of section 2?

Mario Carneiro (Dec 02 2021 at 04:50):

In 4.1, you talk about taking a proof and drilling down to the axioms. Although it might not be your cup of tea, I think the metamath web pages deserve a mention here because they are very good for this kind of thing. For a mathematician working at a high level they can feel long and verbose, but for someone who knows very little of the mathematics having a uniform way to display everything, even the advanced stuff, is great for being able to understand how everything holds together. Mathematicians know how to explain the forest, but metamath can explain the trees.

Patrick Massot (Dec 02 2021 at 15:25):

Thanks Kevin! I hope this will contribute to bring more mathematicians here. I think it would be nice to include some more citations to other proof assistants and maybe a couple of sample code. A rather cheap way to do this would be to replace all Lean code from Section 3.5 with Coq code (Section 3.2 would also be a natural candidate but unfortunately the recursor story is not exactly the same in Coq). You could also add citations at least to some foundational Coq paper (for instance when you write "Calculus of inductive constructions") and maybe also some Sledgehammer paper when you write "hammer". On Page 13, you need to remove my name in the "theory of manifolds" sentence, and add Sébastien's name in the calculus sentence. Also the exotic integrals take values in Banach spaces, not general topological vector spaces. I'll have some more minor remarks but I don't have time right now. I think the remarks above are the most important ones.

Patrick Massot (Dec 02 2021 at 15:38):

Maybe I should have written that the most urgent thing I think you should do after adding a bit more Coq and Isabelle is to send this to Assia Mahboubi and maybe Manuel Eberl and very politely ask them to help you removing as much factual inaccuracies as possible.

Anne Baanen (Dec 02 2021 at 15:45):

However, more recently two things have happened. [...] many modern proof assistants support “tactics”,

I had the impression that tactics have been quite widespread since the 1980's, at least in the LCF family (e.g. HOL). At least Edinburgh LCF had tactics in 1979.

Anatole Dedecker (Dec 02 2021 at 15:51):

In the section about types, I feel like it could be worth mentioning that you cannot prove a : X, so this is not just another notation for a ∈ X (but maybe this is not relevant).

Anne Baanen (Dec 02 2021 at 16:10):

In section 1.4 you mention that modern proof assistants have no issues with classical reasoning, and give Lean and Coq as examples. I would add the HOL family here, since their logic is explicitly classical in setup. (Potentially we could leave out Lean since its support for classical reasoning is essentially the same as Coq's, just that the communities have different tastes.)

Mario Carneiro (Dec 02 2021 at 16:11):

...also Mizar and Metamath. Really any system that isn't DTT or HoTT based takes LEM for granted

Riccardo Brasca (Dec 02 2021 at 16:24):

In 1.8 you could mention finiteness of the class group.

Anne Baanen (Dec 02 2021 at 16:26):

That formalization is already mentioned in the mathlib overview in section 2. I would not object to being mentioned twice of course :)

Patrick Massot (Dec 02 2021 at 16:26):

I also didn't get why you seem to imply that excluded middle is more builtin in Lean than in Coq.

Riccardo Brasca (Dec 02 2021 at 16:30):

Ah yes, sorry, I hadn't read section 2 yet.

Riccardo Brasca (Dec 02 2021 at 16:32):

I hope I hadn't missed it, but also the theory of Witt vectors, being notoriously intricate, could be a good example of what is doable nowadays in a proof assistant.

Kevin Buzzard (Dec 02 2021 at 16:34):

Many thanks for all these comments, which I've not yet had the chance to look at. I hope to get a version 1 written tomorrow.

Stuart Presnell (Dec 02 2021 at 16:56):

"Digitised and semantically searchable databases of mathematics are going to appear." Why is this phrased as a prediction for the next 10 years? Does mathlib not already qualify as such a database? Or am I misunderstanding what you mean by "semantically searchable"?

Riccardo Brasca (Dec 02 2021 at 16:58):

" Similarly the definitions of the rationals and integers are the same in type theory as in set theory." These are our dirty secrets, but the statement as it's written it's not accurate, right ? I am not suggesting to explain the definition of Z or Q in mathlib, but maybe saying something like "the definition can be the same" or something similar.

Stuart Presnell (Dec 02 2021 at 17:05):

"If you can get to the point where you are able to explain the statements of your own theorems to a computer proof assistant, then the database people can take it from there"
This suggests that merely formalising the statement of the theorem is the end of the mathematical input, and that formalising the proof then requires no further mathematical insight or understanding.

Stuart Presnell (Dec 02 2021 at 17:35):

Last sentence of Section 1.1: Many mathematicians imagine that formalisation of mathematics is exactly the kind of fiddly gritty chore that you describe at the start of this section — which is exactly why they haven't tried doing it! Perhaps better to say something like "Tactics allow formalised mathematics to more closely resemble ordinary mathematical practice by making "obvious" things automatic."

Jireh Loreaux (Dec 02 2021 at 17:38):

Mario Carneiro said:

  • "most modern proof assistants have no problems with the law of the excluded middle, the axiom of choice, and other classical axioms."

I would replace "classical" -> "nonconstructive"; this use of "classical" is jargon which I don't think is used by most pure mathematicians

For what it's worth, in my mind the jargon goes the other way (i.e., "nonconstructive" is somewhat jargon and "classical" is common parlance). Moreover, "classical" also evokes familiarity.

Mario Carneiro (Dec 02 2021 at 17:38):

Classical is a very overloaded word in mathematics

Stuart Presnell (Dec 02 2021 at 17:42):

"classical" just means any mathematics that doesn't use relativity or quantum mechanics, right?

Mario Carneiro (Dec 02 2021 at 17:42):

@Stuart Presnell I don't think it's necessary to sugarcoat things here - formalization is a fiddly gritty chore, as much as we would like it not to be. Things are changing, but it's still quite far from what most mathematicians would consider acceptable

Johan Commelin (Dec 02 2021 at 17:43):

@Jireh Loreaux "classical" means that you are doing algebraic geometry over an algebraically closed field, instead of over an arbitrary base scheme :rofl:
(At least that's what all the the people on my floor of the math dept think.)

Stuart Presnell (Dec 02 2021 at 17:48):

@Mario Carneiro Sure, there's still a lot of work to be done to close the gap between practice and formalisation (since we still don't have a left as an exercise for the reader tactic). I was just suggesting an expression of what tactics do for us.

Stuart Presnell (Dec 02 2021 at 18:01):

The argument is a very delicate argument -> The proof involves a very delicate argument ?

Rob Lewis (Dec 02 2021 at 18:45):

Nice writeup, Kevin. A few thoughts (I may be repeating what people already said, sorry):

  • The bit about "replacing one computer proof with another" about the 4ct proof read kind of funny to me. If someone  just learned what "formalization" means a section before, I don't think it helps to insist "no, you're missing the point, this one was formalized" without elaboration. It's maybe a point to insert something about small kernel, shifting the burden of trust from one ad hoc program to a small generic checkable thing, etc.
  • Mario could say more but I'm not sure the Metamath-Lean comparison is quite fair. As I understand it, there are "assistant"/tactic-like tools for producing MM proofs, right? The crazy strings of symbols are (sometimes) closer to proof terms than input-level tactic proofs? Lean proofs "need to be written from first principles" in the same sense that MM proofs do, if the translation happens at the foundational level and not the input level.
  • This was pointed out but the "constructive axioms built in" bit isn't fair. If you really have to compare Lean and Coq on this axis, the difference is in how the standard libraries for each make use of nonconstructive axioms.
  • Not to beg for citations, but since you explicitly call out norm_cast, there is a paper :) https://dblp.org/rec/conf/cade/LewisM20.html?view=bibtex
  • The reading of eq.rec is weird, I don't really follow.
  • You might want to use link shorteners for some of the web editor links. This way you could even keep them up to date if the code breaks with mathlib changes. 
  • I was surprised not to see a link to Patrick's document experimentation/sphere eversion after you described it.

Stuart Presnell (Dec 02 2021 at 20:05):

"Humans were well aware even back in the 1960s that the proof was correct"
I think this quite seriously underplays the problem of error and trust in published mathematics. I appreciate that perhaps you want to emphasise that the value of systems like Lean is not just checking the correctness of proofs (since this might be regarded as a small payoff for a lot of effort). But still, verifying correctness is an important contribution and shouldn't be too heavily downplayed. It's worth noting that the entire field of Homotopy Type Theory was, in part, motivated by not one but two separate erroneous proofs published by Voevodsky (who nevertheless was also awarded the Fields Medal). [Voevodsky (2014) The Origins and Motivations of Univalent Foundations]

Scott Morrison (Dec 02 2021 at 22:06):

My guess is that Kevin still agrees with the "correctness is an important contribution" line, but has realised that for better or worse it doesn't actually get much traction with many pure mathematicians.

Scott Morrison (Dec 02 2021 at 22:08):

For the purposes of pure maths research, I'm actually much more excited about the potential for "multi-level" proofs that formalisation brings. It's essential that on paper we give human level explanations, and give readers who don't want or need the gory detail a way to grok the big ideas. But too often people write explanations that are unnecessarily painful to expand into the careful detail when you want them. If we ever start writing proper literate proofs in Lean, we can solve this problem.

Stuart Presnell (Dec 02 2021 at 22:36):

Oh, absolutely, these other advantages should be emphasised. I'd love to see literate collapsible proofs that allow the reader to say "hold on, explain this step in more detail for me". I'm just noting that verified correctness shouldn't be tossed away as if it was an unimportant side-effect of formalisation, given that there are genuine examples of substantial errors in published papers by well established authors.

Kevin Buzzard (Dec 02 2021 at 22:50):

I haven't read through this thread yet; I will do so tomorrow. But I noticed Stuart's message pop up and indeed Scott is right: mathematicians get nothing but irked if you tell them that their system doesn't work and so instead I'm telling them what they want to hear. The point is that the system is 99.9% fail-safe and that has been enough for thousands of years. We don't need to get to 99.999% especially if it's a lot of work to get there. We want to hear other reasons to formalise. Computer scientists often come across as paranoid in this regard. Perhaps Voevodsky was also paranoid -- or perhaps he was careless. If you talk to people other than Voevodsky they seem to be well aware that his erroneous paper had an error in, many years before he accepted the idea. The system was working but Voevodsky gives a skewed impression in his talks.

Filippo A. E. Nuccio (Dec 02 2021 at 23:12):

Very nice paper, @Kevin Buzzard , congratulations! As minor comments, I have:

  • Why do you prefer the expression "nonabelian Iwasawa theory" to "noncommutative Iwasawa theory"?
  • On p. 11, after quoting Clausen-Scholze's, theorem 9.4 you have an extra parenthesis )
  • This is very personal, but on page 9 you say that computer scientists are expert in "practical data management" or something is "pratical from the point of view of the computer prover" and I feel that the sentence is a bit harsh to computer scientists.
  • I find Gouëzel's story of passing from Isabelle to Lean to formalise Gromov-Hausdorff inspiring, and a big result which might be missing from 1.8 (or section 2)
  • You mention in a footnote that the de Bruijn factor for the perfectoid space is well over 5: is it really so? You say it comprises 16000 lines, and I wonder if 3000 lines is not a reasonable estimate for all that is really needed to define a perfectoid space.
  • In 3.3 you sometimes write proposition and sometimes Proposition (with capital P): is that intended to hint at the existence of Prop?
  • In 3.6 why don't you write Zermelo--Frankel with a n-dash (you write, for instance, Hales–Ferguson)
  • In the title of our paper with Anne, Sander and Ashvni, Dedekind should replace dedekind.

David Renshaw (Dec 02 2021 at 23:18):

... this is where the computer scientists come in; they are experts in practical data management ...

Since others have commented on this sentence, I just wanted to say: I really liked this bit and found it to be resonant.

David Renshaw (Dec 02 2021 at 23:34):

I suppose it is something of a rhetorical flourish (a benign equivocation?), where the "data" in the first half of the sentence is not necessarily the same as the "data" that we typically associate with computer scientists. But in my opinion, the sentence totally makes sense, is memorable, and if anything is flattering to computer scientists.

Matthew Ballard (Dec 03 2021 at 00:26):

I think the paper does an excellent job of answering the titular questions. A couple of comments/suggestions:

  • If you are interested by reading the paper and want to explore further, where do you go? Just reading the intro and then references, it is hard to figure out where to learn more about Lean or another ITP. A footnote at

    once you know the language

    Saying something like:
    If you want to learn the Lean language a good place to start is \href{https://leanprover-community.github.io/index.html}{https://leanprover-community.github.io/index.html}
    would catch the majority of people. Leaving in the url would make sure people know where to go in the case that the pdf is stripped of hyperlinks via some reprocessing back into pdf or to paper.

  • Interested but overextended mathematician? Find a CS inclined student. Teach them math and have them learn and then teach you Lean by formalizing some of that math. Beats having them read a paper and then write a paper showing they understood the original paper.

Matthew Ballard (Dec 03 2021 at 00:28):

If you can solve the problem of figuring out good honors math thesis topics, that is definitely something done for the working mathematician.

Mario Carneiro (Dec 03 2021 at 02:07):

Rob Lewis said:

  • Mario could say more but I'm not sure the Metamath-Lean comparison is quite fair. As I understand it, there are "assistant"/tactic-like tools for producing MM proofs, right? The crazy strings of symbols are (sometimes) closer to proof terms than input-level tactic proofs? Lean proofs "need to be written from first principles" in the same sense that MM proofs do, if the translation happens at the foundational level and not the input level.

Yes, this is a bit inaccurate and I thought about saying something. While I started to write more tacticky things toward the end, for the vast majority of my time writing metamath proofs the level of automation was essentially equivalent to refine + show + library_search. This is very far from nothing; in particular unification is absolutely essential for being able to produce those something like those line-by-line proofs without a huge amount of copy-paste. The main tactics that I use often in lean that would have been significantly more painful in metamath are simp, norm_num, ring, linarith (and I actually ended up writing norm_num for metamath).

Mario Carneiro (Dec 03 2021 at 02:10):

Filippo A. E. Nuccio said:

  • You mention in a footnote that the de Bruijn factor for the perfectoid space is well over 5: is it really so? You say it comprises 16000 lines, and I wonder if 3000 lines is not a reasonable estimate for all that is really needed to define a perfectoid space.

I thought that was poking fun at the fact that "let X be a perfectoid space" is a lot less than 16000 lines.

Filippo A. E. Nuccio (Dec 03 2021 at 06:02):

Oh, I certainly missed that one: thanks!

Filippo A. E. Nuccio (Dec 04 2021 at 11:05):

I actually have one minor remark on the "types don't mix" section (3.1). When trying to explain to colleagues this point, I got the impression that a more useful example is the fact that R0\mathbb{R}_{\geq 0} and R\mathbb{R} are different types, and so that " a non-negative real number is not a real number". The problem with N\mathbb{N} vs Z\mathbb{Z} vs Q\mathbb{Q} etc... is that every mathematician agrees that they are "truly different sets" and that we put arrows under the rug in common mathematics. So they don't see a theoretical difference, just a lot of pedantry. But with nonnegative reals, things are somewhat different: satisfying a property does not interfere with membership, so I feel this example better serves the goal of explaining that types and sets are different. The same holds when saying that sin ⁣:RR\sin\colon\mathbb{R}\to\mathbb{R} and sin ⁣:R[1,1]\sin\colon\mathbb{R}\to[-1,1] are different in type theory, but seen as subsets of R×[0,1]R×R\mathbb{R}\times [0,1]\subseteq\mathbb{R}\times\mathbb{R} they are equal (or "more equal" at any rate).

Kevin Buzzard (Dec 04 2021 at 11:06):

I'm about to sit down and read all of the above comments and revise the article -- thanks a lot for this comment!

Junyan Xu (Dec 04 2021 at 14:59):

Filippo A. E. Nuccio said:

R0\mathbb{R}_{\geq 0} and R\mathbb{R} are different types

and that's why we ever need to assign a value to r/0 ...

Yury G. Kudryashov (Dec 05 2021 at 06:48):

I'd mention https://topology.pi-base.org/ in Sec. 4.2

Patrick Massot (Dec 07 2021 at 09:38):

Here is the full review I promised. I understand that this is still your paper and your style, so feel free to ignore anything you don't like in the little liste below.

The paper is full of http links which are completely useless on paper. I think you can turn them in regular \cite with links in the bibliography. When read on a computer this means only one extra click. Also there are links to Lean web editors that I didn't check. Did you make sure they link to a frozen Lean web editor with frozen mathlib so that you won't have to maintain them? Ask for help to setup this if needed.

Page 1

In the abstract and many other places, including the third paragraph of the introduction, I would add "and communicate mathematics" to "prove theorems".

I wouldn't start in the first paragraph with such a controversial statement as "Mathematics is a game with precise rules". Generally I don't think we need to claim anything about the nature of mathematics. It's enough to discuss the way we communicate mathematics.

Page 2

"The technology to make such tools is already available" (this comes back several times). I think this is an exageration. I understand what you mean, but many people make a living of trying to bring us this technology and wouldn't be happy to read this. Maybe you could soften it to: "The technology to make such tools is already coming".

Paragraph 3, the first time you mention Lean you can already mention Coq and Isabelle, maybe after "If you can get...". Then I don't know whether "database people" is a good terminology. I understand you need to be vague here, but there is a risk people think about SQL. Maybe "data scientists" would be better? That's the vague word we use all the time in France. It would allow to also fix the issue that you start mentioning AI only a couple of sentences later while we know it is needed even for a searchable database. We don't want exact match for statements, there are too many variations in ways to express any given definition and result.

In the last sentence of that paragraph, I would again soften a bit your "formalisation is mathematics re-interpreted as a computer puzzle game", maybe including "can be seen as". But I understand this kind of sentence is very much part of your style and its efficiency so feel free to ignore such suggestions.

As I already told you, I think you can expand on the digitised music analogy. Deezer and similar stuff didn't not only reduce storage requirements. I'm not using these things for young people, but my understanding is they fundamentally changed the way modern artist communicate with their fans, essentially bypassing the traditional editorial and advertisement process. I hope that formalized mathematics will also fundamentally improve communication and accessibility of maths. Johan also mentioned that new animated movies do things that were completely impossible in the hand-drawn era.

Page 3

The discussion of tactics is a bit weird. It sounds like tactics are much more recent that they are. This comes back on Page 5 in "In the final 15 years...". I think you should check this. Maybe also cite a SSReflect paper and a Isar paper (Isar is the new style of Isabelle proof script that Isabelle people like so much).
And that third paragraph misses an extremely important point: one key new ingredient is the growth of the community of mathematicians using a proof assistant.

Second to last paragraph is a good place for the canonical Lean citation (from CADE 25 in 2015), and also for the mathlib paper.

Page 5, in the paragraph before Section 1.2, are you sure the ring tactic is called the same in Isabelle/HOL?

Page 6, in the description of the 4 colours formalisation, is there actually any topology involved? You may be right but this is suprising to me.

Page 7, do you really want to keep that "odd" word, even with quotation marks? Why not adding half a sentence here and be less controversial?

Page 8, Section 1.4 it would be nice to \cite the formalisation paper from the beginning. At the end of the first paragraph, I think you're missing and important point. A lot of time in the odd order project was spent developping SSReflect (which began with the four colours proof). And also figuring out how to handle such large scale projects.

Page 9, end of second paragraph, I already wrote this but let me repeat that LEM is not more builtin Lean than in Coq. The difference is the library (and people, but that's roughly the same thing).

Page 10, about Hales original paper. I think even the Annals published a disclaimer about this proof. But you should check.

Page 11, first sentence of Section 1.7 reads weird. Surely analytic geometry have been using homological algebra at least since Cartan. I know what you mean of course, but some readers will be puzzled. At the end of this paragraph, the parenthetical remark seems to have some grammatical issues. In the last paragraph, I'd like to mention I also contributed non-trivial proofs to that project, I don't understand why you want the team to be made only of algebraic number theorists and arithmetic geometers.

Page 12

Section 1.8, I would add the Poincaré-Bendixon formalisation, noting the usual proof very much relies on drawings. Maybe also Assia's work on numerical integrals and Manuel's word on analytic number theory. Also note that Isabelle formalized manifolds.

In the next paragraph, note we are not formalizing Smale's proof. We are formalizing a much more general theorem that has Smale's result as a corollary. The last sentence about schemes reads weird since you explained earlier schemes we done very early.

First paragraph of section 2, don't forget to mention mathlib is monolithic and consistent (in the sense you can mix all parts). Otherwise its size is not so impressive.

Page 13

About Galois theory, isn't there a paper you can cite? Also mention somewhere the Coq formalisation. When mentioning manifolds, remove my name. Add Sébastien's name for calculus and maybe write that calculus include implicit function theorem and Picard-Lindelöf. About cateogry theory I would add Adam's name. When describing my work, you may add "adic topology, valuation theory".
Why is there no name for "over time flat and projective..."?
Integrals is for function taking values in Banach spaces, not topological vector spaces.
I would remove footnote 7 and the "pull request" terminology and write "Contributions are reviewed...". Pull request is a very specific GitHub term.

Page 14

Section 3, I feel this lacks a general explanation of why set theory is not a good foundation (or at least not a good user interface). Maybe cite Stacks tag 0009 somewhere around here. Second paragraph of Section 3.1: you can't claim notation is the only difference between set theory and type theory...

Page 15

"In ZFC set theory, the existence..." is this litteraly true?

Page 16

Are you aware that this story is one of the differences between Lean and Coq? In Coq inductive types give rise to a fixpoint operation, not a recursor. You should probably check with Mario.

Section 3.3: is the first paragraph the begining of an explanation that was abandonned?

Page 17

Right before Section 3.5, the jump from dependant type as a way to handle ∀ x, P x to sheaves is really weird and probably very hard to understand.

At the end of this page, I would mention that the convention for ℕ is the one used in civilized countries. And I don't think that calling finset.range like this is a "computer science convention".

Page 18

As other wrote, I think confronting nat division and coercions is not a good choice.

Page 19

I really think that you mention Fields medals and Annals of maths way too many times in this essay. It really sounds like formalized maths is for people who like prizes and h-factors.

Section 3.6 feels weirdly positionned. Also, does it miss a paragraph where you wanted to mention universes in Lean? It feels like this section ends too soon.

Page 20

plasTeX has no leading P.

Page 21

I think you should cite a sledgehammer paper when mentioning hammers.

Section 4.3

You can't seriously keep that first sentence when there are so many videos of Youtube showing you explaining maths is full of errors and this is a problem.

At the very end of paper, I would soften the sentence saying the proof must be clear on paper before formalisation. LTE wasn't clear to Johan when he started.

Page 22

I would soften the last sentence before Section 4.4 a lot if you want to keep good relations with Peter.

In Section 4.4, I wouldn't mind seeing Orsay being mentioned here.

Yury G. Kudryashov (Dec 07 2021 at 10:02):

About 4 color thm: here is the code that glues continuous statement to a combinatorial one. I haven't read it, so I don't know what happens there.

Yury G. Kudryashov (Dec 07 2021 at 10:08):

At the end of this page, I would mention that the convention for ℕ is the one used in civilized countries.

Note that the talk will be given in a country where 0 is not a natural number (at least, in school math). And if you want to say that it is not civilized, then 0 ∉ ℕ is not the best argument.

Patrick Massot (Dec 07 2021 at 10:42):

I'm pretty sure Kevin understood I'm not seriously suggesting he writes this is the civilized convention.

Arthur Paulino (Dec 07 2021 at 11:58):

About mathlib being monolithic, this can have bad connotation from a software engineering standpoint. The term is often used to refer to a piece of software that's hard to tweak and improve

Ruben Van de Velde (Dec 07 2021 at 12:10):

Maybe "well-integrated" or something along those lines?

Johan Commelin (Dec 07 2021 at 12:21):

@Arthur Paulino I agree, but I consider this one of the weird results of mathlib: we did what is "evil" from a CS pov, and built this giant monolith. But it seems to work, refactors happen, and cool things are built on top of it.

Johan Commelin (Dec 07 2021 at 12:21):

So calling it a monolith seems correct to me.

Matthew Ballard (Dec 07 2021 at 12:47):

Besides by the time of the ICM, monorepos will be back in style :wink:

Arthur Paulino (Dec 07 2021 at 12:52):

Johan Commelin said:

Arthur Paulino I agree, but I consider this one of the weird results of mathlib: we did what is "evil" from a CS pov, and built this giant monolith. But it seems to work, refactors happen, and cool things are built on top of it.

I agree and it's indeed a monolith. It's just that it doesn't sell well.

Arthur Paulino (Dec 07 2021 at 12:53):

About "database people", I'd say "data folks", which sounds more inclusive and friendly (at least to me). Or even "data/AI folks".

Patrick Massot (Dec 07 2021 at 12:54):

I really think Kevin shouldn't care about "bad connotation from a software engineering standpoint". He is not writing at all for people with a software engineering standpoint.

Yaël Dillies (Dec 07 2021 at 12:54):

One clear difference between maths and computer science is that the former has much deeper theories, by which I mean that the longest chain of statements/functions in maths is much bigger than in computer science.

Patrick Massot (Dec 07 2021 at 12:54):

It doesn't mean we should write stuff for these people, but that particular essay simply isn't targeting them.

Patrick Massot (Dec 07 2021 at 12:56):

And concerning the actual "issue" we have a very clear answer here: many people proved that the modular separate libraries scheme doesn't work for formalized math and we proved the monolithic approach works. This is not a theoretical discuss, only facts.

Patrick Massot (Dec 07 2021 at 12:58):

We will always see people coming from software engineering explaining they pity us and we should split mathlib, but we can simply continue to ignore them, at least as long as we are successful.

Yaël Dillies (Dec 07 2021 at 13:03):

What about Isabelle? They're kind of modular and although I wouldn't want to have to deal with several duplicate libraries, that seems to work.

Patrick Massot (Dec 07 2021 at 13:11):

No it doesn't

Patrick Massot (Dec 07 2021 at 13:11):

Topology and algebra are extremely difficult to mix because they made different technical decisions about infrastructure.

Yaël Dillies (Dec 07 2021 at 13:12):

Fair enough

Johan Commelin (Dec 07 2021 at 13:52):

At the same time, it's not clear to me that our current monorepo approach will scale to 100x the size. (Which is a lower bound on the endgoal I'm aiming for.) But we can solve that issue when it becomes a real problem.

Yaël Dillies (Dec 07 2021 at 13:54):

:wink: affinity refactor :wink:

Filippo A. E. Nuccio (Dec 07 2021 at 14:50):

Johan Commelin said:

At the same time, it's not clear to me that our current monorepo approach will scale to 100x the size. (Which is a lower bound on the endgoal I'm aiming for.) But we can solve that issue when it becomes a real problem.

Since I have been asked this a couple of times, can you speculate a bit on this? What are the problems you might foresee? More on the "human side" (having enough maintainers with enough time to review all PR or stuff like this) or more " practical" (CI would take two days to compile mathlib) or something else?

Arthur Paulino (Dec 07 2021 at 15:09):

I do think this subject would deserve a thread of its own, just to keep the focus on Kevin's paper

Kevin Buzzard (Dec 07 2021 at 15:10):

I've had tons of feedback on the paper (many thanks to eveyone!) and am currently trying to write v1 of the document. I'm quite happy for the conversation to wander, but the reason it should have a thread of its own is not because it could derail this one but because it will be easier to find later on.

Notification Bot (Dec 07 2021 at 15:28):

This topic was moved by Anne Baanen to #general > Is a monolithic mathlib sustainable?

Mario Carneiro (Dec 08 2021 at 12:09):

Patrick Massot said:

Page 15: "In ZFC set theory, the existence..." is this literally true?

For reference:

In ZFC set theory, the existence of the set of natural numbers is postulated as an axiom, namely the axiom of infinity. In type theory systems such as Lean’s, the so-called calculus of inductive constructions can be made to construct types. This means that one can define types “inductively”.

I think it is literally true, but in some ways presents a false distinction. In ZFC, the axiom of infinity is more or less the statement that the natural numbers exist. But it is important to note that you don't need an "axiom of reals" to prove that the real numbers exist, or the first uncountable ordinal, or other much larger sets. Which is to say, the axiom of infinity is all you need to get basically all the power of inductive types.

I think it is somewhat of a marketing gimmick to say that CIC has "inductive constructions", because inductive types aren't constructed at all: ZFC axiomatizes the existence of the natural numbers but CIC axiomatizes the existence of the natural numbers, the integers, the reals and tons of other things, and this is considered a good thing in type theory circles because being closer to the axioms means that you can hide implementation details.

Patrick Massot said:

Are you aware that this story is one of the differences between Lean and Coq? In Coq inductive types give rise to a fixpoint operation, not a recursor. You should probably check with Mario.

It is somewhat folklore that the two approaches (recursors vs fixpoint operations) are equivalent, but they present very differently, and so they encourage different ways to "bend the rules", leading to some foundational differences between Coq and Lean. As I mention in my thesis, doing something analogous to what I did for Lean in Coq is still an open problem, because the rules aren't an exact match. If you scale back a bit, though, I think there is definitely a subset of Coq that is bi-interpretable with Lean. I believe "Coq is a Lean typechecker" is a partial attempt at this (they had to fudge a lot of rules to make it work).

Kevin Buzzard (Dec 09 2021 at 22:08):

Within the next 12 hours I hope to have dealt with all these comments, but let me just flag a couple of issues.

1) People are saying "LEM is no more built in to Lean as it is to Coq". I don't understand this. LEM and the other classical axioms are explicitly present in core Lean. As far as I know this is not true in Coq. For me this is a big difference. I removed the comment anyway because if there is a difference of opinion then probably it should go.

2) The objection about natural division I simply do not buy, although I have removed the example anyway because of Scott's objection. When a mathematician has n : nat and writes n(n-1)/2, I absolutely claim that they mean n*(n-1)/2 : rat, because subtraction and division to a mathematican mean subtraction and division in a field. So I regard the coercion to rat as being a literal translation of what a mathematician is saying and I regard n*(n-1)/2 : nat as being mathematically meaningless, even though coincidentally (and it is only coincidentally) it gives the same answer in this case.

Yury G. Kudryashov (Dec 09 2021 at 22:11):

https://coq.inria.fr/library/Coq.Logic.Classical_Prop.html is in the core library

Kevin Buzzard (Dec 09 2021 at 22:12):

And AC?

Yury G. Kudryashov (Dec 09 2021 at 22:17):

A few forms of AC: https://coq.inria.fr/library/Coq.Logic.ChoiceFacts.html, see also https://github.com/coq/coq/wiki/CoqAndAxioms

Yury G. Kudryashov (Dec 09 2021 at 22:17):

Propositional extensionality and quotient types are built-in in Lean and are not built-in in Coq.

Mario Carneiro (Dec 09 2021 at 22:20):

The closest equivalent to our choice axiom is https://coq.inria.fr/library/Coq.Logic.IndefiniteDescription.html

Mario Carneiro (Dec 09 2021 at 22:21):

I couldn't find an exact match, but I believe this was the original form of classical.choice before the current one (a simplification I suggested)

Anatole Dedecker (Dec 09 2021 at 22:24):

Yury, did you mean proof irrelevance (rather than prop ext) or did I miss something ?

Mario Carneiro (Dec 09 2021 at 22:24):

Kevin Buzzard said:

So I regard the coercion to rat as being a literal translation of what a mathematician is saying and I regard n*(n-1)/2 : nat as being mathematically meaningless, even though coincidentally (and it is only coincidentally) it gives the same answer in this case.

I don't think it is a coincidence. It usually shows up explicitly as part of the proof, as if it was a side condition on writing the expression

Mario Carneiro (Dec 09 2021 at 22:26):

@Anatole Dedecker Propositional extensionality is in the core library of both Coq and Lean, like choice, but quotient types are built into lean and not Coq, and similarly for proof irrelevance.

Mario Carneiro (Dec 09 2021 at 22:27):

I don't think Coq even has a general definition of quotient type

Floris van Doorn (Dec 09 2021 at 22:28):

Since a couple years Coq also has a (definitionally) proof irrelevant version of Prop, called SProp: https://coq.inria.fr/refman/addendum/sprop.html

Eric Rodriguez (Dec 09 2021 at 22:29):

I feel like when mathematics students say n*(n-1)/2, they carry around a lot of implicit arguments in their head; I think their version of the ℕ division operator is "if (↑a/↑b) is a natural then that else throw a what the hell are you doing error". I think the closest Lean gets to this is something like division_by_monic, which is zero if q isn't monic. For a more extreme example take the product formula of the totient function; but in that case, I feel like it's more used "formally" to get back to an expression in terms of +/* as soon as possible. Maybe this changes higher up in academia, though.

edit: Zulip won't let me escape asterisks...

Floris van Doorn (Dec 09 2021 at 22:32):

I think the main difference between classicality of Coq and Lean is the attitude if its users, not the system or the availability of classical axioms.
Many Coq users try to avoid choice (and many other axioms like function extensionality) as much as they can, and often in papers of Coq formalizations there is a section on what parts do and do not use axioms (and the reason that axioms were necessary).

Though other libraries freely use choice throughout (e.g. math-comp analysis: https://github.com/math-comp/analysis/blob/27f0473aa958606ae2b954a1328a8e85c9fda5d5/theories/boolp.v#L25 )

Floris van Doorn (Dec 09 2021 at 22:32):

@Eric Rodriguez n*(n-1)/2?

Floris van Doorn (Dec 09 2021 at 22:35):

My experience with divisions aligns with Kevin's. You write something like n*(n-1)/2 (or something more complicated) and then at the bottom of the page you write "notice that n*(n-1)/2 is always integral"; the integralness is not considered a precondition for writing n*(n-1)/2

Mario Carneiro (Dec 09 2021 at 22:38):

er, now I'm confused. When you say n*(n-1)/2 in a summation limit or otherwise some position which requires it to be a natural number, that's a precondition on the expression to make sense. If you don't, then it's just a real number

Mario Carneiro (Dec 09 2021 at 22:42):

Why is that mathcomp file stating indefinite description and proving diaconescu's theorem if these are already in the core library?

Floris van Doorn (Dec 09 2021 at 22:43):

I am not sure how much math-comp (analysis) uses from the standard library. I think it redoes a lot of stuff (everything?)

Mario Carneiro (Dec 09 2021 at 22:43):

They don't seem to be the only coq library that does that kind of thing. I'm not sure how many Coq people even use the "standard library"

Mario Carneiro (Dec 09 2021 at 22:45):

I guess this means that you can't use the standard library and mathcomp simultaneously, since nothing is compatible

Floris van Doorn (Dec 09 2021 at 22:50):

Yeah, many Coq users never use the standard library. But there are also big libraries on top of the standard library. This is tricky for e.g. the Proof Ground competition (https://www21.in.tum.de/~wimmers/proofground/) which in past years only supported the Coq standard library, which is unfamiliar to many users. We had some discussion about providing both a standard library and math-comp version of the problems.

Floris van Doorn (Dec 09 2021 at 22:52):

For example, I believe that Coquelicot (http://coquelicot.saclay.inria.fr/) builds on top of the standard library. (except that it ignores the real numbers of the standard library) (edit: it seems like they use the real numbers of the standard library, but extend the theory)

Mario Carneiro (Dec 09 2021 at 22:53):

In this case, I think Kevin was closer to the truth in saying that LEM is more built in to Lean than Coq. Yes, it's in the standard library, but it's not that standard, and people often just use something else, so when working in a Coq development it may or may not be available

Mario Carneiro (Dec 09 2021 at 22:54):

Plus, if you use it, expect to have to defend your contentious choice in the paper

Filippo A. E. Nuccio (Dec 09 2021 at 22:59):

Kevin Buzzard said:

2) The objection about natural division I simply do not buy, although I have removed the example anyway because of Scott's objection. When a mathematician has n : nat and writes n(n-1)/2, I absolutely claim that they mean n*(n-1)/2 : rat, because subtraction and division to a mathematican mean subtraction and division in a field. So I regard the coercion to rat as being a literal translation of what a mathematician is saying and I regard n*(n-1)/2 : nat as being mathematically meaningless, even though coincidentally (and it is only coincidentally) it gives the same answer in this case.

I am probably being very naïf here, but I would say that when a mathematician has n : natand writes n(n-1)/2 they don't mean much: only once the question is asked they mean something (and then, I agree with you that they mean it is in rat). It is one of the wonderful (although pride-killing) benefit of working with Lean, that mathematicians got the question asked. I know that it sounds trivial, but putting this under the rug, on my opinion, is neglecting that Math is done by human beings and that changing the way humans interact with it is also part of making Math lands in the 21st century.

Mario Carneiro (Dec 09 2021 at 23:00):

I don't think they specifically mean it to be in rat though, any more than it is in real or complex

Filippo A. E. Nuccio (Dec 09 2021 at 23:02):

Well, this is getting somewhat personal (like: "what is an algebraically closed field of char 0"? gets the answers C\mathbb{C} or Qˉ\bar{\mathbb{Q}} according to taste); what I meant is that I agree with Kevin that every mathematician would, if asked, perceive both subtraction and division to take place in a field, and for economy it could be the smallest one doing the job (otherwise F3\mathbb{F}_3 is also a nice answer...)

Kevin Buzzard (Dec 09 2021 at 23:24):

Maybe I'm misunderstanding this LEM thing. It is literally impossible to use lean without having LEM available (unless you start your file with prelude). Is the same true in Coq?

Reid Barton (Dec 09 2021 at 23:45):

Mario Carneiro said:

er, now I'm confused. When you say n*(n-1)/2 in a summation limit or otherwise some position which requires it to be a natural number, that's a precondition on the expression to make sense. If you don't, then it's just a real number

It has to be a natural number because it is a sum of natural numbers, but it's by coincidence that Lean's interpretation of n*(n-1)/2 is the correct natural number. For example if I rewrote it as n*n/2 - n/2 then it is still the correct natural number, but even more by coincidence.

Reid Barton (Dec 09 2021 at 23:46):

If I wrote it as n*((n-1)/2) then it is the wrong natural number.

Reid Barton (Dec 09 2021 at 23:46):

In math all of these are equal.

Mario Carneiro (Dec 09 2021 at 23:50):

It is not by coincidence that a/b : nat in lean is defined to be the right answer if the right answer exists

Mario Carneiro (Dec 09 2021 at 23:50):

so (n*(n-1))/2 : nat works out correctly because 2 divides n*(n-1)

Mario Carneiro (Dec 09 2021 at 23:51):

all of the other examples are "coincidences"

Reid Barton (Dec 09 2021 at 23:51):

It's not always though, because the right answer might not be an integer

Mario Carneiro (Dec 09 2021 at 23:51):

If it's not an integer, then it evaluates to "garbage"

Reid Barton (Dec 09 2021 at 23:51):

It's only the final result that we know a priori is an integer (or natural number) but there might be intermediates to worry about as well

Mario Carneiro (Dec 09 2021 at 23:51):

or more precisely, the floor of the actual answer, which is often what you want in e.g. summation bounds

Reid Barton (Dec 09 2021 at 23:52):

It's kind of like how the result of a single floating-point operation is always rounded correctly (and so in particular is always exact if the correct result is precisely representable) but that property doesn't extend to larger expressions.

Yury G. Kudryashov (Dec 09 2021 at 23:53):

@Kevin Buzzard There are many levels of "built-in". E.g., (p : Prop) (a b : p) : a = b is built into the C++ code of Lean while classical.choice needs an axiom (though this axioms is in prelude and is used everywhere). For (some) computer scientists, only the first flavor of "built in" is truly built in.

Yury G. Kudryashov (Dec 09 2021 at 23:54):

(at least I this is my impression from some discussions)

Mario Carneiro (Dec 09 2021 at 23:54):

At least some of those "non-builtin" axioms are actually required by the C++ code though, for example simp makes explicit reference to propext

Mario Carneiro (Dec 09 2021 at 23:55):

the prelude is pretty tightly coupled to the lean C++ code

Yao Liu (Dec 10 2021 at 01:07):

It falls under the "things that are details that, if asked, Lean can provide". Another possibility (for implementation) is n*(n-1)/2 being a shorthand for {n choose 2} which is defined to be nat, say 1+2+...+n, but happens to have a rational expression in n.

Rob Lewis (Dec 10 2021 at 15:04):

Kevin Buzzard said:

Maybe I'm misunderstanding this LEM thing. It is literally impossible to use lean without having LEM available (unless you start your file with prelude). Is the same true in Coq?

Ignoring any debate about the technical meaning of "built in": there's a history of lots of people saying "Lean is better than Coq for classical reasoning," either erroneously or without real justification. It's not true that the Lean system is better at classical reasoning because choice is imported by default, where in Coq you need to add one import line. This is an immaterial difference. I know you didn't write that line as a value judgment but it will definitely be read as stoking the flames of this argument.

Johan Commelin (Dec 10 2021 at 15:16):

The differences are of a social kind.

Eric Wieser (Dec 10 2021 at 15:41):

As well as the social preference for / against choice, is the preference for Prop vs SProp also relevant to the abundance of classical mathematics in lean?

Eric Wieser (Dec 10 2021 at 15:43):

That is, something like:

  • no one case whether a Lean Prop(coq SProp) is proved classically, because you can't extract data from it anyway; lemmas are never noncomputable
  • coq has a culture / history of using Prop, which isn't proof irrelevant, and so noncomputability is meaningful on lemmas

(warning: I have never used Coq, this is speculation based on earlier conversation)

Dima Pasechnik (Dec 11 2021 at 10:01):

(deleted)

Dima Pasechnik (Dec 11 2021 at 10:01):

cf https://softwarefoundations.cis.upenn.edu/lf-current/Extraction.html

Dima Pasechnik (Dec 11 2021 at 10:04):

hmm, sorry, pressed wrong button. I was saying that LEM prevents program extraction, something Coq appears to do well, while Lean never had it released.
https://softwarefoundations.cis.upenn.edu/lf-current/Extraction.html

This might explain the difference in Coq vs Lean work we see.

Yury G. Kudryashov (Dec 11 2021 at 10:11):

LEM in proofs doesn't affect program extraction.

Sebastian Reichelt (Dec 11 2021 at 11:12):

Maybe propositions in Coq correspond to Decidable propositions in Lean? (At least if "program extraction" and "code generation" are the same thing -- and then Lean does have it.) (EDIT: I think that first sentence is actually blatantly wrong.)
I think it's quite telling that among all the aspects mentioned in the paper, this one gets so much attention.

Kevin Buzzard (Dec 11 2021 at 11:14):

Just to comment that in v1 of the paper (which I really hope to post before the builder arrives this afternoon) I remove claims that Lean's treatment of LEM is any different to Coq's, and I'll also remark that I will be saying very little about classical v constructive mathematics, because the audience of the paper is research mathematicians, for many of whom "mathematics" := classical mathematics and, like me (or at least like me pre 2017), will believe that constructivism rightfully died out in the 1930s.

Kevin Buzzard (Dec 11 2021 at 18:04):

ICMtalkv1.pdf

Main changes: If you commented above then I almost certainly changed the MS according to your comments. Section 1.8 (other results) now bigger and better-referenced. Propositions as types stuff now removed. Example involving n(n-1)/2 now removed. LEM stuff now hopefully much more accurate. More mathlib work mentioned in section 2. If there are people who feel that they merit a mention (because they formalised something mathsy which the audience will recognise as interesting or relevant) and who I didn't mention yet then feel free to DM me or flag the issue somehow.

Yaël Dillies (Dec 11 2021 at 18:08):

Section 1.8, Other results: "Argyraki, Edmonds and Paulson verified Szemeredi’s theorem in Isabelle/HOL"
Nope nope nope they didn't. We didn't either. Szemerédi's regularity lemma is far easier than Szemerédi's theorem.

Yaël Dillies (Dec 11 2021 at 18:10):

Also, both teams did pretty much the same stuff:

  • Us: Equitable Szemerédi's regularity lemma, Triangle counting lemma, Triangle removal lemma, Corners theorem, Roth's theorem on arithmetic progressions + some more random stuff like #10509 and #10645
  • Them: Szemerédi's regularity lemma, Triangle counting lemma, Triangle removal lemma, Roth's theorem on arithmetic progressions.

Kevin Buzzard (Dec 11 2021 at 18:16):

Thanks!

Yaël Dillies (Dec 11 2021 at 18:19):

"Szemerédi's regularity lemma and Roth's theorem on arithmetic progressions" is a fair summing up for both.

Johan Commelin (Dec 11 2021 at 18:25):

Nitpick:

However the system worked, and produced code which compiled; however it was of course also [...]

You use however twice in a row.

Rob Lewis (Dec 11 2021 at 18:31):

In type theory systems such as Lean’s, a system known as the calculus of inductive constructions [CP88] can be used to construct types.

"Calculus of inductive constructions" is the name for the particular flavor of dependent type theory that Lean and Coq implement. (Also plenty of non-CIC type theories allow inductive types.) Something like "Type theories such as Lean's allow the user to define custom inductive types" might be a better phrasing.

Johan Commelin (Dec 11 2021 at 18:33):

Typo:

used extensivel in

extensively

Rob Lewis (Dec 11 2021 at 18:36):

I'm still not quite sure why you bring up

A corollary is that if R is any binary relation satisfying ∀a, R(a, a) and if a = b, then we can deduce R(a, b).

in the type theory section. Is this example relevant later or something? Would it be more interesting (or just more confusing) to show how to derive symmetry from substitution?

Kevin Buzzard (Dec 11 2021 at 18:47):

oh I was just following what I did in my own blog post

Kevin Buzzard (Dec 11 2021 at 18:47):

substitution is a statement about types, the corollary is a prop

Kevin Buzzard (Dec 11 2021 at 18:48):

(at least in my head)

Kevin Buzzard (Dec 11 2021 at 18:48):

I think you're right that it's just easier to remove it though

Kevin Buzzard (Dec 11 2021 at 18:50):

I have always been fascinated and confused about type-valued v prop-valued recursors. When writing NNG I noticed that you needed the type-valued recursor to prove the props nat.succ_inj and nat.zero_ne_succ; the prop-valued recursor (induction) didn't seem to be enough.

Kevin Buzzard (Dec 11 2021 at 18:50):

Historically those two props are presented as axioms in the usual statements of Peano's axioms, but Lean deduces them from the recursor.

Johan Commelin (Dec 11 2021 at 18:55):

Nitpick:

The library is not designed for pedagogy or readability;

Would it make sense to write s/designed/optimised/?

Johan Commelin (Dec 11 2021 at 19:10):

aside (semi-off-topic):

apply theorems such as ↑(x+y)=↑x+↑y and ↑(x∗y)=↑x∗↑y automatically (before this tactic had been written, doing mathematics which involved switching between the naturals, integers and rationals could be quite frustrating [...]

Wow yes! It's good to occasionally remember that this used to be a major PITA. And now you don't even blink twice. Big kudos to the norm_cast authors.

Kevin Buzzard (Dec 11 2021 at 19:12):

Also thank @Chris Hughes for tirelessly working on basic number theory (every natural is sum of four squares etc) and discovering exactly where the pain points in 2018 were -- it was because of his experiences, at least to some extent (at least this is my memory of things), that we got norm_cast and ring

Johan Commelin (Dec 11 2021 at 19:16):

another nitpick:

defines schemes in Isabelle/HOL but which has to implement a new implementation

duplicates implement*

Johan Commelin (Dec 11 2021 at 19:17):

maybe build a new implementation?

Kevin Buzzard (Dec 11 2021 at 19:42):

Alex J. Best said:

  • "As Carneiro once said, you can’t stop progress" is a great ender :D

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Updating.20Mathlib/near/131243695

Sebastian Reichelt (Dec 11 2021 at 20:18):

Some random nitpicks:

If such a triviality hides 30 lines of axiomatic mathematics, imagine what is hidden behind claims of the form “The function ff is clearly O(x2)O(x^{-2}) for xx large”?

As "for xx large" is redundant in that statement (and thus should be omitted IMHO), I'm not convinced this is a particularly nasty claim.

I was surprised by the somewhat frequent use of the word "shock", in particular twice on page 7. But maybe I'm just not easily shocked.

Naively, it looks like in this case we are replacing one “proof by computer” with another one, however this is missing the point. ...

I second the view you are expressing in this paragraph, and I think the argument can be strengthened a bit. Anyone who spends just a bit of time with theorem provers will quickly notice that in order to formalize something, one already needs to have a correct proof in mind, and be able to fill in all necessary details if required. Even if the prover has a bug that compromises soundness, the existence of that bug doesn't actually change anything about the process of formalization. Or, in other words, to get a wrong proof accepted, you'd have a start with a wrong proof in the first place, one that's wrong in exactly the right way. ;-) And how would that even happen, except deliberately?

In the odd order formalisation, the de Bruijn factor (ratio of lines of computer code to lines of human text) was around 5. Here one could argue that it is 16000.

How could one argue that? (I guess it may be meant as a joke, but I don't really understand the joke then.)

In the section about the difference between set theory and type theory, I have a feeling that one particular aspect could be misinterpreted by people not used to type theory. You write "distinct types are disjoint" and then later give an example about positive reals, where an x:R0x : \mathbb{R}_{\geq 0} does not have type R\mathbb{R}. Before, you stress that the difference between :: and \in is mostly one of notation. In combination, the reader could wrongly conclude that something analogous to xRx \notin \mathbb{R} holds (and dismiss type theory as stupid).
I'm not sure how to avoid this, other than maybe to state explicitly that this would be exactly the wrong way of thinking about types.

... has to implement a new implementation ...

"has to reimplement ring theory from scratch" maybe?

FWIW, I'd like to suggest an additional item for "4. The Future". Formalization can motivate mathematical laypersons (like me...) to dabble in research-level mathematics. There are potentially two aspects to this. The first is that formalization helps test one's intuition; this is related to what you wrote about teaching. But in the future, I can also imagine laypersons (or also just mathematicians from a different field) formalizing their work in order to convince people of its correctness.
(This also works in reverse. "Oh, you think you have a proof of the Riemann Hypothesis? Very nice, please formalize it and get back to me.")

Kevin Buzzard (Dec 11 2021 at 20:22):

Many thanks!

I think it's dangerous to start suggesting "you have to formalise it before we believe it" will ever be a thing -- this is not how our culture works and I suspect it will never be how it works. I even explicitly suggest in the article that telling Mochizuki to formalise his proof is an unreasonable thing to do, even though part of me thinks it's a really good idea. David Roberts has convinced me in various blog posts and conversations that were Mochizuki to try and write down carefully in Lean some of the things he's talking about he might himself learn something about how to express his ideas more clearly.

Johan Commelin (Dec 11 2021 at 20:25):

Sebastian Reichelt said:

Some random nitpicks:

If such a triviality hides 30 lines of axiomatic mathematics, imagine what is hidden behind claims of the form “The function ff is clearly O(x2)O(x^{-2}) for xx large”?

As "for xx large" is redundant in that statement (and thus should be omitted IMHO), I'm not convinced this is a particularly nasty claim.

I think that it depends very much on the f in question. My interpretation of this sentence was that for rather innocent f, it might still be painful to verify the claim.

Kevin Buzzard (Dec 11 2021 at 20:25):

right -- can you formalise that 1/(1+x^2) is clearly O(x^{-2}) for x large without using any tactics, just using the axioms of a field?

Kevin Buzzard (Dec 11 2021 at 20:26):

Maybe I should change ff to 1/1+x3+x41/\sqrt{1+x^3+x^4} or something.

Johan Commelin (Dec 11 2021 at 20:30):

I think it's fine as it is

Sebastian Reichelt (Dec 11 2021 at 20:48):

I think it's dangerous to start suggesting "you have to formalise it before we believe it" will ever be a thing

Yes, that's not at all what I was suggesting though. (OK, except for the "Riemann Hypothesis" thing, which I said because supposedly some people are regular bothered by cranks.)

right -- can you formalise that 1/(1+x^2) is clearly O(x^{-2}) for x large without using any tactics

I can believe that it's difficult depending on ff. But reading with a non-Lean POV, my thoughts went something like: "OK, I guess 'for xx large' first needs to be made precise... Wait, it's actually redundant... Now what's so special about ff being O(x2)O(x^{-2})?"

Patrick Massot (Dec 11 2021 at 21:30):

I don't understand what you you find redundant in that "for xx large enough". Saying "f(x)f(x) is O(x2)O(x^{-2}) for xx large enough" and "f(x)f(x) is O(x2)O(x^{-2}) for xx close to zero" are very different statements. Maybe you would prefer "f(x)f(x) is O(x2)O(x^{-2}) when xx goes to infinity" or something like this?

Ruben Van de Velde (Dec 11 2021 at 21:55):

Formalising all the proofs in the [Stacks] database is not a feasible idea.

I found this statement somewhat surprising - is there something making it impossible besides that it'd be a lot of work? (Maybe I read more in the word "feasible" than was meant.)

Kevin Buzzard (Dec 11 2021 at 22:26):

It's not feasible in the following sense. Consider the collection of people who have the knowledge in algebraic geometry to do the job, and the lean skills. That's a group of around 20 people all of whom hang around on this Zulip. Now consider the amount of work it would be. Now where are those people going to find the time to do that work? Right now there is no infrastructure in place for paying us to do it and no compensation eg promotions or job offers at the end of it. Thus I'm arguing that in practice right now this is not a feasible proposal

Jörg Hanisch (Dec 11 2021 at 22:31):

Some typos "Accessed: 30-11-2011" in the references

Kevin Buzzard (Dec 11 2021 at 22:40):

Oops!

Julian Berman (Dec 11 2021 at 22:56):

I found this very approachable to read. The only minor comment I had whilst reading it (beyond some typos that it looks like were pointed out above) was that I found the sentence "Gouëzel observes that the HOL systems [etc.]" a bit out of place -- the rest of the section doesn't do much comparison with other theorem provers I believe.

Sebastian Reichelt (Dec 12 2021 at 01:06):

Patrick Massot said:

I don't understand what you you find redundant in that "for xx large enough". Saying "f(x)f(x) is O(x2)O(x^{-2}) for xx large enough" and "f(x)f(x) is O(x2)O(x^{-2}) for xx close to zero" are very different statements. Maybe you would prefer "f(x)f(x) is O(x2)O(x^{-2}) when xx goes to infinity" or something like this?

My bad, I automatically assumed the former because in computer science that's all that ever appears anywhere.

Jineon Baek (Dec 12 2021 at 01:58):

I enjoyed reading it - I always thought that an open library/database of known theorems is needed, but didn't know that it was planned and being worked on now. A typo: 'matheamtics' in page 23

Will Sawin (Dec 12 2021 at 02:23):

Kevin Buzzard said:

Maybe I should change ff to 1/1+x3+x41/\sqrt{1+x^3+x^4} or something.

Maybe 1/x411 / \sqrt{x^4-1} would be an example that's harder to prove step-by-step than 1/1+x3+x41/\sqrt{1+x^3+x^4}.

Mario Carneiro (Dec 12 2021 at 17:23):

Ruben Van de Velde said:

Formalising all the proofs in the [Stacks] database is not a feasible idea.

I found this statement somewhat surprising - is there something making it impossible besides that it'd be a lot of work? (Maybe I read more in the word "feasible" than was meant.)

I'm not sure whether you mean this in the "I'll eat my hat if" sense, but this does seem like one of the predictions of the paper that is least likely to age well. I can believe in a possible future where the Stacks project is mostly formalized within 5 years. Lots of things (in particular priorities) would have to change to make that possible, but nothing inconceivable from the present moment.

Kevin Buzzard (Dec 12 2021 at 17:56):

It's 7000 pages of advanced mathematics mario. The odd order theorem was 400 pages of relatively straightforward arguements in finite group theory and it took a team of 12 people 6 years

Kevin Buzzard (Dec 12 2021 at 17:57):

We can't train a random person to do the job because the material is complex

Adam Topaz (Dec 12 2021 at 18:08):

One point that might be worth emphasizing here is that for projects such as "formalize the stacks project" to be remotely feasible, the incentive structure in academic math would have to change drastically.

Kevin Buzzard (Dec 12 2021 at 19:43):

Yes this is part of the reason why it's not feasible. Young people like Adam and Johan are right now taking risks, working on projects which will produce results which are alien to the traditional assessment approach when it comes to things like hiring or promotion or tenure.

Kevin Buzzard (Dec 12 2021 at 19:45):

Right now we have Hoskinson but I think his centre might be more focused on outreach, teaching tools, interactive stuff etc. We have to work on other sources of funding to level up. I can make the definition of a scheme in my spare time on Thursday evenings with a few undergraduates who have nothing to lose and everything to gain from the project. I can't make the stacks project in that way.

Dima Pasechnik (Dec 12 2021 at 20:19):

That it took 6 years for Odd Order Theorem formalisation is more to do with the authors being very far from the group theory, research-wise. I gather 50-75% of the time was spent learning enough group theory.

Kevin Buzzard (Dec 12 2021 at 21:33):

I think closer to the truth world be the assertion that a lot of the time was spent on formalising the prerequisites. But my point is that I think it's easier for a human to learn undergraduate level group theory, number theory and representation theory than it is to learn PhD level material about algebraic stacks and other technical things in alg geom.

If you like it's the same kind of problem which I'm now facing at Xena. In the past I could tell people "choose anything you like, it's probably not in mathlib" and I'd have undergraduates making PRs defining matrices. Nowadays you have to be far more mathematically advanced to contribute. It's that phenomenon but much worse when it comes to a 7000 page document summarising amongst other things post-Grothendieck breakthroughs in commutative algebra and algebraic geometry

Dima Pasechnik (Dec 13 2021 at 00:31):

I am not sure about "ease to contibute" - I still easily find undergrad combinatorics topics not in mathlib which potentially should lead to contributions.

But it's the grown requirements for PRs to fit well that stop the contributions, e.g. https://github.com/leanprover-community/mathlib/pull/7498 is stalled for such a reason since summer. Or problems that my other student, Lu-Ming, faced, which seem to be due to inefficiencies in Lean/mathlib dealing with a seemingly easy object, the group Z-algebra of an order $n$ cyclic group, where he had to check concrete identities for concrete values of $n$.

Johan Commelin (Dec 13 2021 at 06:18):

I don't think we have stricter requirements for PRs these days compared to when I started 3 years ago. The only significant change I can think of is that you now need to satisfy a bunch of linters, but those were mostly enforced by hand before they became code. (Maybe 3 years ago you could write defs without docstrings. But I don't think writing docstrings is what you consider a problem.)
I'm sure that we all want the contribution process to be as easy as possible. If you have concrete suggestions for something that is hard and could be made easier, please let us know.

Yaël Dillies (Dec 13 2021 at 07:35):

I personally got a bit harsh on #7498, sorry. I will make sure it gets into mathlib some time soon. Just haven't gotten round to doing it yet.

Dima Pasechnik (Dec 13 2021 at 09:43):

by "stricter" I meant that there is now more "furniture in the room" a PR should fit into, without triggering a chain of rewrites.

Eric Wieser (Dec 13 2021 at 10:14):

I think graph theory is particularly bad in that regard, because there's much less of an obvious choice of definition vs say matrix multiplication.

Filippo A. E. Nuccio (Dec 13 2021 at 13:01):

typo there are four dots on p. 1 after the `number theory, algebra, analysis, list (using \dots you get the right ellipses with three dots).

Kevin Buzzard (Dec 18 2021 at 18:56):

There are four dots because I put a full stop after the \dots! Is that not right?? <googles> (still don't know)

Mario Carneiro (Dec 18 2021 at 20:13):

I think four dots is correct, and that's what I use in my writing.

Filippo A. E. Nuccio (Dec 20 2021 at 14:12):

I am attaching an excerpt of my "Oxford Guide to Style"; the way I see things is that if an an ellipsis marks the end of an incomplete sentence, it replaces the period (= 3 points). You only have four points whenever a normal complete sentence (with its usual period) is followed by omitted material, and it does not seem to me to be your case. The-Oxford-Guide-to-Style.pdf

Julian Berman (Dec 20 2021 at 14:20):

Wikipedia seems to say:

Whether an ellipsis at the end of a sentence needs a fourth dot to finish the sentence is a matter of debate; Chicago advises it,[8] as does the Publication Manual of the American Psychological Association (APA style),[9] while some other style guides do not;[citation needed] the Merriam-Webster Dictionary and related works treat this style as optional, saying that it "may" be used.[10]

So you can win internet points by linking to that oxford style guide for the citation needed :)

Filippo A. E. Nuccio (Dec 20 2021 at 14:21):

I did not get that far, I have simply studied one guide to style and it was the Oxford one—whence my comment—but it is nice to see that the matter is debatable :-)


Last updated: Dec 20 2023 at 11:08 UTC