Notices of the AMS paper

Stream: general

[Kevin Buzzard]

Here is the current version of my paper for the Notices of the AMS. They would like a final version by 1st May, 1 week from today. Any comments, however brutal, would be welcome.

[Kevin Buzzard]

NB I am not shouting about this paper on Twitter or anything yet -- this is a preliminary version (indeed there's still a TODO on p7 -- it would be great to hear from some people who know the state of analysis/geometry in Lean and who could supply some juicy theorem names if they're in master.

[Johan Commelin]

I don't like the spacing in footnote * on page 1.

[Johan Commelin]

There. You've got your first brutal comment.

[Yury G. Kudryashov]

Some examples from analysis: analytic functions, C^r functions, mean value theorem and friends, uniqueness of a solution of an ODE, inverse function thm and implicit function thm (PRed, hopefully will land before May 1st).

[Yury G. Kudryashov]

Probably @Sebastien Gouezel will come up with a different list, and you'll be able to choose from the union.

[Patrick Massot]

I wouldn't mention uniqueness in ODEs until we have existence.

[Johan Commelin]

Lean’s tactic state can often be easily understood by mathematicians without any specialist knowledge of ITP’s, because the notation used is standard mathematical notation.

@Kevin Buzzard Apart from the fact that you write x : X :rofl:

[Johan Commelin]

Maybe add a link to the Codewars website, when you first mention it?

[Johan Commelin]

In your discussion of gaps, you might mention that we have measure theory, but no applications to probability theory/stochastics. Combinatorics and graph theory is under construction.... but lots of gaps there.

[Kevin Buzzard]

Johan Commelin said:

I don't like the spacing in footnote * on page 1.

Eew! Neither do I!

[Johan Commelin]

@Kevin Buzzard I've read it, and I like it! You've already seen all my brutal comments above (-;

[Donald Sebastian Leung]

@Kevin Buzzard Thanks for mentioning Codewars in your paper!

I've skimmed through the first one and a half pages and found a typo (or is it a pun?) on page 2. Near the end of subsection 1.1, it says, "At this stage in the development of mathematics, every proof can be chased right down to the axioms of the system we are considering, and students are expected to lean from such courses that mathematics can be done in this way." I suppose it should say "learn"?

[Oliver Nash]

I might be going crazy but I think on LHS of page 5 in the proof of injectivity of g∘f there are some fs in place of gs and vice-versa.

[Oliver Nash]

"By definition, our task is to prove that if a,b∈X and g(f(a)) =g(f(b)), then a=b. By injectivity of f, it suffices to prove that f(a) =f(b), and this followsfrom injectivity of g and our assumption."

I claim the second sentence should begin "By injectivity of g ..." etc.

[Oliver Nash]

Actually maybe it's possible to read it two ways, rendering it correct as written. I take it back.

[Reid Barton]

oops right

[Reid Barton]

Backwards reasoning strikes again

[Oliver Nash]

Right!

[Johan Commelin]

have vs suffices :lol:

[Oliver Nash]

(deleted)

[Donald Sebastian Leung]

Oliver Nash said:

I might be going crazy but I think on LHS of page 5 in the proof of injectivity of g∘f there are some fs in place of gs and vice-versa.

"By definition, our task is to prove that if a,b∈X and g(f(a)) =g(f(b)), then a=b. By injectivity of f, it suffices to prove that f(a) =f(b), and this followsfrom injectivity of g and our assumption."

I claim the second sentence should begin "By injectivity of g ..." etc.

I'm used to backwards reasoning since I'm more used to proving theorems in an ITP than on paper (my paper proofs are often unnecessarily long and verbose), but, strangely, I also initially thought the same as you did.

[Oliver Nash]

Thanks. I have no excuse!

[Donald Sebastian Leung]

About the Lean example on pages 5-6 about the composition of two injective functions, perhaps it would be better to add a trailing comma to the last tactic invocation (assumption)? I would imagine that someone new to Lean stepping through the proof after clicking on the link might be confused that (s)he cannot see the "no goals" message right after the assumption since the theorem is already proven at that point.

[Kevin Buzzard]

I'll reword the proof. I wanted it to follow the tactic proof. Thanks

[Jalex Stark]

I will try to come up with some more brutal comments but first I want to say that I absolutely love the latex analogy

[Patrick Massot]

I have a couple of them, but I don't have time to write now.

[Kevin Buzzard]

The LaTeX analogy is my attempt to explain to a mathematician what a computer program is

[Yury G. Kudryashov]

Some \subsection titles end with ., some don't.

[Yury G. Kudryashov]

I'd mention https://en.wikipedia.org/wiki/Four_color_theorem#Simplification_and_verification

[Alex J. Best]

Some (personal preference?) comments, overall I really enjoyed it, it is a really nice summary and call to arms.

I'm not sure about the introduction, I don't know the exact audience of the notices, but given that it is a bit broad and that notices is a coffee table type magazine, it might be better to make it clear that this is an example (whose details are not important for the article) from the get go rather than having people read two paragraphs about Galois deformations and Hida's hecke algebra to get going. Maybe swapping the first few paragraphs around would help, or add a hook, giving the reader a sense of where the article is going to draw them in?

"Just as a LATEX file is likely to contain some parts written
in “maths mode”, a Lean file is likely to contain some
parts written in “tactic mode”." - I don't understand the comparison here really, it makes it sound like the maths only happens in tactic mode, and at this point in the discussion I don't think term/tactic is relevant yet. The way I see it given that math-mode is the less readable to humans part of a TeX document, that makes it more analogous to term mode in some ways. (I see later you draw the comparison again and do mention term mode with a harder to read example, I feel like you are using the term tactic mode really to mean all non-comment lean code).

I feel like it would be helpful to say more / give an example early when you say "The file might contain errors,
for example perhaps a proof in the file is incomplete
or incorrect, or a definition is not specified precisely
enough." of a specific sort of way a proof can be incorrect people can relate to, "e.g. not all hypotheses are satisfied of a theorem that is applied, or some cases have not been checked"

"Suffice it to say" seems like a typo in section 2.

"open function -- giving us access to the concept of injectivity" - also seems like a needless complication at this point in the article (surely composition of injectivity is in the function namespace anyway ;) )

Probably you are aware or this is a placeholder but at the end of 3.1 there is an errant sentence "A Proposition is any true/false statement."

"Probably many of us are familiar with Sudoku"... I think you can just say "In the game Sudoku one .." :D

"Recall that a b : X" looks like there is a double space between : and X, weird

[Bryan Gin-ge Chen]

I really liked the paper as well! Here are some comments:

1. I agree with @Alex J. Best about the first few sentences of the intro.

2. Some of the comments in the proof script jumped out at me:

   • open function -- giving us access to the concept of injectivity: maybe -- lets us abbreviate function.injective as injective? (This shows up twice)
   • import tactic -- tactic mode: maybe -- gives access to many useful tactics? If you do want a "tactic mode" comment, it should go after begin.
     I know it's better not to get into the weeds with the code, but I could also see these comments leading to confusion in the #new members thread too...

3. Rather than link directly to the Zulip chat (which will show a somewhat intimidating login screen), maybe we should link to https://leanprover-community.github.io/ instead? Actually, we should make a nice landing page for "Getting started with Lean": I like the text that's on the perfectoid project home page.

4. It might be nice to include an attractive illustration of a graph of some declarations in mathlib or something like that. (I'd volunteer, but I'm not convinced that I can produce anything suitable.)

[Mario Carneiro]

In your list of example propositions, I don't know if it would take you too far afield to put the continuum hypothesis in the list

[Mario Carneiro]

Heh, now everyone who reads the Notices of the AMS will think I am a computer scientist :)

