ICM talk

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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

needs a capital A.

[Jeremy Avigad]

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]

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]

octonians --> octonions

[Scott Morrison]

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]

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]

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]

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

[Johan Commelin]

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]

• 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]

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

[Johan Commelin]

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

[Johan Commelin]

(• "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]

• 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]

• "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]

• "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]

"cinompletions" -> "completions"

[Mario Carneiro]

• "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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

In 1.8 you could mention finiteness of the class group.

[Anne Baanen]

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

[Patrick Massot]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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

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

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

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]

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]

Classical is a very overloaded word in mathematics

[Stuart Presnell]

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

[Mario Carneiro]

@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]

@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]

@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]

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

[Rob Lewis]

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]

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

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]

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]

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]

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]

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]

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

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]

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]

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]

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]

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]

Oh, I certainly missed that one: thanks!

[Filippo A. E. Nuccio]

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 $\mathbb{R}_{\geq 0}$ and $\mathbb{R}$ are different types, and so that " a non-negative real number is not a real number". The problem with $\mathbb{N}$ vs $\mathbb{Z}$ vs $\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\colon\mathbb{R}\to\mathbb{R}$ and $\sin\colon\mathbb{R}\to[-1,1]$ are different in type theory, but seen as subsets of $\mathbb{R}\times [0,1]\subseteq\mathbb{R}\times\mathbb{R}$ they are equal (or "more equal" at any rate).

[Kevin Buzzard]

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]

Filippo A. E. Nuccio said:

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

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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]

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]

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]

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

[Arthur Paulino]

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]

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

[Johan Commelin]

@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]

So calling it a monolith seems correct to me.

[Matthew Ballard]

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

[Arthur Paulino]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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]

No it doesn't

[Patrick Massot]

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

[Yaël Dillies]

Fair enough

[Johan Commelin]

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]

:wink: affinity refactor :wink:

[Filippo A. E. Nuccio]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

And AC?

[Yury G. Kudryashov]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

@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]

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

[Floris van Doorn]

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]

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]

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]

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

[Floris van Doorn]

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]

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]

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

[Floris van Doorn]

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]

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]

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

[Floris van Doorn]

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]

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]

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]

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

[Filippo A. E. Nuccio]

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]

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]

Well, this is getting somewhat personal (like: "what is an algebraically closed field of char 0"? gets the answers $\mathbb{C}$ or $\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 $\mathbb{F}_3$ is also a nice answer...)

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

In math all of these are equal.

[Mario Carneiro]

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]

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

[Mario Carneiro]

all of the other examples are "coincidences"

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

@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]

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

[Mario Carneiro]

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]

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

[Yao Liu]

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]

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]

The differences are of a social kind.

[Eric Wieser]

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]

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]

(deleted)

[Dima Pasechnik]

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

[Dima Pasechnik]

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]

LEM in proofs doesn't affect program extraction.

[Sebastian Reichelt]

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]

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]

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]

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]

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]

Thanks!

[Yaël Dillies]

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

[Johan Commelin]

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]

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]

Typo:

used extensivel in

extensively

[Rob Lewis]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(at least in my head)

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

Nitpick:

The library is not designed for pedagogy or readability;

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

[Johan Commelin]

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]

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]

another nitpick:

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

duplicates implement*

[Johan Commelin]

maybe build a new implementation?

[Kevin Buzzard]

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]

Some random nitpicks:

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

As "for $x$ 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 : \mathbb{R}_{\geq 0}$ does not have type $\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 $x \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]

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]

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 $f$ is clearly $O(x^{-2})$ for $x$ large”?

As "for $x$ 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]

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]

Maybe I should change $f$ to $1/\sqrt{1+x^3+x^4}$ or something.

[Johan Commelin]

I think it's fine as it is

[Sebastian Reichelt]

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 $f$. But reading with a non-Lean POV, my thoughts went something like: "OK, I guess 'for $x$ large' first needs to be made precise... Wait, it's actually redundant... Now what's so special about $f$ being $O(x^{-2})$?"

[Patrick Massot]

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

[Ruben Van de Velde]

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]

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]

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

[Kevin Buzzard]

Oops!

[Julian Berman]

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]

Patrick Massot said:

I don't understand what you you find redundant in that "for $x$ large enough". Saying "$f(x)$ is $O(x^{-2})$ for $x$ large enough" and "$f(x)$ is $O(x^{-2})$ for $x$ close to zero" are very different statements. Maybe you would prefer "$f(x)$ is $O(x^{-2})$ when $x$ 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]

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]

Kevin Buzzard said:

Maybe I should change $f$ to $1/\sqrt{1+x^3+x^4}$ or something.

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

[Mario Carneiro]

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]

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]

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

[Adam Topaz]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Filippo A. E. Nuccio]

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]

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]

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