Stream: general

Topic: Notices of the AMS paper

Kevin Buzzard (Apr 24 2020 at 13:55):

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 (Apr 24 2020 at 13:57):

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 (Apr 24 2020 at 13:57):

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

Johan Commelin (Apr 24 2020 at 13:57):

There. You've got your first brutal comment.

Yury G. Kudryashov (Apr 24 2020 at 14:26):

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 (Apr 24 2020 at 14:28):

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

Patrick Massot (Apr 24 2020 at 14:30):

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

Johan Commelin (Apr 24 2020 at 14:33):

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 (Apr 24 2020 at 14:40):

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

Johan Commelin (Apr 24 2020 at 14:44):

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 (Apr 24 2020 at 14:46):

Johan Commelin said:

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

Eew! Neither do I!

Johan Commelin (Apr 24 2020 at 14:53):

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

Donald Sebastian Leung (Apr 24 2020 at 14:54):

@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 (Apr 24 2020 at 15:12):

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 (Apr 24 2020 at 15:13):

"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 (Apr 24 2020 at 15:15):

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

oops right

Reid Barton (Apr 24 2020 at 15:16):

Backwards reasoning strikes again

Right!

Johan Commelin (Apr 24 2020 at 15:18):

have vs suffices :lol:

(deleted)

Donald Sebastian Leung (Apr 24 2020 at 15:29):

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 (Apr 24 2020 at 15:31):

Thanks. I have no excuse!

Donald Sebastian Leung (Apr 24 2020 at 15:33):

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 (Apr 24 2020 at 15:34):

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

Jalex Stark (Apr 24 2020 at 16:32):

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 (Apr 24 2020 at 16:33):

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

Kevin Buzzard (Apr 24 2020 at 19:29):

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

Yury G. Kudryashov (Apr 24 2020 at 19:47):

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

Alex J. Best (Apr 24 2020 at 20:26):

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 (Apr 24 2020 at 23:31):

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 (Apr 25 2020 at 01:25):

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 (Apr 25 2020 at 01:33):

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

Johan Commelin (Apr 25 2020 at 05:11):

@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 (Apr 25 2020 at 05:12):

I'm more into classical improv, actually.

David Michael Roberts (Apr 25 2020 at 05:59):

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 (Apr 25 2020 at 07:20):

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 (Apr 26 2020 at 17:16):

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

Patrick Massot (Apr 26 2020 at 17:17):

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 (Apr 26 2020 at 17:18):

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

Patrick Massot (Apr 26 2020 at 17:20):

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 (Apr 26 2020 at 17:20):

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 (Apr 26 2020 at 17:22):

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 (Apr 26 2020 at 17:22):

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

Patrick Massot (Apr 26 2020 at 17:24):

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 (Apr 26 2020 at 17:25):

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

Patrick Massot (Apr 26 2020 at 17:26):

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 (Apr 26 2020 at 17:27):

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 (Apr 26 2020 at 17:28):

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 (Apr 26 2020 at 17:30):

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 (Apr 26 2020 at 17:30):

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

Patrick Massot (Apr 26 2020 at 17:31):

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

Patrick Massot (Apr 26 2020 at 17:32):

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 (Apr 26 2020 at 17:34):

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

Patrick Massot (Apr 26 2020 at 17:34):

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 (Apr 26 2020 at 17:36):

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 (Apr 26 2020 at 17:37):

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 (Apr 26 2020 at 17:40):

Thanks a lot for all this

Patrick Massot (Apr 26 2020 at 17:41):

Is it brutal enough?

Definitely!

Kevin Buzzard (Apr 26 2020 at 17:43):

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 (Apr 26 2020 at 17:46):

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 (Apr 26 2020 at 17:57):

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
• search existing lemmas and definitions, fabstract style

• 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 (Apr 26 2020 at 17:58):

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

Patrick Massot (Apr 26 2020 at 17:59):

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 (Apr 26 2020 at 18:08):

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

Kevin Buzzard (Apr 26 2020 at 18:20):