[Johan Commelin]

@Mario Carneiro He didn't claim you are only a computer scientist... for all we know you might also be a Jazz musician. :rolling_on_the_floor_laughing:

[Mario Carneiro]

I'm more into classical improv, actually.

[David Michael Roberts]

As one solves the level, i.e., builds the proof,

there is no reference to Lean games or levels before this point, just Sudoku levels. But 'levels' in Sudoku seems an odd concept: it's not like eg Super Mario Bros. or Lean's Natural Number Game. There's just individual puzzles, they aren't levels in some overarching game.

[Sebastien Gouezel]

Yury G. Kudryashov said:

Some examples from analysis: analytic functions, C^r functions, mean value theorem and friends, uniqueness of a solution of an ODE, inverse function thm and implicit function thm (PRed, hopefully will land before May 1st).

That's a good list (I especially like the inverse function theorem). One could add the Banach open mapping theorem, or Arzela-Ascoli.

[Patrick Massot]

Ok, let's try to find some brutal comments for Kevin.

[Patrick Massot]

About the title. I understand the concept of click-bait, and I know Kevin had great success with this concept in the past. But there is really very little about this question in the paper. I'm not sure it's wise to be so openly click baiting.

[Patrick Massot]

You could actually add some information in this direction if you are interested in discussing this.

