Zulip Chat Archive

Stream: general

Topic: Notices of the AMS paper


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 24 2020 at 13:57):

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

view this post on Zulip Johan Commelin (Apr 24 2020 at 13:57):

There. You've got your first brutal comment.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 24 2020 at 14:30):

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

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Apr 24 2020 at 14:40):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 (-;

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Apr 24 2020 at 15:16):

oops right

view this post on Zulip Reid Barton (Apr 24 2020 at 15:16):

Backwards reasoning strikes again

view this post on Zulip Oliver Nash (Apr 24 2020 at 15:16):

Right!

view this post on Zulip Johan Commelin (Apr 24 2020 at 15:18):

have vs suffices :lol:

view this post on Zulip Oliver Nash (Apr 24 2020 at 15:22):

(deleted)

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Apr 24 2020 at 15:31):

Thanks. I have no excuse!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 15:34):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 24 2020 at 16:33):

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

view this post on Zulip Kevin Buzzard (Apr 24 2020 at 19:29):

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

view this post on Zulip Yury G. Kudryashov (Apr 24 2020 at 19:47):

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

view this post on Zulip Yury G. Kudryashov (Apr 24 2020 at 19:52):

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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:12):

I'm more into classical improv, actually.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 26 2020 at 17:16):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 26 2020 at 17:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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;

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 26 2020 at 17:24):

When commenting on xXx \in X vs x:Xx : 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.

view this post on Zulip Patrick Massot (Apr 26 2020 at 17:25):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 26 2020 at 17:30):

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

view this post on Zulip Patrick Massot (Apr 26 2020 at 17:31):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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;

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:40):

Thanks a lot for all this

view this post on Zulip Patrick Massot (Apr 26 2020 at 17:41):

Is it brutal enough?

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:42):

Definitely!

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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
  • 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip orlando (Apr 26 2020 at 18:08):

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

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 18:20):

When will it appear? I'll ask

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:27):

p. 1: "occured" is misspelled.

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:28):

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

view this post on Zulip 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.

view this post on Zulip 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. ;)

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:36):

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

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:38):

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

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:40):

p. 5: ITP's -> ITPs.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:50):

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

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:52):

p. 10: Cocalc -> CoCalc.

view this post on Zulip Jasmin Blanchette (Apr 26 2020 at 18:53):

[Sag20] Inc. SageMath, ??

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 19:27):

Thanks so much Jasmin!

view this post on Zulip 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"

view this post on Zulip 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\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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Apr 27 2020 at 08:03):

I see. It's taboo.

view this post on Zulip Kevin Buzzard (Apr 27 2020 at 08:11):

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

view this post on Zulip Kevin Buzzard (Apr 27 2020 at 08:12):

Barbara is a serious algebraic geometer

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip Patrick Massot (May 01 2020 at 14:39):

It's certainly less catchy but much more honest

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 11:29):

That's really old

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 11:30):

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

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 11:30):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 17 2020 at 11:38):

It's not run by MS

view this post on Zulip Johan Commelin (Jun 17 2020 at 11:39):

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

view this post on Zulip 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:

view this post on Zulip Billy Price (Jun 17 2020 at 11:44):

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

view this post on Zulip Billy Price (Jun 17 2020 at 11:46):

Allow me to be direct

"I want a fulfilling career in Mathematics and Logic"

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 17 2020 at 14:54):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 17 2020 at 14:55):

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

view this post on Zulip Patrick Massot (Jun 17 2020 at 14:56):

Oh no

view this post on Zulip Patrick Massot (Jun 17 2020 at 14:56):

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

view this post on Zulip Patrick Massot (Jun 17 2020 at 14:57):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (May 06 2021 at 11:11):

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

view this post on Zulip 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.

view this post on Zulip Eric Rodriguez (May 06 2021 at 12:25):

I'm on texlive 2021, should be fine hopefully

view this post on Zulip Eric Wieser (May 06 2021 at 12:29):

Does TexLive even bundle pygments?

view this post on Zulip 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

view this post on Zulip 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