When will it appear? I'll ask

Jasmin Blanchette (Apr 26 2020 at 18:27):

p. 1: "occured" is misspelled.

Jasmin Blanchette (Apr 26 2020 at 18:28):

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

Jasmin Blanchette (Apr 26 2020 at 18:30):

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 (Apr 26 2020 at 18:33):

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 (Apr 26 2020 at 18:36):

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

Jasmin Blanchette (Apr 26 2020 at 18:38):

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

Jasmin Blanchette (Apr 26 2020 at 18:40):

p. 5: ITP's -> ITPs.

Jasmin Blanchette (Apr 26 2020 at 18:45):

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

Jasmin Blanchette (Apr 26 2020 at 18:49):

"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 (Apr 26 2020 at 18:50):

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

Jasmin Blanchette (Apr 26 2020 at 18:52):

p. 10: Cocalc -> CoCalc.

Jasmin Blanchette (Apr 26 2020 at 18:53):

[Sag20] Inc. SageMath, ??

Kevin Buzzard (Apr 26 2020 at 19:27):

Thanks so much Jasmin!

Ashwin Iyengar (Apr 26 2020 at 19:31):

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

Jasmin Blanchette (Apr 27 2020 at 07:18):

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 (Apr 27 2020 at 07:37):

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 (Apr 27 2020 at 07:38):

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 (Apr 27 2020 at 08:03):

I see. It's taboo.

Kevin Buzzard (Apr 27 2020 at 08:12):

Barbara is a serious algebraic geometer

Kevin Buzzard (Apr 27 2020 at 08:14):

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 (Apr 27 2020 at 08:19):

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

Kevin Buzzard (Apr 27 2020 at 08:20):

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 (Apr 27 2020 at 11:41):

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 (Apr 27 2020 at 11:44):

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 (Apr 27 2020 at 11:48):

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 (Apr 27 2020 at 12:16):

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

Kevin Buzzard (May 01 2020 at 14:38):

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 (May 01 2020 at 14:39):

It's certainly less catchy but much more honest

Kevin Buzzard (May 01 2020 at 17:58):

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 (May 04 2020 at 17:02):

@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 (May 19 2020 at 17:05):

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 (Jun 17 2020 at 11:24):

@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 (Jun 17 2020 at 11:29):

That's really old

Kevin Buzzard (Jun 17 2020 at 11:30):

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

Kevin Buzzard (Jun 17 2020 at 11:30):

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

Billy Price (Jun 17 2020 at 11:32):

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

Kevin Buzzard (Jun 17 2020 at 11:33):

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 (Jun 17 2020 at 11:35):

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

Johan Commelin (Jun 17 2020 at 11:38):

It's not run by MS

Johan Commelin (Jun 17 2020 at 11:39):

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

Johan Commelin (Jun 17 2020 at 11:43):

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

Billy Price (Jun 17 2020 at 11:44):

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

Billy Price (Jun 17 2020 at 11:46):

Allow me to be direct

"I want a fulfilling career in Mathematics and Logic"

Jalex Stark (Jun 17 2020 at 12:24):

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 (Jun 17 2020 at 14:48):

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 (Jun 17 2020 at 14:54):

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

Patrick Massot (Jun 17 2020 at 14:55):

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

Patrick Massot (Jun 17 2020 at 14:55):

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

Oh no

Patrick Massot (Jun 17 2020 at 14:56):

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

Patrick Massot (Jun 17 2020 at 14:57):

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

Utensil Song (Jun 17 2020 at 15:23):

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 (May 06 2021 at 10:48):

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

Eric Wieser (May 06 2021 at 11:40):

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

Eric Rodriguez (May 06 2021 at 12:25):

I'm on texlive 2021, should be fine hopefully

Eric Wieser (May 06 2021 at 12:29):

Does TexLive even bundle pygments?

Eric Rodriguez (May 06 2021 at 14:21):

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 (May 06 2021 at 15:11):

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

Last updated: May 14 2021 at 02:15 UTC