[Patrick Massot]

On page 3, I think the word "Lean" comes too early. I really appreciate the herculean efforts you made to stop trolling the other proof assistants in this paper. But here you could easily do it even more. All this Section 2 is 100% generic. I would introduce the word Lean only when you are ready to show some code.

[Patrick Massot]

Footnote 1 one Page 3 refers to "Lean's kernel". I would remove "'s kernel" that is impossible to understand for your readers and don't add anything here.

[Patrick Massot]

At the very beginning of Section 3, you mention teaching mathematics to computers using the same path as the way we teach it to humans. But this is not what we do in mathlib, unless you count Bourbaki's treatise as teaching;

[Patrick Massot]

When code show up, you don't explain the weird symbols for logical and and for implication.

[Patrick Massot]

When commenting on $x \in X$ vs $x : X$ you write that "The difference is purely notationnal". I don't think you need such lies. If you don't want to spend time explaining how type theory is actually closer to our intuition then you can simply remove that sentence.

[Patrick Massot]

I also think the Sudoku sentence is weird, but this was already explained by others.

[Patrick Massot]

When referring to Lean in a web browser, I think you must write that the true thing is much faster. Otherwise people who will click that link will discard Lean as unusable.

[Patrick Massot]

At the end of page 3, the paragraph on Codewars seems really weird to me. It feels like it was put there because you wanted to mention that website but didn't know where to put this paragraph.

[Patrick Massot]

In the first paragraph of Section 3.4, I don't know what you mean by "Borel and Lebesgue measure". What is "Borel measure"?

[Patrick Massot]

In the next paragraph, I find it rather depressing to see that you expect the Cauchy formula in twelve months. It sounds like we would need that long to prove it, when you mean you expect twelve months until someone decides this is the priority and it should be done now.

[Patrick Massot]

I don't think you should write my work on topology was heroic.

[Patrick Massot]

I don't think Scott wrote a "generic category theory diagram-chasing tactic".

[Patrick Massot]

I think your comparison between MathSciNet and Fabstracts makes sense. Good math reviews contain much more that statements, they are meant to prove context. I think we need both.

[Yury G. Kudryashov]

I want to have Cauchy formula so you can expect it in much less than a year.

[Patrick Massot]

I don't think you should cheat with the Annals paper formalization. The work of Johannes, Rob and Sanders is very nice, but everybody knows they targeted a very unusual Annals paper. You can still mention it of course.

[Patrick Massot]

I think mentioning Mathematics in Lean is risky, given this has barely started. I would be more vague, saying we plan to work on teaching material;

[Patrick Massot]

I think the last paragraph is encouraging the confusion between proof assistant and computer assisted proofs involving huge case analyses (or numerical analysis).

[Kevin Buzzard]

Thanks a lot for all this

[Patrick Massot]

Is it brutal enough?

[Kevin Buzzard]

Definitely!

[Kevin Buzzard]

I was a bit unsure about the paper when I finished it. I read it and felt that maybe I was just a dreamer and some people should tell me to tone it down

[Johan Commelin]

I should add that I really enjoyed reading it, and I'm looking forward to reactions from the AMS and later on the general public. It's a nice advertisement, and after processing Patrick's comments it will be even better!

[Patrick Massot]

If you can afford a few more sentences (I don't know what are your constraints) it would be nice to mention other applications of proof assistants. If I remember correctly, you mention:

• having computerized Barry Mazurs
• teaching undergrads
• search existing lemmas and definitions, fabstract style

I would add at least:

• check very long proofs that require to remember a super-human amount of details
• force people to clarify their thinking, maybe discover better abstractions

[Patrick Massot]

And probably also: reading a proof and being able to jump to precise definitions and statements without any ambiguity

[Patrick Massot]

Now let's ask an important question: do you know when this paper will appear? We really really need to work on the documentation and website before this appears.

[orlando]

@Kevin Buzzard we need dreamer in this world :wink:

[Kevin Buzzard]

When will it appear? I'll ask

[Jasmin Blanchette]

p. 1: "occured" is misspelled.

[Jasmin Blanchette]

p. 1: Why the quotes around "thought experiment"? The phrase is recorded in dictionaries.

[Jasmin Blanchette]

Inconsistent uses of Oxford commas, e.g. "group theory, linear algebra, and real analysis" on p. 2 vs. "sets, functions and binary relations" on p. 1.

[Jasmin Blanchette]

Gustave Flaubert would have used ironic italics in many places where you use quotes, e.g. "known to the experts". I'm trying to imagine what a British Flaubert would read like. ;)

[Jasmin Blanchette]

"We will capitalise Proposition to remind us of this slightly non-standard usage." Nonstandard??? ;)

[Jasmin Blanchette]

Is Sudoku still capitalized by anybody? My dictionary (Oxford Am. E. Dict.) uses lowercase.

[Jasmin Blanchette]

p. 5: ITP's -> ITPs.

[Jasmin Blanchette]

p. 7: "via completing levels": is "via" (as opposed to "by") + gerund really a thing in English?

[Jasmin Blanchette]

"developed by a team led by Larry Paulson in 2007". Not true. He started in 2003 or so. SH's first release was in 2007.

[Jasmin Blanchette]

p. 7: "at a /v/f/ast rate".

[Jasmin Blanchette]

p. 10: Cocalc -> CoCalc.

[Jasmin Blanchette]

[Sag20] Inc. SageMath, ??

[Kevin Buzzard]

Thanks so much Jasmin!

[Ashwin Iyengar]

funny typo, 2nd page bottom left before 1.2: "students are expected to lean from such courses"

[Jasmin Blanchette]

One last point, Kevin. It strikes me that most working mathematicians who are seriously interested in proof assistants have had some traumatizing experience with $\LaTeX$ proofs. IIRC you had yourself a manuscript on arXiv for 2 years because you couldn't feel 100% confident that it was correct. Voevodsky had amazing slides about this as well. Sander Dahmen at the VU is deeply worried about the correctness of computer algebra systems he uses. Maybe I was too focused on the commas and hyphens, but your article could emphasize the motivation for all this. I doubt every mathematician sees the point of computer-checked proofs.

[Kevin Buzzard]

My extensive experience talking to mathematicians about this issue is that the vast majority regard it as something not to worry about so I made the decision not to talk about it at all

[Kevin Buzzard]

I don't want to come across as paranoid, even though this is one of the reasons I personally got into this area in the first place.

[Jasmin Blanchette]

I see. It's taboo.

[Kevin Buzzard]

https://twitter.com/BarbaraFantechi/status/1221765472846262272?s=20

I couldn't finish the slides, there's so much I disagree with. 1) acceptance of wrong proofs is privilege 2) wrong proofs have always existed, it's getting better 3) there are other methods to fix the problem 4) "wrong proofs maths is useless" is a bad take 1/ https://twitter.com/HigherGeometer/status/1221567236223029248

- Scoffing Mathematician 🏳️‍🌈🇪🇺 (@BarbaraFantechi)

[Kevin Buzzard]

Barbara is a serious algebraic geometer

[Kevin Buzzard]

I definitely didn't want to get into some sort of Twitter spat with her (she broadly supports the principle of making these ITP systems better and I have a lot of respect for her) but wrong proofs have always existed and in my opinion it's getting worse. But it's clearly just my opinion if someone like her thinks otherwise (it might be subject-dependent as well).

[Mario Carneiro]

I don't really understand the point about privilege. Is there some kind of correlation between underprivileged groups and proof correctness?

[Kevin Buzzard]

The actual status of "wrong proofs maths" is actually very complex. There is this completely unquantifiable concept of an "idea" and if a wrong proof contains a good idea then one can get a lot from it. In fact another Italian algebraic geometer, Alessio Corti, told me that the ideas in the false Tsuji Annals proof which I cite in the talk had inspired some of the work related to the big finite generation of canonical ring result which helped to get Birkar his FIelds Medal.

[Chris Hughes]

Mario Carneiro said:

I don't really understand the point about privilege. Is there some kind of correlation between underprivileged groups and proof correctness?

This is the first in a stream of tweets. She goes on to explain that women, non-whites and people from less prestigious universities get a harder time from referees.

[Mario Carneiro]

In that case, I would guess that proof assistants are a good thing, since computerized referees only care about whether your proof is correct and not other social-based correctness proxies that can bias against underprivileged groups

[Chris Hughes]

That was my impression. In fact at first I misunderstood the tweet, and thought she was listing things that Kevin said that she disagreed with.

[Kevin Buzzard]

This brings to mind Voevodsky's quote about how a proof from a trusted author might not be checked in detail

[Kevin Buzzard]

Patrick Massot said:

About the title. I understand the concept of click-bait, and I know Kevin had great success with this concept in the past. But there is really very little about this question in the paper. I'm not sure it's wise to be so openly click baiting.

I am dealing with these comments today. How about "Proving theorems using computers" for the title @Patrick Massot ?

[Patrick Massot]

It's certainly less catchy but much more honest

[Kevin Buzzard]

Here's the version I sent. I also asked when it might be likely to appear. I don't know if there is now some refereeing process.

[Kevin Buzzard]

@Patrick Massot asked (possibly offline?) when the article would appear -- they say "The article is lined up for the November issue. However, if referee take longer than usual, we'll move it for later." In particular, we have time to prepare for the dream result of a bunch more people arriving.

[Nam]

just finished skimming through your paper. i'd like to also point out some prelim work related to automatic proof of math statements at deephol.org

[Billy Price]

@Kevin Buzzard How did you format lean code in that paper? I've followed this guide https://github.com/leanprover/lean/blob/master/doc/syntax_highlight_in_latex.md and I have a bunch of red boxes around all the unicode characters - and the characters themselves look pretty ugly. Do you use the minted package like in the guide or something else?

[Kevin Buzzard]

That's really old

[Kevin Buzzard]

https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.md

[Kevin Buzzard]

Anything in leanprover/lean is likely to be very old, that repo is frozen

[Billy Price]

Ah cool thanks. Isn't lean4 in progress? Where does the most up-to-date lean3 stuff go?

[Kevin Buzzard]

MS is not generating any Lean3 stuff; all the Lean3 action is on the community website. The Lean 4 stuff is in leanprover/lean4

[Billy Price]

What's the relationship between leanprover-community and lean? Is it unofficial or is it run by MS?

[Johan Commelin]

It's not run by MS

[Johan Commelin]

https://leanprover-community.github.io/meet.html

[Johan Commelin]

@Billy Price The community is unofficial... if you're not careful you run the risk of becoming part of it :wink:

[Billy Price]

https://mywiki.wooledge.org/XyProblem Oh god I'm so guilty of this

[Billy Price]

Allow me to be direct

"I want a fulfilling career in Mathematics and Logic"

[Jalex Stark]

it's an open question how well the tactic "participate in leanprover-community" applies to the goal "get funded as an early-career mathematician". Certainly if you already have funding, it is great for "stimulate mathematical work that feeds into a research program with a long future"

[Utensil Song]

Billy Price said:

Kevin Buzzard How did you format lean code in that paper? I've followed this guide https://github.com/leanprover/lean/blob/master/doc/syntax_highlight_in_latex.md and I have a bunch of red boxes around all the unicode characters - and the characters themselves look pretty ugly. Do you use the minted package like in the guide or something else?

"a bunch of red boxes around the unicode characters" is still an issue in this Zulip, could it be fixed somehow?

[Patrick Massot]

You need to pester people at pygments to make a release.

[Patrick Massot]

Wait, I see on https://github.com/pygments/pygments/releases there has been a release on March 6th.

[Patrick Massot]

So maybe we should now pester the people at Zulip to upgrade

[Patrick Massot]

Oh no

[Patrick Massot]

Bryan commits went in on March 14th. I thought it was older.

[Patrick Massot]

So I go back to saying you should pester people at pygment.

[Utensil Song]

The PR was https://github.com/pygments/pygments/pull/1415 and there was a discussion about the release frequency here although there isn't much in the 2.7 milestone left. The release cycle seems to be around 3-6 months.

[Eric Rodriguez]

Sorry to completely necro an ancient thread, but does anyone know how to make pygments not show red boxes on custom notation?

[Sebastian Ullrich]

See the end of https://leanprover.github.io/lean4/doc/syntax_highlight_in_latex.html

[Eric Wieser]

You might need to update your pygments too; certainly overleaf if you're using that has quite an old version.

[Eric Rodriguez]

I'm on texlive 2021, should be fine hopefully

[Eric Wieser]

Does TexLive even bundle pygments?

[Eric Rodriguez]

not sure to be honest, it worked fine when I used the workaround so hopefully I didn't just accidentally send malware or something :b

[Eric Wieser]

You might want to run pygmentize -V or similar to work out what version you're on, in case its ancient!