## Stream: general

### Topic: Lean in the wild

#### Johannes Hölzl (Nov 29 2018 at 08:37):

Its always interesting to find unexpected Lean theories: https://github.com/levjj/esverify-theory/
From a first glance, esverify is a Javascript/ECMAScript verifier, and these are some semantics with soundness...

#### Andrew Ashworth (Nov 29 2018 at 08:42):

I enjoy looking at different people's coding style; this is nicely written

#### Johan Commelin (Dec 08 2018 at 10:41):

@Kevin Buzzard Did you just confess on Reddit that you don't know much about Reddit?

#### Johan Commelin (Dec 08 2018 at 10:42):

Anyway, congrats with the visibility!

#### Kenny Lau (Dec 08 2018 at 10:54):

yes... visibility... is a bad thing in my opinion

#### Bryan Gin-ge Chen (Jan 26 2019 at 22:02):

Here's a cool writeup of the thesis that includes the esverify project mentioned up above by @Johannes Hölzl https://chris-schuster.net/thesis#esverify

#### Rob Lewis (Feb 06 2019 at 10:55):

More Lean in the wild, if you're willing to read some Portuguese: someone was working on cryptography last summer. https://www.maxwell.vrac.puc-rio.br/35851/35851.PDF

#### Mario Carneiro (Feb 06 2019 at 11:03):

is premise still a keyword? Looks like it means axiom from context

#### Rob Lewis (Feb 06 2019 at 11:06):

I thought it was a Prop-valued variable, but I'm not sure.

#### Mario Carneiro (Feb 06 2019 at 11:14):

actually I think you're right

#### Kevin Buzzard (Feb 06 2019 at 11:37):

"When describing a proof of a theorem, one must be cautious to ensure said proof
does not contain errors or inconsistencies.". This guy obviously has no idea about how mathematics works in practice. We're in a post-caution world now.

#### Scott Morrison (Feb 12 2019 at 10:41):

A slightly unusual "Lean in the wild" story:

My partner was out at an aerials (circus stuff) class this evening, talking to someone, who at some point in the conversation asked "Coq or Lean"? (Context: they worked in CS at a research institute here in Canberra, my partner mentioned to them I was interested in automated theorem proving.)

#### Johannes Hölzl (Feb 12 2019 at 12:25):

Now I'm disappointed they didn't ask about Isabelle. For me Australia is Isabelle territory.

#### Kevin Buzzard (Feb 12 2019 at 12:26):

Everyone knows that mathematicians can't use Isabelle because it doesn't have dependent types?

#### Kevin Buzzard (Feb 12 2019 at 12:27):

I gave a talk in Cambridge two weeks ago and at the end of it Larry Paulson told one of his post-docs to go away and define a scheme in Isabelle, to prove it could be done. When he'd left I told the post-doc that I'd met people who were skeptical.

#### Kevin Buzzard (Feb 12 2019 at 12:27):

Or, at least, skeptical that you could do it whilst remaining sane.

#### Mario Carneiro (Feb 12 2019 at 12:28):

set theory doesn't have dependent types either...

#### Kevin Buzzard (Feb 12 2019 at 12:28):

yeah but look at the set theorists.

#### Johan Commelin (Feb 12 2019 at 12:28):

Set theory probably doesn't have schemes either :rolling_eyes:

#### Kevin Buzzard (Feb 12 2019 at 12:28):

Wait -- you can basically make dependent types in set theory, right?

#### Mario Carneiro (Feb 12 2019 at 12:28):

being a de facto foundation for pen-and-paper maths?

#### Mario Carneiro (Feb 12 2019 at 12:29):

you can, that's kind of the point

#### Johannes Hölzl (Feb 12 2019 at 12:29):

Most of analysis works in HOL.

#### Mario Carneiro (Feb 12 2019 at 12:29):

set theory doesn't really have types at all, but you can reconstruct it all

#### Kevin Buzzard (Feb 12 2019 at 12:29):

An example of a dependent type is a function which Johan will have seen, which takes a topological space and presheaf on it, and defines a function from the space sending a point to an element of the stalk of the presheaf at that point.

#### Mario Carneiro (Feb 12 2019 at 12:29):

as long as you can make a big enough type you can do most of the same things in HOL

#### Kevin Buzzard (Feb 12 2019 at 12:29):

This is manifestly a dependent type, because the target depends on the source.

#### Mario Carneiro (Feb 12 2019 at 12:30):

you just can't call it a dependent type

#### Kevin Buzzard (Feb 12 2019 at 12:30):

However in Hartshorne he just says "now let $Y$ be the disjoint union of all the stalks, and define a function from X to Y..."

#### Mario Carneiro (Feb 12 2019 at 12:30):

in set theory a function from X to Y is just a set

#### Mario Carneiro (Feb 12 2019 at 12:30):

no dependent types here

#### Mario Carneiro (Feb 12 2019 at 12:30):

doesn't matter how fancy X and Y are

#### Kevin Buzzard (Feb 12 2019 at 12:31):

Can you do that in Isabelle? @Johannes Hölzl I've noticed that people do non-trivial analysis in this Isabelle thing. So what about schemes? Everyone seems to think it will be hell, apart from Larry.

#### Mario Carneiro (Feb 12 2019 at 12:32):

it's not pleasant to encode a function as a set when the foundation supports functions directly, but it can be done

#### Mario Carneiro (Feb 12 2019 at 12:32):

and it has to be done this way when you can't find a suitable hack to make your dependent type less dependent

#### Johannes Hölzl (Feb 12 2019 at 13:28):

I'm not sure I know enough about schemes to know how to write them down in HOL. You essentially need to relativize everything, i.e. make every definition relative to a set. As far as I understand it, for schemes the biggest advantage of dependent types is that we can ad hoc use the subtype of a open set. This is not possible in HOL.

#### Kevin Buzzard (Mar 20 2019 at 20:14):

https://plus.maths.org/content/pure-maths-crisis

#### Scott Morrison (Mar 20 2019 at 21:19):

Pretty cool, Kevin! I hope people read this.

#### Scott Morrison (Mar 20 2019 at 21:21):

I understand from the "pitch to journalists" standpoint the 'crisis' story is great, and I fully appreciate that the mathematics literature is crap. Nevertheless, I think when talking to other mathematicians, I'd prefer to emphasise more the "this is fun" / "this isn't quite helpful yet, but if you pitch in someday soon this is going to be an awesome tool" / "if you don't pay attention now you're going to be a dinosaur" arguments.

#### Patrick Massot (Mar 20 2019 at 21:23):

We should rename this thread "Kevin in the wild" :wink:

#### Patrick Massot (Mar 20 2019 at 21:25):

I also think we should be careful with this "crisis" story. Insisting on this will probably only result in regular mathematicians thinking we are crackpots. And the general audience may also get the wrong message

#### Kevin Buzzard (Mar 20 2019 at 22:13):

I did not write that article, someone who came to my talk wrote that article. But I did say the word "crisis".

#### Andrew Ashworth (Mar 20 2019 at 22:24):

Semi-related: "Death of Proof", from 1993 Scientific American

#### Andrew Ashworth (Mar 20 2019 at 22:24):

https://blogs.scientificamerican.com/cross-check/the-horgan-surface-and-the-death-of-proof/

#### Andrew Ashworth (Mar 20 2019 at 22:25):

It is a decades-long crisis :sunglasses:

#### Kevin Buzzard (Mar 20 2019 at 22:38):

"A case in point was Andrew Wiles’s proof of Fermat’s last theorem. Only a handful of experts were qualified to evaluate the dense, 200-page proof when it first appeared. "

This is extremely misleading. I'm not even sure that it is true, but even if it is true, within a year or two of the proof appearing there was a very detailed survey article by Darmon, Diamond and Taylor explaining the proof which needed only the kind of background which a graduate student working in this area in algebraic number theory would have, so hundreds and maybe even thousands of people were able to verify the proof within a couple of years of it appearing.

#### Kevin Buzzard (Mar 20 2019 at 23:24):

I also think we should be careful with this "crisis" story. Insisting on this will probably only result in regular mathematicians thinking we are crackpots. And the general audience may also get the wrong message

I could give a far harsher talk where I point out various serious mistakes by prestigious people and then point to various recent extremely technical papers by these same people which I know because of insider information did not go through as rigorous a refereeing process as they should have done and then flat out accuse the mathematical community of not having done its job correctly. I am not sure who is the crackpot but recent events in number theory have made me start to firmly believe that it's not me but them. I have thus far refrained from telling such stories in public, but believe you me this is why I am here in the formal proof verification community.

#### Johan Commelin (Mar 21 2019 at 20:15):

There is also a follow-up to the blog post that @Andrew Ashworth linked: https://blogs.scientificamerican.com/cross-check/okay-maybe-proofs-arent-dying-after-all/. It seems to give a slightly different perspective...

#### Kevin Buzzard (Mar 29 2019 at 13:20):

https://stackoverflow.com/questions/55417159/lean-define-product-of-r-ideal-and-r-module

#### Kevin Buzzard (Mar 29 2019 at 13:20):

This sort of thing has come up before

#### Kevin Buzzard (Mar 29 2019 at 13:21):

There are people in our community who believe that because stackexchange is the goto place for programming questions, people should not be being redirected here for answers

#### Simon Hudon (Mar 29 2019 at 13:24):

Is there an archive-related reason to keeping all the discussions here?

#### Kenny Lau (Mar 29 2019 at 13:28):

hey I wrote that code :P maybe I should answer

#### Johan Commelin (Mar 29 2019 at 13:28):

You are taking a break from Lean (-;

#### Kevin Buzzard (Mar 29 2019 at 14:36):

I think it was @Scott Morrison who was arguing that SO was a place where we should be building a fanbase and I trust his judgement on these matters

#### Simon Hudon (Mar 29 2019 at 14:40):

... so the opposite of redirecting people here

#### Kevin Buzzard (Mar 29 2019 at 15:23):

Exactly. There was some discussion about this a while back. The point is that however well we attempt to archive this site, you can't just email the man at Google to say "whenever someone googles for Lean questions, point them here and not at Stack Exchange please". Have you noticed more and more people coming out of the woodwork recently asking random questions? This guy today is asking about modules over a ring -- they have a mathematical background and they are going to SO not here. It's something we need to think about.

#### Kevin Buzzard (Mar 29 2019 at 15:41):

Jordan tweeted to his 11.7K followers :D

#### Johan Commelin (Mar 29 2019 at 15:41):

Did he just misunderstand what happened?

#### Kevin Buzzard (Mar 29 2019 at 15:43):

I am pretty sure that he did not :-)

#### Kevin Buzzard (Mar 29 2019 at 15:43):

he's just being a wag

#### Patrick Massot (Mar 29 2019 at 16:18):

Following links brings https://t.co/qFMmlbCj9d which reminds us very much how little math is done in Lean compared to Isabelle...

#### Kevin Buzzard (Mar 29 2019 at 16:46):

They have apostol, we have Atiyah MacDonald, and I know which one I'd rather have

#### Patrick Massot (Mar 29 2019 at 19:05):

Except we don't "have Atiyah-MacDonald", right? We have part of chapter one if I followed correctly

#### Johan Commelin (Mar 29 2019 at 19:12):

Well, by now we have Nakayama, Hilbert basis, tensor products.

#### Johan Commelin (Mar 29 2019 at 19:13):

So that's also quite some stuff from other chapters

#### Johan Commelin (Apr 25 2019 at 21:51):

We just had a wonderful installation of Kevin's talk here in Freiburg. With CS and maths in the audience (and a bunch of undergrads!). People kept Kevin busy for >30 minutes after the talk.

#### Kevin Buzzard (May 21 2019 at 23:22):

https://twitter.com/XenaProject After several people in one day told me I needed to get on Twitter, I have got on Twitter. Apparently now I am just supposed to follow shedloads of people and retweet the things they tweet. This is what the world has become?? Patrick I stole your graph because it looks cool.

#### Kevin Buzzard (May 21 2019 at 23:32):

Oh now there's a surprise: https://twitter.com/leanprover

#### Mario Carneiro (May 21 2019 at 23:38):

not a single tweet. sounds about right

#### Mario Carneiro (May 21 2019 at 23:40):

lots of followers though, haha

#### Kevin Buzzard (Jun 04 2019 at 19:48):

http://www.math.columbia.edu/~woit/wordpress/?p=11053

#### Scott Morrison (Jun 04 2019 at 20:07):

I commented, including inviting people here ...

#### Johannes Hölzl (Jun 06 2019 at 18:05):

https://itp19.cecs.pdx.edu/accepted-papers/ 5 Lean papers at ITP, not bad

#### Simon Hudon (Jun 06 2019 at 18:12):

Nice! How do you know which one is about Lean?

#### Johannes Hölzl (Jun 06 2019 at 18:20):

Guessing by Name. I was counting 4, but then Rob pointed out that Minchao's paper is also a Lean implementation.
The concrete list:

• Jeremy Avigad, Mario Carneiro and Simon Hudon. Data types as quotients of polynomial functors
• Mario Carneiro. Formalizing computability theory via partial recursive functions
• Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics
• Robert Y. Lewis, Johannes Hölzl and Sander Dahmen. Formalizing the Solution to the Cap Set Problem
• Jesse Han and Floris van Doorn. A formalization of forcing and the consistency of the failure of the continuum hypothesis

#### Simon Hudon (Jun 06 2019 at 18:31):

All papers have authors who are or have been at CMU

#### Simon Hudon (Jun 06 2019 at 18:38):

I see Cody Roux has a paper too. Wasn't he also working with Lean?

#### Johannes Hölzl (Jun 06 2019 at 18:39):

The paper seams to refering to this Coq project: https://github.com/slasser/vermillion

#### Patrick Massot (Jun 06 2019 at 19:07):

Did you see https://www21.in.tum.de/~wimmers/proofground/? @Mario Carneiro we need you!

#### Mario Carneiro (Jun 06 2019 at 19:09):

You want me to write a proof problem or play the game?

#### Kevin Buzzard (Jun 06 2019 at 19:15):

I once managed to get a problem onto the IMO!

#### Kevin Buzzard (Jun 06 2019 at 19:15):

I quite like the idea of coming up with some problems.

#### Patrick Massot (Jun 06 2019 at 19:22):

We need you to get Lean to win the contest!

#### Patrick Massot (Jun 06 2019 at 19:23):

Now you know Kevin will submit problems, you can train on sample Langlands program riddles.

#### Mario Carneiro (Jun 06 2019 at 19:26):

is kevin going to trick me into solving langlands conjecture or something?

#### Kevin Buzzard (Jun 06 2019 at 19:26):

that would be good

#### Kevin Buzzard (Jun 06 2019 at 19:26):

Maybe tricking you to solving 3x+1 would be easier

#### Patrick Massot (Jun 06 2019 at 19:27):

I need to suggest defining Lebesgue integral

#### Mario Carneiro (Jun 06 2019 at 19:32):

defining the real lebesgue integral (by breaking into positive and negative parts) would probably be a half hour project given the ennreal integral

#### Patrick Massot (Jun 06 2019 at 19:33):

Do we really need this contest to get it done then?

#### Mario Carneiro (Jun 06 2019 at 19:33):

It's not in mathlib because it's overcomplicated and worthless

#### Mario Carneiro (Jun 06 2019 at 19:33):

but it's not hard to do

#### Patrick Massot (Jun 06 2019 at 19:36):

How can it be half an hour and overcomplicated?

#### Kevin Buzzard (Jun 06 2019 at 19:38):

The only question Martin Hairer ever asks me about Lean is "have you guys got the Gaussian measure yet?"

#### Kevin Buzzard (Jun 06 2019 at 19:39):

So someone who knows what it is could do that at some point, so I could finally tell him yes and we could find out what Q2 is

#### Reid Barton (Jun 06 2019 at 19:42):

I think at this point it just needs typing in

#### Patrick Massot (Jun 06 2019 at 19:47):

Let me return to the main topic of this thread today (Lean papers in ITP). It's probably obvious to computer scientists, but I prefer to write it just in case. As was pointed out to the perfectoid team, forgetting to write that Lean is developed at Microsoft research is not helping to keep Lean funded. So everybody should make sure their papers and slides mention Microsoft research.

#### Mario Carneiro (Jun 06 2019 at 19:47):

I think that's one of the things @Koundinya Vajjha is working on (gaussian measure)

#### Tim Daly (Jun 06 2019 at 23:20):

Is there any effort to collect and catalog copies of all Lean papers? I would be willing to maintain a bibtex bibliography of papers. One of the key problems of doing "independent research" (as I am) is that papers get locked behind paywalls or lost due to authors leaving the field.

#### Rob Lewis (Jun 07 2019 at 00:02):

We have the website at https://leanprover-community.github.io/ that isn't doing anything beyond hosting the Zulip archive right now. This would be a good place to collect mathlib-based papers.

#### Tim Daly (Jun 07 2019 at 00:05):

A 0-th level try is here: http://axiom-developer.org/leanbib.tex

I don't have write access to the leanprover github. It would be nice to host copies of the papers there also.

#### Tim Daly (Jun 07 2019 at 00:57):

Who controls this website?

#### Mario Carneiro (Jun 07 2019 at 01:03):

I think the leanprover-community maintainers all have access, but Rob set it up

#### Mario Carneiro (Jun 07 2019 at 01:04):

Would you like write access to mathlib? We give it out to whoever wants it

#### Tim Daly (Jun 07 2019 at 01:11):

I'd like write access to someplace where people would expect to find a lean bibliography (e.g. a link on the leanprover-community page. Anybody with write access could then add bibliographic entries to their (or other's) papers. A central resource for finding biblio links would make it easier to cite papers. A central repository of copies of the papers would mean that your bibliography could also include a hyperlink.

#### Rob Lewis (Jun 07 2019 at 01:26):

You can make a pull request to the leanprover-community repo. (https://github.com/leanprover-community/leanprover-community.github.io)

#### Rob Lewis (Jun 07 2019 at 01:27):

I'm a little hesitant to hand out write access, because accidental changes to the archive part of the site might break the auto-updates.

#### Tim Daly (Jun 07 2019 at 02:18):

In theory I've created a correct pull request.

#### Kevin Buzzard (Jun 07 2019 at 07:23):

I commented, including inviting people here ...

I note that a discussion began in the comments at Woit's blog .

I regard this sort of thing (online chat) as not unimportant. I have had over 1000 blog views in the last thee days, just from the fact that he mentioned my blog (the wordpress software tells me that people are clicking on his link) so I think we can assume (if we didn't know already) that Woit's blog is very widely read. If people feel that they have something to say about the issues being discussed there and want to contribute, I can pretty much guarantee that there is an audience reading it.

The reason they're not unimportant is that I am still convinced that the mathematical community is still overwhelmingly completely ignorant of software like Lean, and the more "chat" about it, the better.

#### Simon Hudon (Jun 07 2019 at 12:38):

(note: I think mathlib has a lemma to simplify this not_unimportant : ¬ unimportant ↔ important)

#### Kevin Buzzard (Jun 07 2019 at 12:55):

I think this argument assumes the law of the excluded middle.

#### Simon Hudon (Jun 07 2019 at 15:40):

I usually do assume the excluded middle. Have you been spending a lot of time with Kenny?

#### matt rice (Jun 07 2019 at 16:07):

def unimportant := true
def important := false
def not_unimportant : ¬ unimportant ↔ important
:= iff.intro
(λ _ : ¬unimportant,
have  ¬true → false, from (λ h, h $by trivial), have unimportant = true, by refl, have ¬true, from (eq.substr ‹unimportant = true› ) ‹¬ unimportant›, show important, from ‹¬ true → false› ‹¬ true› ) (λ _ : important, false.elim ‹important›) #print axioms not_unimportant  i'm still not convinced nihilism is all that constructive though #### Tim Daly (Jun 08 2019 at 07:22): Leonardo de Moura at PLSE 2016: The Lean Theorem Prover https://www.youtube.com/watch?v=69ytTKfSSgc #### Kevin Buzzard (Jun 13 2019 at 08:29): https://galoisrepresentations.wordpress.com/2019/06/12/harris-versus-buzzard/ #### Kevin Kappelmann (Jun 13 2019 at 09:30): Is that face-off on the 20th of June in Paris recorded by any chance? #### Johan Commelin (Jun 13 2019 at 09:32): I don't know, but if it's in France it will probably be dubbed in French #### Kevin Buzzard (Jun 14 2019 at 15:29): https://www.youtube.com/watch?v=aZHbnQlFOn4 My general audience talk with a bunch of Lean in. #### Tim Daly (Jun 14 2019 at 16:23): re; Squares Tessellate Tait, "Truth and Proof: The Platonism of Mathematics" http://logic.harvard.edu/EFI_Tait_PlatonismInMathematics.pdf #### Kevin Buzzard (Jun 26 2019 at 12:54): https://itp19.cecs.pdx.edu/accepted-papers/ 5 Lean papers at ITP, not bad https://itp19.cecs.pdx.edu/invited-speakers/ So now 6 Lean talks ;-) #### Reid Barton (Jun 26 2019 at 13:16): Do you know what you'll talk about, or will you decide at 3 AM the night before? #### Kevin Buzzard (Jun 26 2019 at 13:28): I was thinking of talking about what makes a mathematician tick. #### Kevin Buzzard (Jun 30 2019 at 22:22): https://twitter.com/derKha/status/1145412656632930304 #### Scott Morrison (Jun 30 2019 at 22:37): I use \mapsto inside an expression. #### Simon Hudon (Jun 30 2019 at 22:40): I don't like the idea that there would be significant notational differences between for all and lambda. I think we shouldn't have a completely different syntax for each binder. If we pick ., we should use it for forall, exists, etc #### Jesse Michael Han (Jun 30 2019 at 22:42): One of Lean's syntactic idiosyncrasies is the use of a comma separator in lambdas and other binders. one of my reviewers complained about this exact thing: How is this tuple parsed? For me it looks like a 5-uple! Apparently, Lean has some magic binding rules where the comma gets a different binding strength if it was preceded by a λ!? ... [What were the designers of Lean thinking here??]  in retrospect, it is indeed hilarious: def check : (pSet : Type (u+1)) → bSet 𝔹 | ⟨α,A⟩ := ⟨α, λ a, check (A a), λ a, ⊤⟩  #### Reid Barton (Jun 30 2019 at 22:53): Yeah, I also noticed how crazy/ambiguous-looking the , , , syntax is when trying to explain some Lean code to a non-Lean user #### Reid Barton (Jun 30 2019 at 22:54): But I don't have a Twitter account so I don't get a vote :not_allowed: :bird: #### Andrew Ashworth (Jun 30 2019 at 23:53): Yeah, I can't vote either. But the traditional separator is the period, so I'd vote for that. And it should also be used for all the other logical quantifiers, like Simon mentioned. #### Reid Barton (Jul 01 2019 at 00:03): if we're thinking outside the box syntaxwise, a lot of people wouldn't mind having the Greek letter λ available as a variable name #### Simon Hudon (Jul 01 2019 at 00:14): from the perspective, \mapsto doesn't use a letter so that frees up lambda but it does use an arrow which we always seem to run out of. Plus, my aforementioned point about homogeneity #### Reid Barton (Jul 01 2019 at 00:21): there are also some alternative Unicode lambdas (see under "Mathematical Lambda" at https://en.wikipedia.org/wiki/Lambda) but I don't know how well supported they are #### Simon Hudon (Jul 01 2019 at 00:48): We could keep the same lambda for functional abstractions and let people find other unicode lambdas for their local purposes #### Mario Carneiro (Jul 01 2019 at 02:12): I would actually prefer to use backslash than unicode lambda (but with lambda available as alternate notation). It would be nice if the core syntax didn't use so much unicode, since this makes it difficult for those that don't want to use a lean-approved editor #### Simon Hudon (Jul 01 2019 at 02:14): Does that issue arise often? #### Johan Commelin (Jul 01 2019 at 02:14): Well, maybe we don't hear those users, because they don't even consider Lean atm... #### Johan Commelin (Jul 01 2019 at 02:14): Is .\ a faithful ASCII rendition of lambda? #### Johan Commelin (Jul 01 2019 at 02:15): .\ x. e :scream_cat: #### Johan Commelin (Jul 01 2019 at 02:16): Btw, I would be a fan of having infix \mapsto available. It's used all over the place in maths, so it doesn't feel like "sacrificing" an arrow. #### Scott Morrison (Jul 01 2019 at 02:17): Yeah --- I'd be pretty upset seeing someone use \mapsto to mean anything else, so arguably it's already taken. #### Mario Carneiro (Jul 01 2019 at 02:27): I would be happy to see \mapsto, although it might be tricky to parse #### Keeley Hoek (Jul 01 2019 at 02:35): ATTACK OF ZE SEMICOLONS #### Keeley Hoek (Jul 01 2019 at 02:35): https://github.com/leanprover/lean4/commit/5c4ec3082099a7e1b008ced0db162c7cac16663a #### Mario Carneiro (Jul 01 2019 at 02:42): Sigh. I wish there weren't so many meaningless syntax changes. I don't really care what the syntax is, but I like consistency and these changes should be considered in the light of all the people that will have to learn the new syntax. I hope there is at least a rationale posted for all these things at some point #### Tim Daly (Jul 01 2019 at 03:06): Guy Steele on logic notation: https://www.youtube.com/watch?v=dCuZkaaou0Q #### Tim Daly (Jul 01 2019 at 03:12): For example, does [x/y]e mean substitute x for y in e or substitute y for x in e? Guy did a survey. #### Andrew Ashworth (Jul 01 2019 at 04:38): I would actually prefer to use backslash than unicode lambda (but with lambda available as alternate notation). It would be nice if the core syntax didn't use so much unicode, since this makes it difficult for those that don't want to use a lean-approved editor there are non-unicode alternatives for lambda, though? Just like coq, I think you can type fun or assume for lambda, and so forth. The implication arrow is the very awesome ->. I mean, you probably know this, so I'm not quite following. #### Patrick Massot (Jul 01 2019 at 09:10): For example, does [x/y]e mean substitute x for y in e or substitute y for x in e? Guy did a survey. This issue is what confused me every single time I read or watched explanations about lambda-calculus. #### Patrick Massot (Jul 01 2019 at 09:16): I'm very close to creating a Twitter account only for the purpose of voting here. @Sebastian Ullrich wouldn't it make more sense to have a GitHub vote? You could created and issue with one message per proposition, and we can use the emoji reactions to vote. I think the period option is really awful. I don't know any language (I mean real language, not programming language) where period is used for anything else than ending a sentence. In what sense does λ x. eends after x?!? Of course every mathematician would vote for x ↦ e but I'd be happy to keep λ x, e if it is important for CS people. #### Keeley Hoek (Jul 01 2019 at 09:38): (x : nat, y : int) ↦ x + y #### Keeley Hoek (Jul 01 2019 at 09:39): The java compiler can parse that #### Keeley Hoek (Jul 01 2019 at 09:39): (I mean an isomorphic expression) #### Sebastien Gouezel (Jul 01 2019 at 10:08): Period is used in Isabelle. It took me a lot of time to get used to the comma in Lean, and in the end I think I prefer the period because the comma is already used to separate expressions in anonymous constructors. My point is rather that I would like to have two different symbols here, be it . , or , ; say. #### Sebastian Ullrich (Jul 01 2019 at 10:17): @Patrick Massot The wording of the poll should imply that it isn't meant to be taken very seriously, nor will its outcome influence our decision #### Sebastian Ullrich (Jul 01 2019 at 10:27): @Sebastien Gouezel I'm not convinced we should unnecessarily include syntax variations (ASCII alternatives are quite useful, OTOH). In practice, whatever syntax TPIL uses will be used by 95% of all users. But you're welcome to override the builtin notation in Lean 4 if you want to. #### Patrick Massot (Jul 01 2019 at 11:24): What about using python's λ x: e? At least it's not a period #### Andrew Ashworth (Jul 01 2019 at 11:30): we can make everybody unhappy and do λx ↦ e #### Simon Hudon (Jul 01 2019 at 19:26): @Andrew Ashworth That looks dicey. To be sure everyone is unhappy, let's put the lambda at the end #### Simon Hudon (Jul 01 2019 at 19:28): @Patrick Massot I'm not too wild about this possibility because : is also used for type annotations. λ v : e : e would be valid and possibly ambiguous. You could require brackets around v : e but I prefer those brackets to be optional #### Johannes Hölzl (Jul 01 2019 at 20:02): @Sebastian Ullrich I think Sebastien didn't mean two syntaxes at the same time, but to have a syntax where the tuple "comma" is different from the binder "dot". #### Johannes Hölzl (Jul 01 2019 at 20:03): While I would also prefer the " fun x. t" instead of "fun x, t" I think this would be another unnecessary syntax change. #### Sebastian Ullrich (Jul 01 2019 at 20:05): I think Sebastien didn't mean two syntaxes at the same time, but to have a syntax where the tuple "comma" is different from the binder "dot". Ah, I see. #### Marc Huisinga (Jul 01 2019 at 20:12): would it really be that difficult to (possibly automatically) convert the old syntax to a new syntax in all important lean resources? are there many existing lean resources that cannot be easily converted? #### Jeremy Avigad (Jul 01 2019 at 20:13): I like the period, but probably because it is common in the CS literature and I have gotten used to it. @Patrick Massot here in the US we write 3.1415... I guess you Europeans sometimes write 1.000.000 for one million. #### Jeremy Avigad (Jul 01 2019 at 20:14): It is possible to get used to anything. #### Tim Daly (Jul 01 2019 at 20:38): The problem is that this isn't fully "a free choice", since some of these will eventually be published in papers and books. Hopefully the syntax can be understood by non-lean readers. #### Patrick Massot (Jul 01 2019 at 20:38): No, we use 1 000 000. #### Rob Lewis (Jul 17 2019 at 11:34): This might not count as "in the wild" since it's from MSR, but: https://sf.snu.ac.kr/aliveinlean/ https://sf.snu.ac.kr/publications/aliveinlean.pdf #### Andrew Ashworth (Jul 17 2019 at 22:48): ooh, if I have time, I want to check this out #### Andrew Ashworth (Jul 17 2019 at 22:53): right now I'm researching how much work it would be to write a program that traverses Clang ASTs and feeds floating point expressions to Herbie, and then spit out the analysis. So maybe not directly related, but somewhat... #### Kevin Buzzard (Jul 19 2019 at 08:16): https://arxiv.org/abs/1907.07801 #### Bryan Gin-ge Chen (Jul 19 2019 at 12:15): The relevant code seems to be here: https://github.com/NeilStrickland/itloc #### Koundinya Vajjha (Jul 20 2019 at 13:03): In particular, we have implemented interaction with the lean theorem prover, whereby the export format of lean is used (via trepplein) to generate code in our implementation of HoTT. This allows us to start with a library for learning as well as a target for natural lannguage processing. http://siddhartha-gadgil.github.io/ProvingGround/ #### Neil Strickland (Jul 22 2019 at 10:29): I'd be interested in thoughts about the arrangement of code for this sort of thing. I think it's desirable to have a static snapshot on the arxiv and a maintained repository on github. Certainly some of the code on my github repository could move into mathlib. We could have a policy and/or aspiration that all code supporting a published paper should move into mathlib. Or we could have a separate repository for that purpose, but still under leanprover-community and set up with travis so we can maintain compatibility with mathlib. #### Andrew Ashworth (Jul 22 2019 at 10:48): It's a little ambitious to expect everybody to keep their code up to date. An arxiv submission should contain git hashes of any dependent packages. Probably also a specific Lean version number too, in order to ensure reproducibility, maybe using Elan? Then even if the paper is read years later the code should still work without squiggly lines. #### Andrew Ashworth (Jul 22 2019 at 10:57): It would be best if ArXiv would host everything needed to make a reproducible paper, but I can imagine the storage costs would be immense, especially for papers in physical science with large datasets... :/ #### Floris van Doorn (Aug 05 2019 at 20:43): On The FOM (foundations of mathematics) mailing list there is a short thread about the NP = PSPACE problem. People are trying to formalize their claimed proof that NP = PSPACE in Lean: In order to avoid incomplete versions, I and my students, are formalizing our version in LEAN. Only after each relevant part is formalized and checked there will be an article published it in arxiv According to Wikipedia, this claim is "widely suspected" to be false. #### Kevin Buzzard (Sep 02 2019 at 16:13): I wrote a short piece about Lean for the London Mathematical Society newsletter, and it has just appeared: https://www.lms.ac.uk/sites/lms.ac.uk/files/files/NLMS_484_for-web_0.pdf (pages 32 to 36). #### Johan Commelin (Sep 02 2019 at 16:34): @Kevin Buzzard Gijswijt's name is missing on p33 #### Kevin Buzzard (Sep 02 2019 at 17:23): Noo! #### Kevin Buzzard (Sep 02 2019 at 17:23): :-( #### Kevin Buzzard (Sep 02 2019 at 17:26): Well it's only missing once, it is there the second time, and it's also clearly a typo rather than me claiming that it's Ellenberg only because of the dangling "and". #### Kevin Buzzard (Sep 02 2019 at 17:28): Oh! Gijswijt's name is in the version I sent them! So they have removed it for some reason -- as well as making the Lean code on p32 look a bit horrible (this is some png rescaling issue perhaps). #### Johan Commelin (Sep 02 2019 at 17:30): Wow, that's some really good editing! #### Kevin Buzzard (Sep 02 2019 at 17:32): The London Mathematical Society runs on a shoestring. #### Johan Commelin (Sep 02 2019 at 17:32): Can they still fix it? Or is it already printed? #### Kevin Buzzard (Sep 02 2019 at 17:33): I have no idea. I'll ask. #### Kevin Buzzard (Sep 04 2019 at 03:50): It will be fixed online when people are back from holidays #### Reid Barton (Sep 05 2019 at 13:47): If minor edits are still relevant: "It is just is a" near the end of the first page #### Kevin Buzzard (Sep 05 2019 at 14:19): Thanks. The person who's making the changes is away until Monday so I believe I might still be able to get this fixed. #### Olli (Sep 26 2019 at 16:06): https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually #### Kevin Buzzard (Sep 26 2019 at 16:07): ?? How did they get from "I think there is a non-zero chance that some of our great castles are built on sand" to "Number Theorist Fears All Published Math Is Wrong" ?? @Rob Lewis this is the guy we were talking about at ITP. #### Kevin Buzzard (Sep 26 2019 at 16:07): That's just a completely click-baity title which does not represent my views. #### Olli (Sep 26 2019 at 16:10): Yep, I ran into it on Twitter posted by a non-mathematician, clearly it is clickbait and how they get their clicks and their ad revenue #### William Whistler (Sep 26 2019 at 16:18): “I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,” Buzzard told Motherboard while he was attending the 10th Interactive Theorem Proving conference in Portland, Oregon, where he gave the opening talk. #### William Whistler (Sep 26 2019 at 16:18): Is that a made-up quote? #### Kevin Buzzard (Sep 26 2019 at 16:20): How can I check? :-/ I was in a hotel room in Portland talking to him on the phone. It's not very good English, that's for sure. #### William Whistler (Sep 26 2019 at 16:23): Hard at this point, if you don't remember or have a record. They might've rolled their question and your response into the quote, or something like that. #### Kevin Buzzard (Sep 26 2019 at 16:23): Well, we live and learn :-/ #### Rob Lewis (Sep 26 2019 at 16:23): Heh, it's not the worst thing Vice has ever published. #### Kevin Buzzard (Sep 26 2019 at 16:23): :-) #### William Whistler (Sep 26 2019 at 16:26): Even "arguing that we must begin to rely on AI to verify proofs" is quite clickbaity. Not all software is AI, for heaven's sake. #### Simon Hudon (Sep 26 2019 at 16:59): But to be fair, Kevin does put a lot of software in the same basket, going so far as to ask "Why isn't Lean smart enough to figure it out?" inviting the classification of interactive provers as AI technology #### Jeremy Avigad (Sep 26 2019 at 23:44): I had the foresight to ask him to check back with me over any quotes he wanted to use. So at least I sound sane (if not nearly as exciting). #### Johan Commelin (Sep 27 2019 at 04:44): @Kevin Buzzard Time for a rectification blogpost? :grimacing: :wink: #### Johan Commelin (Sep 27 2019 at 04:55): I'm not so much concerned about the general public, or clickbaity titles. More about the mathematical community that doesn't speak with you on a daily basis. #### Kevin Buzzard (Sep 27 2019 at 07:13): I'm a bit snowed under at the minute, teaching starts next week, but I'll see what I can do #### Kevin Buzzard (Sep 27 2019 at 11:19): I'm not so much concerned about the general public, or clickbaity titles. More about the mathematical community that doesn't speak with you on a daily basis. I think you're probably more concerned than I am :-) I think that when I was younger I would have been running around panicking, but now I understand the internet much better and it seems to me that most Lean stuff on the internet is sane, and then this one piece is a bit more extreme but it will just disappear into the general noise. I think much more interesting is Frank Calegari's claim that some humans completely understand the proof of Fermat's Last Theorem, so I wrote a blog post about that instead. What do you think @Johan Commelin ? I can't quite work out if you're being serious. I mention the Vice article a bit at the beginning. https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ #### Johan Commelin (Sep 27 2019 at 11:33): @Kevin Buzzard I think the first paragraph of your blogpost settles it in a nice and relaxed way (-; #### Johan Commelin (Sep 27 2019 at 11:42): But Frank hasn't provided a proof of his counterclaim. Not even a "mathematical" proof (-; #### Patrick Massot (Sep 27 2019 at 14:10): I just ran into François Charles in the corridor and stopped me to tell me: "I saw in newspapers that your collaborator says every maths is wrong". He was smiling though. #### Kevin Buzzard (Sep 27 2019 at 14:16): What can you do :-) Given that you yourself found omissions in Bourbaki, maybe all maths _is_ wrong :-) #### Patrick Massot (Sep 27 2019 at 14:17): Of course François heard about this on Twitter. Did you put links to your blog post there? #### Kevin Buzzard (Sep 27 2019 at 14:23): Yes. #### Joe Hendrix (Sep 27 2019 at 18:12): I think reporters generally run with quotes they think they need to drive views. Being very measured in responses just means no news. #### Chris Hughes (Sep 27 2019 at 22:36): My phone showed me this today https://www.popularmechanics.com/science/math/a29252622/is-math-wrong/ #### Kevin Buzzard (Sep 28 2019 at 12:39): Good to see it mentions Lean! #### matt rice (Sep 28 2019 at 15:52): I guess my interest in proof checking stems from a very different thing, where we have a general proof that something is (unprovable? -- i dont want to say false), but in special cases can be proven true, the general cases tend to throw shade on the special case, and the special case tends to require a lot of setup... It's probably best if I just give an example... like the idea that nand has no inverse and loses information, but in the case where nand is the partial application of a reversible universal logic gate like a fredkin gate, or a toffoli gate the complete gate has an inverse. I like proof checkers for their ability to convey all these special assumptions, when trying to convey a counterintuitive truth ... This is somewhat the dual of Kevin's what if its false when we think it true I guess. #### Jesse Michael Han (Sep 29 2019 at 17:03): kevin just hit # 1 on hacker news: https://news.ycombinator.com/item?id=21107706 #### Kevin Buzzard (Sep 29 2019 at 21:17): Amazing what a clickbait headline can do! #### Kevin Buzzard (Sep 29 2019 at 21:17): TPIL is #12! That's a good thing. #### Kevin Buzzard (Sep 29 2019 at 21:23): What I am manifestly relieved about is that most people actually seem to be completely avoiding saying "this guy is clearly an idiot, clearly all published maths is not wrong". It's like today's kids are somehow immune to the clickbait, or forget it instantly or something. #### Kevin Buzzard (Sep 29 2019 at 21:37): Oh! Because of hacker news rules, apparently they changed the headline from the clickbaity one to "Number theorist fears many proofs widely considered to be true are wrong ". That's closer to the truth, but perhaps "some proofs" would be better. #### Kevin Buzzard (Sep 29 2019 at 21:43): The whole thing is great. People are talking about Lean, people are talking about theorem provers, this is just what we need to get young people interested in the area. #### Johan Commelin (Sep 30 2019 at 09:13): This comment from Hacker News is quite a marvel: IMO the final paper had too much technical jargon which was convoluting some simple concepts. This is symptomatic of IMHO the biggest single problem with the world of mathematics today. This discipline should be about developing ideas based on rigorous foundations and logic, which is a useful and important purpose. Once you have understood those ideas, even "advanced" results often seem quite simple and intuitive, and we can take that understanding and apply it to other work if helps us to make useful progress. However, the amount of needlessly obscure terminology, poor notation and just plain bad writing in formal papers make the whole field absurdly inaccessible, even to many who might have no trouble understanding the underlying concepts and important results. Just imagine what would happen if we tried to write engineering specs or software the way postgraduate mathematics research is done. We'd be trying to debug source code where every identifier was a single character, taken from one of three or four different alphabets, with several of them looking similar enough to mistake one for another, with a bunch of combining accent modifiers on top that were used to fundamentally change the semantics of the program, interspersed with comments by someone who needs a remedial class in basic writing skills, full of technical terminology that is defined in terms of other technical terminology from other software packages, except that sometimes the meaning is subtly different in this context but that isn't noted anywhere on the screen at the time, resulting in needing to spend half an hour doing a depth-first-search of all the definitions only to find that a function whose only identifier is the name of the developer who wrote the second version (because the first person to work on it already has another function bearing their name) is actually equivalent to what a programmer would write as const DAYS_IN_WEEK := 7  I write this as someone who studied mathematics to a high level and has touched on the field many times since in connection with heavily mathematical software development. It's the worst sort of closed-world gate-keeping, and we could do so much better, but sadly inertia and vested interests are not our friends in this matter. https://news.ycombinator.com/item?id=21109440 #### Tim Daly (Sep 30 2019 at 10:58): Mathematica won in the computer algebra field for a simple reason. It had the best documentation. The learning curve for any computer algebra system is quite steep and all of the other systems relied on "learn by trial". Now look at Lean. Take, for example, group.lean. It is a wall of text. Finding a theorem relies on odd names like mul_eq_of_eq_inv_mul. The whole of the "communication" with people, such as it is, is contained in that name. Programmers made the mistake of this "pile of sane" (POS) approach, witness the "src", "inc", "tst", and (usually empty) "doc" directories with "semantic naming" like parser.c, SMTFuns.pl, or catsim.ml. Suppose, instead, there was a group theory textbook in latex. The textbook explains the ideas in natural language. It contains all of the lemmas in group.lean, each one with a paragraph or so of explanation. The lemmas are in named "chunks", basically a verbatim block with a name. Lemmas should only be accepted when they contain a paragraph or section in the group theory volume. Now you have a book, with a table of contents, a table of equations, chapters, sections, paragraphs, an index, and a bibliography, all hyperlinked and searchable. Since each lemma is in a named verbatim chunk you can extract any or all lemmas automatically, letting the compiler do it. You can find relevant lemmas by looking in the table of contents or the index. Code to extract a named chunk is 170 lines of C. Axiom already uses this technology. The idea is called "literate programming" (Knuth). You write for people, and incidently, write for the machine. And, as a benefit, you get a book to publish, which counts on your resume rather than a file of code that doesn't. #### Tim Daly (Sep 30 2019 at 11:00): "pile of sand" (POS) ... #### Johan Commelin (Sep 30 2019 at 11:01): I'm quite happy that 20 pesky little trivial lemmas all fit on one screen. If all of those trivialities came with a paragraph of documentation, I think it would be harder to find something for me. #### Johan Commelin (Sep 30 2019 at 11:01): Mathlib is currently in the process of documenting definitions and major theorems #### Tim Daly (Sep 30 2019 at 11:01): How long have you been using Lean? #### Johan Commelin (Sep 30 2019 at 11:01): But I think one can go overboard on the other side #### Johan Commelin (Sep 30 2019 at 11:02): There was a time when I had not yet used Lean for a very long time... #### Johan Commelin (Sep 30 2019 at 11:03): Documentation is important. But it's not the reason why mathematicians aren't jumping on board. It simply isn't #### Tim Daly (Sep 30 2019 at 11:03): It took me 10 courses and 3 years to be able to read current research papers, many of which contain whole pages of nothing but greek rules. #### Johan Commelin (Sep 30 2019 at 11:04): And if I ask the mathematician in the office next to me why he doesn't use Lean, he'll ask me... do you have the K-theory of coherent sheaves on a scheme? #### Johan Commelin (Sep 30 2019 at 11:04): If I ask someone on the floor below me, they'll want to know if special holonomy groups are in our library... #### Johan Commelin (Sep 30 2019 at 11:04): Etc... #### Tim Daly (Sep 30 2019 at 11:05): I'm one of the authors of Axiom. Axiom was a commercial competitor to Mathematca and Maple. It was considered "one of the big 3". I got a lot of feedback from professors who taught using computer algebra, including those who contributed to Axiom. Documentation mattered for teaching and students kept using what they knew. #### Johan Commelin (Sep 30 2019 at 11:05): That's the main obstruction. The fact that we don't have étale cohomology groups, or even just the discriminant of a number field, or whatever. #### Tim Daly (Sep 30 2019 at 11:08): Take a calc textbook. Shake out all of the equations and paste them on index cards. Throw away the words. Now teach calculus from the index cards. The group.lean file is "just the equations", i.e. just the index cards. If all of mathematics were reduced to a wall of 200-character named lemmas I'm not sure it would get much use. #### Kevin Buzzard (Sep 30 2019 at 11:10): I don't know who's right. My experience talking to mathematicians is the same as Johan -- they're not interested because the things they do aren't there. However in 5 years' time when they are there, documentation will most definitely be an issue. Whether it contributes now or not is something I don't know. I am trying to write documentation for maths undergraduates, but progress is slow because I have a busy job :-/ #### Tim Daly (Sep 30 2019 at 11:11): I can read group.lean because I've done group theory for years. I have no idea what the other lemmas mean or how to use them. #### Johan Commelin (Sep 30 2019 at 11:11): Take an introductory textbook on group theory. Shake out all the theorems and lemmas and paste them on index cards. Throw away all the words. Now try to find a corresponding entry for each index card in group.lean. For >50% of the index cards, you won't find an entry. On the other hand, for 90% of the lines in group.lean, you won't find an index card... #### Tim Daly (Sep 30 2019 at 11:13): I'm suggesting that the "library" format for lean is books, not files. Of course the group theory "book" would be written to hold the current lemmas surrounded by paragraphs (useful for word searching). New lemmas would update the book. I'm not suggesting "decorating" an existing group theory book with the lemmas. #### Tim Daly (Sep 30 2019 at 11:16): Latex was written in lterate programming style in the 70s and is still maintained, mostly because you can read and understand it. Almost every program I've written in the last half century is gone, despite being quite useful for current things, such a remotely monitoring data centers. #### Johan Commelin (Sep 30 2019 at 11:16): If only Knuth were to write an ITP... #### Tim Daly (Sep 30 2019 at 11:17): Or a text that explains BDDs for solvers :-) #### Johan Commelin (Sep 30 2019 at 11:18): Tim, how is Lean different from Coq, Isabelle, whatever? Why are there more pure mathematicians in this small and young community than in the others? #### Tim Daly (Sep 30 2019 at 11:18): The documentation problem isn't a problem now. It shows up as a problem once the origianl authors leave the project. Witness the tens of thousands of dead projects on github, sourceforge, and savannah. #### Tim Daly (Sep 30 2019 at 11:20): Well, Benjamin Pierce taught COQ courses in Oregon, which is where I started learning it. And he has a textbook which I can use. #### Johan Commelin (Sep 30 2019 at 11:20): Many math papers and textbooks are "dead" in that sense. Also, it doesn't answer my question. #### Johan Commelin (Sep 30 2019 at 11:20): The average math paper from <1950s is unreadable for us. #### Tim Daly (Sep 30 2019 at 11:21): Yeah, I struggled with Frege's papers due to notation #### Keeley Hoek (Sep 30 2019 at 11:22): One clear problem is that probably 5% to at most 10% (just a guess, an authority can jump in if they please) of the lemmas in mathlib are actually even stated in a mathematics book. At the very least, in mathlib proofs of important and hard, "real", propositions and theorems are often chopped up in order to remain manageable. I think just the act of stating many of the broken-up pieces as they are phrased in lean would be totally unbearable to read in a mathematics book. Imagine, for example, such a direct translation of https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/sylow.lean So much is "obvious". That's not even to say it's not worth checking---it just stands in the way of understanding. #### Tim Daly (Sep 30 2019 at 11:22): But then I've struggled with recent papers for the same reason (look up Guy Steele's talk on logic notation) #### Tim Daly (Sep 30 2019 at 11:24): Keeley, lemmas are where proofs get creative. A few words about why it is needed gives a clue but a few lines of Lean does not. #### Johan Commelin (Sep 30 2019 at 11:24): Tim, that's simply not true #### Johan Commelin (Sep 30 2019 at 11:25): There are dozens of lemmas in the library that are exactly the opposite of being creative #### Johan Commelin (Sep 30 2019 at 11:25): They are there only to handhold the system #### Mario Carneiro (Sep 30 2019 at 11:25): I think you mean "thousands" #### Johan Commelin (Sep 30 2019 at 11:26): Usually, page of code after a new definition is just scaffolding. Stuff that mathematicians don't even unconsciously think about when writing a detailed introductory text. #### Mario Carneiro (Sep 30 2019 at 11:26): I would say not that they are handholding for the system, rather they are there to bring the system up to a basic level of competence, so that you don't have to worry about extremely piddling details for your next project #### Johan Commelin (Sep 30 2019 at 11:27): Right, that's a better way of putting it #### Tim Daly (Sep 30 2019 at 11:27): Well, it will then grow into the millions if Kevin Buzzard's dream comes true. #### Mario Carneiro (Sep 30 2019 at 11:27): "mathlib does the piddling details so you don't have to" #### Mario Carneiro (Sep 30 2019 at 11:28): group.lean is not group theory. It is basic highschool algebra #### Mario Carneiro (Sep 30 2019 at 11:28): nothing in that file has a name in math #### Mario Carneiro (Sep 30 2019 at 11:28): it is not representative of all of math #### Tim Daly (Sep 30 2019 at 11:29): Does it have an "idea" in math? And is that "idea" properly communicated in 16 characters? #### Mario Carneiro (Sep 30 2019 at 11:29): although coming from a CAS background you might become disproportionately interested in that material #### Mario Carneiro (Sep 30 2019 at 11:30): but mathematicians are looking much further afield #### Mario Carneiro (Sep 30 2019 at 11:30): no, it does not have an "idea" #### Mario Carneiro (Sep 30 2019 at 11:30): its meaning is completely described by the statement of the theorem itself #### Mario Carneiro (Sep 30 2019 at 11:30): a * (a^-1 * b) = b is just that #### Mario Carneiro (Sep 30 2019 at 11:31): you can give the property a name if you want, but it's just a thing that is true #### Marc Huisinga (Sep 30 2019 at 11:31): but even if it does grow to millions, most of those lemmas wouldn't benefit much from extensive documentation. i suppose the normal workflow is the following: you encounter a technical issue in one of your proofs that is intuitively obvious but would be bothersome to prove. you use library_search or some other lemma search tool to resolve the technicality, and then go on with your proof. there's really not much beyond the lemma type that matters. #### Tim Daly (Sep 30 2019 at 11:31): I'm just trying to suggest that there might be methods for the Lean project to survive once the original authors leave. 10,000 lemmas in flat files like group.lean is completely unmaintainable. #### Mario Carneiro (Sep 30 2019 at 11:32): again, group.lean is not representative #### Mario Carneiro (Sep 30 2019 at 11:32): look around #### Mario Carneiro (Sep 30 2019 at 11:32): documentation is much more important in places where it's not bleeding obvious why the theorem is true #### Tim Daly (Sep 30 2019 at 11:33): Are you suggesting that there ARE books in Lean? #### Mario Carneiro (Sep 30 2019 at 11:33): TPIL? #### Tim Daly (Sep 30 2019 at 11:33): I'm reading that. #### Tim Daly (Sep 30 2019 at 11:34): Ah, well. I'm done. #### Mario Carneiro (Sep 30 2019 at 11:35): I have heard a lot of praise for that book, specifically as it relates to documentation making it easy to get into lean #### Mario Carneiro (Sep 30 2019 at 11:35): I think we are all aware of the importance of documentation, and there is a push for more high level documentation in mathlib #### Johan Commelin (Sep 30 2019 at 11:36): Tim, I am sincerely interested in your thoughts on why there are disproportionately many pure mathematicians in the Lean community compared to other prover-communities. Even though Lean is the youngest of them all. #### Tim Daly (Sep 30 2019 at 11:39): I'm in "the lean community" because Jeremy Avigad taught a class, so I know how to use it. I want to use it underneath Axiom as my proof engine and Jeremy has been most helpful with that. Without Jeremy's help I probably couldn't even read the group.lean file. #### Tim Daly (Sep 30 2019 at 11:41): Axiom has over 10,000 functions and 1100 "typeclasses". I fully understand how hard it is to maintain the mathematics, the compiler, and the interpreter. Why when I open-sourced Axiom, it had about 3 useful comments in total. Who would possibly need more? #### Tim Daly (Sep 30 2019 at 11:43): Who doesn't understand Risch integration with radical field extensions? Why bother to even include a reference to a paper? #### Tim Daly (Sep 30 2019 at 11:44): Lean is following the same path Axiom took. I'm trying to suggest ideas that keep it from becoming an open source project maintained by one person and used by 4 on odd months. #### Tim Daly (Sep 30 2019 at 11:47): Axiom was developed at IBM Research, contains the results of many PhD theses, costs an extimated 42 million dollars to develop, and involved mathematicians worldwide. #### Sebastien Gouezel (Sep 30 2019 at 11:49): You can have a look at more recent files, where we are precisely trying to enforce more documentation, but at places where it is useful -- i.e., there are nonobvious definitions or design decisions. For instance https://github.com/leanprover-community/mathlib/blob/master/src/geometry/manifold/manifold.lean, that I wrote recently and for which the more than 100 comments in the PRs made me vastly improve the documentation. Does it correspond to what you are looking for, or how would you envision things for better documentation? #### Tim Daly (Sep 30 2019 at 11:50): The key question is, what discipline is required in development so that when Lean has 100,000 lemmas, 5,000 theorems, and dozens of fields of mathematics, it can still be maintained by people who have no idea what a homology is. #### Johan Commelin (Sep 30 2019 at 11:52): No. That is not the key question. #### Johan Commelin (Sep 30 2019 at 11:52): The key question is: why are pure mathematicians not using ITPs on a large scale right now? #### Tim Daly (Sep 30 2019 at 11:52): Sebastien, I'm quite fond of literate programming. We all understand books, how to write them, how to navigate them, how to orgainzie them, and how to index them. It is trivial to extract code from a latex document. #### Tim Daly (Sep 30 2019 at 11:54): Johan, that's where we differ. Axiom's motto is "The 30 Year Horizon". I'm looking at what Axiom needs to be in 30 years, say as a trusted computational oracle for proof systems. You're looking at enlarging the community this month. So we're talking about different objectives. #### Mario Carneiro (Sep 30 2019 at 11:55): Johan didn't say Lean, he said ITPs #### Mario Carneiro (Sep 30 2019 at 11:55): what is it that the ITP community lacks right now that is preventing world domination? #### Tim Daly (Sep 30 2019 at 11:55): If you were given Lean and everyone else left, could you maintain it and extend it? The C++ code is quite clever. #### Johan Commelin (Sep 30 2019 at 11:56): If I were given all maths textbooks in the world, and everyone left... all I could do was sit on top of them... #### Mario Carneiro (Sep 30 2019 at 11:56): Tim, that kind of happened with lean 3 #### Johan Commelin (Sep 30 2019 at 11:57): Tim, I never said "this month". But I do know that (i) we are moving towards 30 years later one month at a time, and (ii) it takes more than documentation of trivialities to get mathematicians interested. #### Johan Commelin (Sep 30 2019 at 11:57): Why do you think I started using Lean, and why am I still using it? Because of superb documentation? #### Tim Daly (Sep 30 2019 at 11:58): Someone working in Cubical Type Theory isn't going to find much support. And since academic promotions never measure code output (withness William Stein) there is no upside to writing Lean theories. #### Tim Daly (Sep 30 2019 at 12:00): Books, however, count. #### Johan Commelin (Sep 30 2019 at 12:00): It depends... #### Johan Commelin (Sep 30 2019 at 12:00): ... on the contents. #### Mario Carneiro (Sep 30 2019 at 12:01): there you've stumbled on one part of our plan for world domination - first fix the financial incentives by making mathematicians care about computers and formal mathematics #### Mario Carneiro (Sep 30 2019 at 12:02): once it becomes sufficiently relevant it won't be career suicide anymore #### Tim Daly (Sep 30 2019 at 12:04): I worked with Gilbert Baumslag, the leader of the field of Infinite Group Theory. He wrote 125 papers on the subject. I open-sourced Magnus, which automates Infinite Group Theory calculations. I THINK there were 3 users. #### Tim Daly (Sep 30 2019 at 12:05): Convincing mathematicans to use computers (the source of all frustration) is like convincing cats to use the internet. You can barely get them to do a google search as it takes time away from their next paper. #### Tim Daly (Sep 30 2019 at 12:09): I feel it is like the transition from the 19th to the 20th century. 19th century mathematicians resisted the idea of proofs. 20th century mathematicians resist the idea of ITP. Progress in science is measured one funeral at a time.-- Max Planck. So design your system for the 30 year horizon so it is possible to maintain it by non-authors and non-experts. #### Tim Daly (Sep 30 2019 at 12:13): If you want ITP mathematicians you have to grow them. So you need courses. You need documentation. You need degrees which recognize programs as well as papers and books. Current mathematicians are successfully set in their ways and they know where credit lies. #### Johan Commelin (Sep 30 2019 at 12:13): Why do you want to use Lean as backend for Axiom? Wouldn't metamath be a lot better for your use case? #### Johan Commelin (Sep 30 2019 at 12:14): It is extremely small, fast, and very flexible in its foundations #### Johan Commelin (Sep 30 2019 at 12:14): The checker is so small that if you write 3000 lines of comments, you will have a paragraph per line of code. #### Tim Daly (Sep 30 2019 at 12:17): I'm looking at several systems (COQ, AGDA, IDRIS, HOL, ISABELLE). HOL88 is interesting because it is implemented in Common Lisp and I can embed it in Axiom directly (which is also Common Lisp). Lean is interesting in particular due to Jeremy Avigad. I used it a bit and now I'm trying to communicate between it and the compiler. Axiom is typed everywhere, at every level, and is dependently typed so I need a robust system. #### Tim Daly (Sep 30 2019 at 12:18): As a mathematician, why aren't you using Axiom? #### Andrew Ashworth (Sep 30 2019 at 12:18): FWIW I figure most people don't use ITPs because being formal is a chore. Nobody cares about Bourbaki, and nobody cares about convincing a computer they are correct. In that sense they are a solution in search of a problem. I think they will take off once we true believers formalize enough math and develop enough useful tactics that the software starts being a net gain in productivity as opposed to a 10x reduction. #### Tim Daly (Sep 30 2019 at 12:21): Andrew, I'm not sure how far tactics can carry you toward that goal. The undecidability issue is an issue. Axiom uses heuristics at runtime to resolve type questions that can't be computed at compile time. I expect to run into the same issue once I try to prove some of Axiom's algorithms correct. Also, tactics have to somehow be related to the specification language of the algorithms and I'm not sure what to think about that connection yet. It is still an "open research question" for me. #### Tim Daly (Sep 30 2019 at 12:23): Most Lean work isn't proving algorithms, of course, so I'm out in left field near the corn silo. #### Tim Daly (Sep 30 2019 at 12:30): Also, note that there is almost no person in common in the bibliographic references in ITP and Computer Algebra. James Davenport seems to be the only crossover I can name. There are 2 "silos" of computational mathematics and the computer algebra people I know can't read the logic literature. #### Tim Daly (Sep 30 2019 at 12:31): The Axiom Sane project (Sane is a synonum for rational, coherent, judicial, and sound) is trying to build a bridge between these two fields, merging computer algebra and theorem proving machinery. #### Andrew Ashworth (Sep 30 2019 at 12:35): I see that Axiom wants to call Lean under the hood. Is it feasible that I could call Axiom from Lean and get a proof certificate for things that a CAS can do? For example, I would love to call out to a cylindrical alg decomp algorithm, or matrix decomposer alg, or symbolic integrator. #### Andrew Ashworth (Sep 30 2019 at 12:36): I guess in these cases it's difficult since not only the result needs to be returned, but also the sequence of transformations that lead up to it #### Tim Daly (Sep 30 2019 at 12:38): Andrew, that's exactly the goal of the Axiom Sane project. Axiom should be a trusted oracle for computing algorithms. Libraries like complex numbers, computing primes, doing CAD, etc. are easy in Axiom but providing a trusted algorithm and a proof certificate is the center of the research question. The oracle response should provide the answer and a proof that the checker can check #### Tim Daly (Sep 30 2019 at 12:40): I can't imagine trying to encode the Risch integration algorithm in Lean. It requires too much algorithmic machinery, most of it at the PhD thesis level. But it already exists in Axiom. #### Tim Daly (Sep 30 2019 at 12:53): The idea of "encoding all of mathematics" doesn't seem to mention the computer algebra field. Certain algorithms (e.g. Buchberger's algorithm) seem to have been proven but the whole subject of Infinite Group Theory, which is mostly non-terminating procedures, doesn't seem to fit into the proof systems easily. #### Mario Carneiro (Sep 30 2019 at 13:12): I think that Andrew's suggestion is the more profitable angle here. Rather than attempt to have lean be a component of axiom, see if you can modify axiom to produce certificates of its results that can then be checked in a theorem prover like lean #### Mario Carneiro (Sep 30 2019 at 13:13): You could also just reimplement selected algorithms in lean #### Mario Carneiro (Sep 30 2019 at 13:16): The problem with treating Axiom as a black box is that you don't trust it, and the very purpose of the project seems to be to make it more trustworthy. The only way you can achieve that is either by whiteboxing the algorithm and proving it correct, or by having the algorithm validate any outputs it gives by producing proofs alongside. #### Tim Daly (Sep 30 2019 at 13:42): Indeed, the point is to prove the Axiom algorithms correct with respect to a specification. #### Kevin Buzzard (Sep 30 2019 at 16:21): If you want ITP mathematicians you have to grow them. So you need courses. You need documentation. You need degrees which recognize programs as well as papers and books. Current mathematicians are successfully set in their ways and they know where credit lies. I am taking a risk in my job by not producing the standard research papers which I used to produce. My justification for this is that I am attempting to put courses together. But I won't be able to change our UG maths degree, other than by adding a pure Lean course to it (which I no doubt will try to do at some point). It will still just be one of many. #### Keeley Hoek (Oct 01 2019 at 03:11): But the lean course will exist, Kevin! :D #### Tim Daly (Oct 01 2019 at 15:45): Survey question: What is the biggest concern developers have about open source: Result: Perhaps the clearest finding from this question is that 46% of respondents indicated risk about how well packages will be maintained into the future is either a major or a moderate obstacle https://thenewstack.io/what-is-the-biggest-concern-developers-have-about-open-source/ #### Luca Seemungal (Oct 01 2019 at 15:45): @Kevin Buzzard Speaking about Lean courses, have you finished docs for the incoming freshers / is it viewable by us? I'm a Warwick second year and am fairly interested in this stuff. I've spent the summer trying to learn it but it's all fairly impenetrable. Some docs for maths undergrads would be obviously very helpful. If they're not finished yet I'll just actually concentrate on my degree (for once ;)) #### Tim Daly (Oct 01 2019 at 16:04): Jeremy Avigad used the Lean browser to organize his class. You might consider adding sections to the browser text and organize it by lecture. #### Kevin Buzzard (Oct 01 2019 at 17:31): @Luca Seemungal Hmm, there are many things which are half-finished, including my preparation for my lectures this week, which have to take priority right now. But we're getting there. #### Bryan Gin-ge Chen (Oct 05 2019 at 03:22): Not about Lean specifically, but this event looks interesting: https://www.helixcenter.org/roundtables/mechanization-of-math/ #### Patrick Massot (Oct 05 2019 at 09:28): @Kevin Buzzard you should leave a comment pointing to your Fermat blog post there. #### Kevin Buzzard (Oct 05 2019 at 18:40): rofl I just tried, and it was rejected as spam ;-) #### Patrick Massot (Oct 05 2019 at 18:57): Internet is so wonderful... #### Tim Daly (Oct 06 2019 at 06:59): There is an interesting talk by John Seale (of the Chinese Room fame), that is related to the question of "machine checked proofs". I suggest you take careful notes of the definitions he uses in the first 5 minutes as the whole talk rests on them. https://www.youtube.com/watch?v=rHKwIYsPXLg #### Patrick Massot (Oct 06 2019 at 09:49): I watched 23 minutes but I hesitate to continue. Is there any moment when he does something else than repeating: "let's laugh together at how stupid are people who disagree with me" and "the computer is not intelligent because it has zero intelligence"? #### Patrick Massot (Oct 06 2019 at 09:51): I don't say I disagree, but I was hoping for arguments instead of authoritarian assertions and jokes. #### Mario Carneiro (Oct 06 2019 at 10:05): He gives an argument, although I don't particularly buy it #### Mario Carneiro (Oct 06 2019 at 10:06): Tim is right though - his argument hinges on a linguistic matter between two senses for what is meant by intelligent #### Mario Carneiro (Oct 06 2019 at 10:07): it's not all about the chinese room #### Bryan Gin-ge Chen (Oct 23 2019 at 15:30): Not sure if this really counts as "in the wild", but I just saw a link on twitter to a nice-looking PDF titled "Logical Verification in Lean" by @Alexander Bentkamp, @Jasmin Blanchette and @Johannes Hölzl. It looks like it's for the course "Logical Verification" by @Jasmin Blanchette and @Alexander Bentkamp. I'm looking forward to reading it! #### Kevin Buzzard (Oct 23 2019 at 15:35): It still amuses me that computer scientists are quite happy to have entire chapters on metaprogramming and monads before the section on "adding two numbers" :D #### Kevin Buzzard (Oct 24 2019 at 08:27): http://chalkdustmagazine.com/features/can-computers-prove-theorems/ #### Luca Seemungal (Oct 24 2019 at 08:39): "it's not hard to get Lean running on a computer" :joy::joy: #### Jason Rute (Oct 24 2019 at 11:20): So where is the scorpion section in mathlib? https://i0.wp.com/chalkdustmagazine.com/wp-content/uploads/2019/10/level.jpg #### Kevin Buzzard (Oct 24 2019 at 11:50): Yeah what the heck is that scorpion thing about?? The UCL people did the graphics, I don't know what they were thinking there. #### Kevin Buzzard (Oct 24 2019 at 11:50): But addition and multiplication world are here: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ #### Johan Commelin (Oct 24 2019 at 11:58): Lol, it's a nice easter egg, right? #### Johan Commelin (Oct 24 2019 at 11:58): I mean, it really fits in the theme #### Johan Commelin (Oct 24 2019 at 11:59): Guess who modeled for the second charachter in this pic: https://i2.wp.com/chalkdustmagazine.com/wp-content/uploads/2019/10/lean-e1571862471361.jpg?resize=670%2C300 #### Kevin Buzzard (Oct 24 2019 at 12:18): It's the launch party of the mag this evening and I'm wearing a pair of trousers which are as close as possible to those depicted #### Kevin Buzzard (Oct 24 2019 at 12:18): They never told me they were going to do all this crazy graphics, I only found out a couple of weeks ago and I wrote the article months ago. And I didn't even notice what Johan is pointing out! #### Kevin Buzzard (Oct 24 2019 at 12:19): I showed it to my daughter and she said "oh wow Dad that's you!" and I'm like "is it??" #### Johan Commelin (Oct 24 2019 at 12:19): Too bad that Zulip doesn't have a "crazy trousers" emoji.... #### Kevin Kappelmann (Oct 24 2019 at 12:24): Too bad that Zulip doesn't have a "crazy trousers" emoji.... ... I was about to do so, but I do not have the permissions :( https://zulipchat.com/help/add-custom-emoji #### Johan Commelin (Oct 24 2019 at 12:35): @Simon Hudon @Mario Carneiro who's the boss here? Can we make an exception :octopus: :tools: :joy_cat: #### Bryan Gin-ge Chen (Oct 24 2019 at 13:35): @Kevin Buzzard @Mohammad Pedramfar The natural number game is looking great! Congrats! #### Kevin Buzzard (Oct 24 2019 at 13:36): Great! So now let's do the complex number game. #### Kevin Buzzard (Oct 24 2019 at 13:36): you import the reals, and then have to define everything. #### Kevin Buzzard (Oct 24 2019 at 13:36): unfortunately all of the proofs are "ext;ring" :-/ #### Kevin Buzzard (Oct 24 2019 at 13:37): maybe I should think of a better game #### Kevin Buzzard (Oct 24 2019 at 13:38): Although others have done it before, and probably they've even done it better (Patrick showed me some impressive stuff I remember), I wonder if we can just get some sort of little suite of games like this, just to get people interested. #### Reid Barton (Oct 24 2019 at 13:46): I've been meaning to make stickers based on the Lean logo, but now I know what I really need is that start screen #### Luca Seemungal (Oct 24 2019 at 13:46): I suppose one could turn a whole undergrad degree into a game... #### Johan Commelin (Oct 24 2019 at 14:01): I think @Edward Ayers created a bunch of alternative Lean logos some time ago #### Johan Commelin (Oct 24 2019 at 14:03): https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Leaked.20Lean.204.20Logos #### Kevin Buzzard (Oct 26 2019 at 18:29): Just saw this on the front page of the internet: https://www.reddit.com/r/math/comments/dnc0jj/imo_grand_challenge_automated_problem_solving/ #### Kevin Buzzard (Oct 27 2019 at 08:45): and now this (on Mario's metamath paper): https://news.ycombinator.com/item?id=21358674 #### Mario Carneiro (Oct 27 2019 at 08:49): I was on the front page for a while :D #### Kevin Buzzard (Oct 27 2019 at 09:23): I regard these things as small victories for the formal proof verification community #### Johan Commelin (Oct 28 2019 at 06:33): @Kevin Buzzard Well... they certainly are small victories within the CS community. But how many pure mathematicians read hacker news? Probably about as many as use ITP's... #### Chris Hughes (Nov 01 2019 at 20:10): IMG_20191101_144932.jpg #### Chris Hughes (Nov 01 2019 at 20:10): Lean related graffiti in room 342 #### Miguel Raz Guzmán Macedo (Nov 02 2019 at 05:13): Nice IMO grand challenge! Is there a prize? #### Bryan Gin-ge Chen (Nov 02 2019 at 05:16): #### Sebastian Ullrich (Nov 05 2019 at 08:48): @Marc Huisinga presented his bachelor's thesis on a partial verification of the compiler in our reference counting paper (done in Lean 3) yesterday. Apart from a much more in-depth description of the IR and compiler than we could have put in the paper, there are some good observation about effective proving in Lean in general in section4, as well as a self-contained section (5) about the list/multiset group function (which he might want to PR to mathlib at some point?). #### Mario Carneiro (Nov 05 2019 at 09:27): The formalization mentions obtain? #### Mario Carneiro (Nov 05 2019 at 09:27): but also #check #### Mario Carneiro (Nov 05 2019 at 09:28): The lean version that was used exists outside the linear flow of time #### Sebastian Ullrich (Nov 05 2019 at 09:34): It's the obtain tactic. I guess we never updated lstlean.tex to remove the obsolete keyword. #### Kevin Buzzard (Nov 05 2019 at 09:52): "we use Lean 3 to prove that Lean 4 works". Cunningly avoiding Goedel. #### Mario Carneiro (Nov 05 2019 at 09:58): wait, I don't think that's the direction that avoids Goedel #### Marc Huisinga (Nov 05 2019 at 10:34): yes, it's the obtain tactic. the proof code certainly still needs to be cleaned up, especially before contributing anything to mathlib. many non-terminal simps, lots of duplication and several instances where i miss-use let and should use have instead :) #### Kevin Buzzard (Nov 05 2019 at 12:15): I'll take that as a vote for "one tactic instead of two please" #### Patrick Massot (Nov 12 2019 at 16:44): Some new "Lean in the wild": Sébastien got a prize for theorems he didn't formalize yet, but half of the interview he gave to the CNRS website is propaganda for proof assistants. #### Johan Commelin (Nov 12 2019 at 17:23): @Sebastien Gouezel Congratulations! :octopus: :cake: #### Sebastien Gouezel (Nov 12 2019 at 17:34): Thank you! #### Wojciech Nawrocki (Jan 03 2020 at 20:43): Slightly more unusual spotting of Lean in the wild: George Hotz has livestreamed writing a small parser for Metamath files on Twitch back in November. #### Mario Carneiro (Jan 03 2020 at 20:51): first 40 minutes: why is the hello world example broken #### Simon Cruanes (Jan 03 2020 at 20:59): This person needs to hear about mm0, as a more modern foundation than metamath :p #### Mario Carneiro (Jan 03 2020 at 23:00): It's actually pretty funny, during the stream he visits the MM0 page like 5 times when searching for things about metamath or lean (and usually coming up empty). Apparently I've got good SEO #### Kevin Buzzard (Jan 26 2020 at 15:28): https://agentultra.github.io/lean-for-hackers/ -- hello world stuff! It had never occurred to me to get Lean to print anything before. #### Tim Daly (Jan 26 2020 at 15:31): Oh SWEET! You've "cracked the code". I can build on that. #### Bryan Gin-ge Chen (Jan 26 2020 at 16:30): @James King made a thread about his guide here. #### Kevin Buzzard (Jan 26 2020 at 16:32): oh nice, thanks Bryan. I see now that I starred that post when it appeared but I never went back and "tidied up recent stars", my bad. #### Patrick Massot (Jan 26 2020 at 16:51): Kevin, did you notice that "The primary focus of Lean is mathematical research and its intended audience are mathematicians." We can be proud of what we did. By taking over this forum, we managed to get James completely confused about Lean's origins an intended audience. :grinning: #### Kevin Buzzard (Jan 26 2020 at 18:37): I did notice that yes :-) #### James King (Jan 26 2020 at 18:49): I am completely confused and PRs are welcome. I've talked to various people around the community but I haven't met all of you nor had a chance to meet Kevin, Jeremy, or Leo. :smiley: #### James King (Jan 26 2020 at 18:54): I made the guide after watching George Hotz try Lean on his "esoteric language sundays" twitch channel and being stymied in a similar fashion by the empty sections on the programming language bits of the Lean documentation. I hope to round it out a bit and work with Simon to contribute parts to the official docs. #### James King (Jan 26 2020 at 18:58): Presently wrapping up work on a JSON parsing library for Lean3 to serve as the intro for the next section to the guide. (I'm really humbled that people have actually read it...) #### Kevin Buzzard (Feb 12 2020 at 11:34): http://aarinc.org/Newsletters/130-2020-02.html#zulip #### Kevin Buzzard (Feb 12 2020 at 11:34): "The lean zulip server demonstrates that good communication tools can help communities thrive, make it easier for newcomers to ask questions, and lower friction for discussions. " #### Jasmin Blanchette (Feb 13 2020 at 20:40): Kevin, since when do you read the AAR newsletter? Next thing you know, you'll be attending IJCAR or CADE. #### Simon Cruanes (Feb 13 2020 at 20:45): Next IJCAR is in Paris, it's the right time to attend! :croissant: :baguette: #### Kevin Buzzard (Feb 13 2020 at 21:02): I gave a talk in Bath on Tuesday and some computer scientists attended, and one of them emailed me the newsletter afterwards :-) #### Jasmin Blanchette (Feb 13 2020 at 21:04): I used to be the editor of that beautiful publication. :) If you want to get it delivered to your mailbox (4-5 times a year), you can ask Sophie Tourret at newsletter@aarinc.org . She's an Isabelle user, though, so you might want to keep a low profile. #### Johan Commelin (Feb 22 2020 at 21:15): @Kevin Buzzard hits frontpage on HN again: https://news.ycombinator.com/item?id=22390486 #### Patrick Massot (Feb 22 2020 at 21:16): Who did he provoked this time? #### Johan Commelin (Feb 22 2020 at 21:18): Just his blogpost from over a week ago (-; #### Kevin Buzzard (Mar 26 2020 at 21:15): https://www.imperial.ac.uk/news/196435/growing-plants-without-soil-amongst-frontier/ Go me, I got money for a Lean post-doc :D #### Kevin Buzzard (Mar 26 2020 at 21:15): Job ad should be out by the end of the week :D #### Andrew Ashworth (Apr 01 2020 at 15:54): Not sure if this was posted anywhere else, but I saw a presentation go up about Lean at Imperial College London: https://www.researchgate.net/publication/339827943_University_students'_proof_writing_and_LEAN_theorem_prover_the_case_of_the_abundant_number_task #### Kevin Buzzard (Apr 01 2020 at 16:28): Athina Thoma is the education post-doc who watched my students learning Lean, interviewed and surveyed them, and tried to draw rigorous conclusions from an educational perspective. #### Jasmin Blanchette (Apr 03 2020 at 12:53): I'm not sure if this is "in the wild", but here's the new version of our Lecture notes: https://lean-forward.github.io/logical-verification/2020/index.html#material Sorry for all the spam. I just want to make sure nobody keeps on reading the old book. #### Bryan Gin-ge Chen (Apr 03 2020 at 12:58): I think prominent links to the new version at the old course site and github repo would help with that. #### Johan Commelin (Apr 06 2020 at 05:24): Blogpost about Lean https://ahelwer.ca/post/2020-04-05-lean-assignment/ (mentions NNG). It's urrently place 14 on HackerNews: https://news.ycombinator.com/item?id=22789953 #### Bryan Gin-ge Chen (Apr 06 2020 at 05:24): #### Kevin Buzzard (Apr 06 2020 at 17:55): Hitchhikers Guide Lean book now on front page of hacker news #### Anne Baanen (Apr 07 2020 at 07:49): Here is the comment section: https://news.ycombinator.com/item?id=22794533 #### Johan Commelin (Apr 07 2020 at 07:49): They are saying silly things over there #### Johan Commelin (Apr 07 2020 at 07:50): Like you can't do epsilon delta proofs in Lean #### Johan Commelin (Apr 07 2020 at 07:50): Clearly didn't read TFA before commenting #### Patrick Massot (Apr 07 2020 at 07:50): I'm not sure arguing a lot about this is a good use of our time. Writing better documentation and tutorials seem like a better idea to me. #### Rob Lewis (Apr 07 2020 at 07:52): Johan Commelin said: They are saying silly things over there Doesn't this apply to literally every comments section on the internet? This will keep happening no matter how perfect the documentation and tutorials are :) #### Anne Baanen (Apr 07 2020 at 16:21): Natural number game on Reddit: https://www.reddit.com/r/math/comments/fwlgf4/natural_number_game_a_game_where_you_learn_to/ #### Kevin Buzzard (Apr 07 2020 at 17:48): Thanks @Patrick Massot -- Patrick encouraged me to give NNG "some love" last week, and I accepted all the PRs, made some edits, and pushed a slightly tidied up version live. Just in time! #### Kevin Buzzard (Apr 08 2020 at 15:59): My default search engine is duck duck go, and I usually get to the mathlib github repo by searching for the word mathlib, because it's usually the second or third hit. But as of the last 24 hours or so it's consistently been number 1. Is that true for everyone or just me? I thought the point was that they weren't tracking me. #### Marc Huisinga (Apr 08 2020 at 16:00): third entry for me #### Alex J. Best (Apr 08 2020 at 16:00): third for me after pearson and matlab #### Ryan Lahfa (Apr 08 2020 at 16:01): Kevin Buzzard said: My default search engine is duck duck go, and I usually get to the mathlib github repo by searching for the word mathlib, because it's usually the second or third hit. But as of the last 24 hours or so it's consistently been number 1. Is that true for everyone or just me? I thought the point was that they weren't tracking me. 2nd entry for me #### Alex J. Best (Apr 08 2020 at 16:02): Its non-deterministic though, simply refreshing changes the order for me. #### Marc Huisinga (Apr 16 2020 at 23:29): "The Mechanization of Mathematics" by Jeremy Avigad #### Sebastian Ullrich (May 11 2020 at 08:27): @Markus Himmel presented his bachelor thesis on diagram chasing in Lean 3 last week. It's a very nice read, even for someone who knows as little about category theory as I do. #### Patrick Massot (May 11 2020 at 08:28): This should be PRed to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/lean.bib right away #### Johan Commelin (May 11 2020 at 08:33): @Markus Himmel Congratulations! I'm looking forward to seeing the snake lemma in mathlib! #### Johan Commelin (May 11 2020 at 08:36): Is this really the first formal proof of the snake lemma? Doesn't some hott lib have it? Or the spectral sequence library by @Floris van Doorn et al? #### Markus Himmel (May 11 2020 at 08:38): I looked for it, but didn't find anything. Perhaps I'm just very bad at searching. I'm pretty confident that it's the first formal proof that is valid in any abelian category. #### Johan Commelin (May 11 2020 at 08:54): lemma four [epi α] [mono β] [mono δ] : mono γ := mono_of_zero_of_map_zero _$ λc hc,
begin
chase c using [g,β,f′,α] with b b′a′a,
have : f a = b, by commutativity,
commutativity
end


That is so cool!

#### Johan Commelin (May 11 2020 at 08:57):

@Markus Himmel Can you comment on how fast this is?

#### Johan Commelin (May 11 2020 at 08:58):

Would we need to cache the result (our maybe use a proof script that commutativity and/or chase output? Or can we just leave these proofs as is, because they will be almost instant?

#### Patrick Massot (May 11 2020 at 09:00):

How much of all this is in mathlib?

#### Johan Commelin (May 11 2020 at 09:00):

Markus has made a couple of PRs in the past, but we don't have abelian categories yet, and neither do we have any of the automation.

#### Markus Himmel (May 11 2020 at 09:01):

Johan Commelin said:

Markus Himmel Can you comment on how fast this is?

Right now, it is quite slow (think tidy levels of slow). However, I believe that there are a lot of performance improvements accessible to someone who knows more about tactic writing than I do.

#### Markus Himmel (May 11 2020 at 09:05):

Johan Commelin said:

Markus has made a couple of PRs in the past, but we don't have abelian categories yet, and neither do we have any of the automation.

Yep. I'm waiting for the enriched branch to be merged so that preadditive categories are available. Once that is ready, I'm planning to start PRing abelian categories

#### Patrick Massot (May 11 2020 at 09:14):

This is really important Markus. Otherwise your work will be lost.

#### Kevin Buzzard (May 11 2020 at 09:39):

Yes, very well done on the thesis but now it's really important that it gets into mathlib before it dies

#### Markus Himmel (May 11 2020 at 09:43):

Do we know what the status of the enriched branch is? If it will take time, would mathlib be happy with a boring pedestrian definition of preadditive categories that can hopefully be replaced seamlessly once enriched categories are ready, so that I can get started PRing? @Scott Morrison, what are your thoughts on this?

#### Reid Barton (May 11 2020 at 11:57):

I think that would probably be a good idea, especially as the enriched branch only works for enrichments where the forgetful functor (like Ab -> Set) is faithful anyways

#### Scott Morrison (May 11 2020 at 16:07):

@Markus Himmel, sorry, I haven't had much time to work on this recently. Moreover, it's been a pretty discouraging experience so far. I'll try to look at it again soon.

#### Scott Morrison (May 11 2020 at 16:07):

Last I looked at it I was pretty frustrated by another instance of https://github.com/leanprover-community/lean/issues/197.

#### Scott Morrison (May 11 2020 at 16:08):

(although this wasn't actually completely blocking progress)

#### Scott Morrison (May 11 2020 at 16:09):

I think I should (or someone else should) just write the "pedestrian" definition of just preadditive categories, so we can call get on with life. :-) Hopefully for a while at least this won't preclude slotting in a more general framework later.

#### Markus Himmel (May 11 2020 at 16:15):

Scott Morrison said:

I think I should (or someone else should) just write the "pedestrian" definition of just preadditive categories, so we can call get on with life. :-) Hopefully for a while at least this won't preclude slotting in a more general framework later.

How about I clean up and PR the definition of preadditive category I have been using in my project?

#### Floris van Doorn (May 11 2020 at 16:30):

We didn't prove the snake lemma in the Lean HoTT library. We actually needed very little homological algebra for our project, much less than we initially suspected. I think we proved some other lemmas, like the four and/or five lemma, but never actually used it.
This is a very nice project, and the tactics look really useful!

#### Noob (May 13 2020 at 00:48):

Can anyone comment on how Lean is doing with regard to the questions asked here https://cs.nyu.edu/pipermail/fom/2020-May/022152.html ?

#### Alex J. Best (May 13 2020 at 00:57):

Edit: I think I misunderstood the question, apologies. Here is what i originally wrote which doesn't answer your questions. If you click on the link you'll see lean is already on that list. Maybe there are a some more things that have more recently appeared in mathlib that we haven't updated Freek about (mean value theorem @Yury G. Kudryashov ?) but more-or-less the answer is we have a fair number of these goals formalized (including at least one which is present in no other system) but less than the more mature systems.

#### Jalex Stark (May 13 2020 at 00:59):

such lists don't do a great job at capturing progress

#### Jalex Stark (May 13 2020 at 01:00):

if you want to get a feel for which things are easy to formalize, hang out here :)

#### Alex J. Best (May 13 2020 at 01:11):

To answer the questions in the post:
1) which of these can make use of work done in which other ones?
There are two ways in which systems can make use of work in others, either via an automated conversion/ or embedding of the logic of one into the other, for this you might be interested in @Mario Carneiro 's work embedding some metamath0 proofs inside of lean, the other way is that those with similar logic can also draw inspiration / replicate ideas from one in another system more easily. For lean this would likely be coq, where a lot of work (tactics especially) in lean have learned from prior work done in coq, rather than reinvent the wheel.

2) which of these would be the easiest for mathematicians with some programming experience to learn to use to create machine-verifiable proofs?
Lean of course ;). More seriously that's a very difficult question to answer as the answer depends on personal preference, how much experience the user has with different types of programming languages.

3) which of these have a good translator that turns a machine-readable proof into something a human reader might gain insight from?
None of them? ISABELLE/NAPROCHE and forthel are projects that go in that direction, but is more aimed at writing a human readable proof that a machine can read, rather than translation. Peter Koepke and Tom Hales have thought about how this might work in lean but I'm not aware of any publications (yet).

#### Jalex Stark (May 13 2020 at 01:28):

Is lean code not human readable?

#### Alex J. Best (May 13 2020 at 01:38):

I took this to mean untrained human, but for lean at least it completely depends on the style, level of comments and whether you have an interactive viewer open, if you show me a random term mode proof in mathlib without lean open what I'm going to get from it is what lemmas are used probably, wether induction is used or not, and at the end of the day I'll be reconstructing the proof "flow" in my head, I don't know what level of insight that is, compared to say a normal proof in a book or paper. I feel like this question is really getting at a system where I can show the output to a random mathematician and they will not think it looks odd (a la Ganesalingam-Gowers).

#### Mario Carneiro (May 13 2020 at 01:38):

I've gained plenty of human insight by reading formal proofs from other proof assistants

#### Mario Carneiro (May 13 2020 at 01:39):

for example when I want to port a proof and I look at some isabelle / mizar / coq file that does it

#### Mario Carneiro (May 13 2020 at 01:39):

but it's not for the untrained human probably

#### Jalex Stark (May 13 2020 at 01:44):

oh i don't know why i haven't looked at the Ganesalingam-Gowers paper

#### Alex J. Best (May 13 2020 at 01:56):

Oh it's great fun, you should check out Gowers' original blog posts on the topic too, IIRC he did turing-test style polls to see if people could guess which proofs were auto-generated (and won?)

#### Alex J. Best (May 13 2020 at 01:58):

Starts here, few posts in sequence https://gowers.wordpress.com/2013/03/25/an-experiment-concerning-mathematical-writing/

#### Scott Morrison (May 13 2020 at 02:39):

tidy originated in a (completely unsuccessful) attempt to imitate what they did. Ed Ayers (who is Gowers' student) has been pursuing this properly.

#### Johan Commelin (May 13 2020 at 03:30):

For the record: the "completely unsuccessful" is a very modest description with a lot of irony. tidy is probably one of the best hidden tactics in mathlib. You don't see it, but it get's called a lot. And that's just the way it was meant to be.

#### Mario Carneiro (May 13 2020 at 03:32):

I think it's fair to say that while it is a useful and powerful tactic, it does not really act like the Ganesalingam-Gowers prover. It's still not clear to me whether this is a failing of tidy or the GG prover

#### Andrew Ashworth (May 15 2020 at 19:15):

Lean was mentioned in a tweet today: https://twitter.com/alexkontorovich/status/1261350124883771392
A journal is having a special issue on formalized mathematics and calling for papers.

#### Mario Carneiro (May 15 2020 at 19:17):

lol, I don't trust the linked journal page because the web design is too good

#### Andrew Ashworth (May 15 2020 at 19:18):

I have the opposite reaction. I have paid out the nose for various textbooks from Taylor and Francis, and now I see where some of my money is going...

#### Bryan Gin-ge Chen (May 15 2020 at 19:19):

I think Experimental Mathematics is a good journal. Well, at least I've read multiple papers published there that I liked a lot.

#### Bryan Gin-ge Chen (Jul 06 2020 at 19:47):

More like 6 days, I think...

#### Lucas Viana (Jul 07 2020 at 04:17):

This is a bit off-topic, but this title got me thinking about lean in the wild more literally. To what extent do you think theorem provers will be present in everyday life?

For example, I have type 1 diabetes, and as pumps and sensors get more automated we currently can't do much more than trust that their software won't go wrong and potentially do terrible things to us. Of course there is a lot of testing that is done to prevent that, but being able to prove things about these devices seems nice to me.

Another thing would be voting systems, of course. And more or the sci-fi side, I wonder what would it be like to have formalized laws and jurisdictions, and lawyers who prove theorems and debate about hypothesis (but of course this kind of thing would certainly come with its own problems)...

#### Andrew Ashworth (Jul 07 2020 at 04:29):

They are already present, in the semiconductor industry

#### Andrew Ashworth (Jul 07 2020 at 04:30):

after the Pentium floating point bug, IIRC Intel started doing formal verification of their hardware designs

#### Andrew Ashworth (Jul 07 2020 at 04:31):

So I guess the answer is: whenever the cost of business becomes so high that verification is necessary...

#### Andrew Ashworth (Jul 07 2020 at 04:31):

One other obstacle is that program extraction code quality isn't quite there yet for Coq/Lean

#### Andrew Ashworth (Jul 07 2020 at 04:33):

Verified, safe code is usually embedded code. However your favorite functional programming language doesn't work so well without a garbage collector

#### Johan Commelin (Jul 07 2020 at 04:35):

Just wait till the end of summer :four_leaf_clover:

#### Andrew Ashworth (Jul 07 2020 at 04:35):

I don't hold out hope for formal laws. The whole point of the judicial system is to allow some degree of human interpretation and oversight

#### Kenny Lau (Jul 07 2020 at 04:53):

https://www.netjeff.com/humor/item.cgi?file=PentiumJokes

#### Chris Wong (Aug 04 2020 at 05:33):

One area where formalization of laws could be useful is in hours of service regulations (i.e. how long truck drivers can work). The rules can get quite elaborate, especially in the US, and in fact formalization is already underway with the move to electronic logbooks.

#### Bryan Gin-ge Chen (Aug 04 2020 at 05:49):

Discussion of formalization of laws reminds me of this interesting post: A mathematical formulation of the tax code?

#### Yury G. Kudryashov (Aug 04 2020 at 08:34):

There were some debates on how one should interpret the "2 terms" rule in Russian Constitution. Putin interpreted the phrase as "no 3 terms in a row" while others did argue that it should be interpreted as "one may be a President either for 1 term in a lifetime, or for 2 terms in a row". (Later he just changed the Constitution).

And there was another debate a few years before Putin. The law says that a president suggest a candidate for the position of the prime minister, and the parliament votes to accept or deny the candidate. If the parliament denies 3 candidates, then elections must be held immediately. The question was: may the president suggest the same person 3 times in a row or he has to suggest 3 different candidates?

#### Kenny Lau (Aug 04 2020 at 08:35):

Later he just changed the Constitution

#### Yury G. Kudryashov (Aug 04 2020 at 08:45):

Disclaimer: these two paragraph were meant to be examples of difficulties with interpreting laws written in natural language. Though I have my opinion about the political situation in Russia, I would prefer to avoid discussing it here because I assume that people should be welcome to contribute to mathlib regardless of their political views (and thus it's better not to discuss these views unless such a discussion is required to resolve something withing the community).

#### Kevin Buzzard (Aug 26 2020 at 00:02):

https://mathoverflow.net/questions/369863/online-evolving-collaborative-foundational-text-projects/370105#370105 seemed to be a reasonable place to plug mathlib

#### Johan Commelin (Aug 26 2020 at 04:37):

I guess the fact that there are no comments under your answer means that everyone agrees that all the adjectives are satisfied (-;

#### Johan Commelin (Aug 31 2020 at 18:17):

This blog is read by a lot of algebraic geometers and number theorists.

#### Rob Lewis (Aug 31 2020 at 18:31):

Hmm, the spacing on the doc entry he links to looks kind of funky. Not that it's worse than it was before the recent changes. It's a long line that's hard to get right. image.png

#### Johan Commelin (Aug 31 2020 at 18:32):

Ouch... it does look a lot less readable than the actual source code :sad:

#### Gabriel Ebner (Aug 31 2020 at 18:33):

Yeah, binders are hard to get right because we don't get enough information about them from Lean.

#### Gabriel Ebner (Aug 31 2020 at 18:33):

Is this really ∃ x y z, true?

#### Johan Commelin (Aug 31 2020 at 18:33):

structure Scheme extends X : LocallyRingedSpace :=
(local_affine : ∀ x : carrier, ∃ (U : opens carrier) (m : x ∈ U) (R : CommRing)
(i : X.to_SheafedSpace.to_PresheafedSpace.restrict _ (opens.inclusion_open_embedding U) ≅
Spec.PresheafedSpace R), true)


#### Rob Lewis (Aug 31 2020 at 18:33):

Gabriel Ebner said:

Is this really ∃ x y z, true?

Heh, I was wondering about that too.

#### Johan Commelin (Aug 31 2020 at 18:34):

I guess we could have done nonempty (_ \iso _)

#### Gabriel Ebner (Aug 31 2020 at 18:34):

I find the source code equally hard to read.

#### Johan Commelin (Aug 31 2020 at 18:34):

The bit with the carrier and opens is better.

#### Johan Commelin (Aug 31 2020 at 18:34):

But I agree that i has a very ugly type.

#### Gabriel Ebner (Aug 31 2020 at 18:35):

The i is fine IMHO.

#### Johan Commelin (Aug 31 2020 at 18:35):

In maths it is written as $U \cong Spec R$

#### Johan Commelin (Aug 31 2020 at 18:36):

Of course there should be a little \u before that $U$ :grinning_face_with_smiling_eyes:

#### Johan Commelin (Aug 31 2020 at 18:36):

But X.to_SheafedSpace.to_PresheafedSpace.restrict _ (opens.inclusion_open_embedding U) seems quite a mouthful as replacement for that LHS.

#### Johan Commelin (Aug 31 2020 at 18:37):

That's a de-Bruijn factor of about 80

#### Ian Riley (Aug 31 2020 at 18:40):

Hey everyone! I'm not sure if this is the right place for this questions, but I'm a graduate student in computer science who does research in verifying program correctness, the correctness of adaptations to program code, requirement satisfaction, etc. I'd like to see what applications Lean has in that space. Is there a specific thread or individual that I should reach out to?

#### Johan Commelin (Aug 31 2020 at 18:41):

@Ian Riley I guess you are looking for this stream: https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification

#### Ian Riley (Aug 31 2020 at 18:43):

Thanks @Johan Commelin

#### Patrick Massot (Aug 31 2020 at 20:32):

Johan Commelin said:

This blog is read by a lot of algebraic geometers and number theorists.

I knew we needed to update the overview page today.

#### Junyan Xu (Aug 31 2020 at 21:31):

Has the existence of fiber product of schemes ever been proved? How's the general progress towards stacks project?

#### Kevin Buzzard (Aug 31 2020 at 21:52):

Students at Imperial, working with preliminary versions of the definition, have proved that Gamma (Spec(R))=R and that Gamma and Spec are adjoint functors between rings and locally ringed spaces. All of this is yet to hit mathlib. We've never done products but we have tensor products so there's a clear path to it.

#### Kevin Buzzard (Aug 31 2020 at 21:53):

Just to be clear -- we got schemes in mathlib today and it will take a while for other things to filter through.

#### Scott Morrison (Aug 31 2020 at 22:21):

We should make a roadmap for other things about schemes. I'm working on several things still, but would prefer if other people who actually knew algebraic geometry did it. :-) Proving that sheafification is an adjunction is the most immediate need, I think, so that opens up lots of the basic categorical properties of Scheme.

#### Scott Morrison (Aug 31 2020 at 22:22):

In terms of a roadmap for a roadmap, we should do some thorough crosslinking of mathlib and the Stacks project. Ideally we could even produce visualisations of the Stacks tag network, coloured according to what's in mathlib.

#### Damiano Testa (Sep 01 2020 at 05:32):

I am not sure whether this counts as a roadmap, but two results that I use quite frequently are

1. the Miracle Flatness Lemma (https://stacks.math.columbia.edu/tag/00R4)
2. Zariski's Main Theorem (https://stacks.math.columbia.edu/tag/02LQ)

Anything that would approach either of these results would be incredibly useful for algebraic geometers in the wild!

#### Johan Commelin (Sep 01 2020 at 05:49):

@Damiano Testa Please feel free to post those as 2-line issues on the mathlib repo (like I did with #4013)
I think those are great theorems to target.

#### Damiano Testa (Sep 01 2020 at 06:06):

Johan Commelin said:

Damiano Testa Please feel free to post those as 2-line issues on the mathlib repo (like I did with #4013)
I think those are great theorems to target.

I just did: is this (https://github.com/leanprover-community/mathlib/issues/4014#issue-689843280) what you had in mind?

#### Johan Commelin (Sep 01 2020 at 06:07):

@Damiano Testa Yup, that way it is easier to keep track of them. These Zulip threads are a bit too ephemeral

#### Kevin Buzzard (Sep 17 2020 at 13:24):

student at the university of Exeter talking about Lean to his maths society

#### Kevin Buzzard (Sep 17 2020 at 13:46):

Ineresting quote from an UG mathematician: "blackboard bold font was the main selling point for me" (the importance of VS Code \N)

#### Adam Topaz (Sep 17 2020 at 13:47):

$\mathbf{N} > \mathbb{N}$ IMO

#### Kevin Buzzard (Sep 17 2020 at 13:48):

Henrik Lenstra always preferred bold. He told me that bold was the notation in the books originally when notation began to be standardised, and then blackboard bold was invented for blackboards, so the correct notation when working in a non-blackboard format (e.g. print) is bold.

#### Kevin Buzzard (Sep 17 2020 at 13:49):

I liked this idea for years but now I've just bowed to the pressure. I've started using blackboard on my problem sheets.

#### Kevin Buzzard (Sep 17 2020 at 13:49):

I want them to look more like Lean

#### Adam Topaz (Sep 17 2020 at 13:49):

I always just figured it was called blackboardbold for a reason :)

#### Reid Barton (Sep 17 2020 at 13:51):

So if blackboard bold $\mathbb{N}$ is the way to write $\mathbf{N}$ on a blackboard, then how do you write $\mathbb{N}$ on a blackboard?

#### Adam Topaz (Sep 17 2020 at 13:51):

Although I'm writing a paper now where I want to talk about decomposition groups as $\mathbf{Z}_{w|v}$ and also the integers as $\mathbf{Z}$, so yeah....

#### Reid Barton (Sep 17 2020 at 13:51):

I mean, you wouldn't want to get $\mathbb{N}$ and $\mathbf{N}$ confused, would you?

#### Adam Topaz (Sep 17 2020 at 13:51):

$\mathbb{N}$ is how you write $\mathbf{N}$ on a blackboard.

#### Adam Topaz (Sep 17 2020 at 13:53):

$\mathrlap{\mathbb{N}}{\hspace2pt\mathbb{N}}$.

#### Adam Topaz (Sep 17 2020 at 13:53):

I need to sharpen up my latex skills. There we go.

#### Johan Commelin (Sep 17 2020 at 14:05):

Kevin Buzzard said:

Henrik Lenstra always preferred bold. He told me that bold was the notation in the books originally when notation began to be standardised, and then blackboard bold was invented for blackboards, so the correct notation when working in a non-blackboard format (e.g. print) is bold.

I have a very strong opinion on this subject. It is one of the few places where I dare to disagree with Lenstra (and Serre!).

Typography is the art of making things invisible. If you notice the design of some piece of text, it is distracting you from the content. If something stands out, it better be important. For that reason we emphasize the word that is being defined in a certain definition. For that reason, it is okay to print the word Theorem 2.1 in bold when you state it (but not when you refer to it, probably).
In my thesis I went so far as to not have any bold text anywhere. But I think that judicious use of bold text is fine. If a user is searching for a theorem statement, then it can help if the eye is attracted to Theorem 2.1.

However, the eye need not be attracted to the symbol $\mathbf{N}$. Of course it is a very important notion in mathematics. But probably not for the topic/page that I'm writing right now. I therefore think that the blackboard bold letters ($\mathbb{N}, \mathbb{Q}$, etc) strike an excellent balance: they are elegant and unintrusive.

#### Johan Commelin (Sep 17 2020 at 14:09):

Typography is usually also a very conservative art (Garamond or Baskerville, anyone?). But in this regard I'm a very progressive typographer.

#### Kevin Buzzard (Sep 17 2020 at 14:13):

I agree with you Johan -- I think these historical viewpoint is outdated.

#### Adam Topaz (Sep 17 2020 at 14:14):

Kevin Buzzard said:

I agree with you Johan -- I think these historical viewpoint is outdated.

I also agree with this, but I do think that $\mathbf{Z}$ and $\mathbf{Q}$ look better than $\mathbb{Z}$ resp. $\mathbb{Q}$.

#### Adam Topaz (Sep 17 2020 at 14:14):

Maybe I'm in a very small minority here...

#### James Arthur (Sep 17 2020 at 14:44):

As the UG from Exeter. Yes, I love blackboard bold font. It's so pretty and amazing.

#### Alexandre Rademaker (Sep 21 2020 at 20:09):

Regarding law formalization, new attempt on Singapore http://www.slaw.ca/2020/08/25/digitizing-law/

#### Kevin Lacker (Sep 21 2020 at 21:23):

the IMO grand challenge seems pretty neat. are you looking for outside contributors for any part of it?

#### Alex J. Best (Sep 21 2020 at 21:26):

There is a specific stream #IMO-grand-challenge on this Zulip

#### Kevin Lacker (Sep 21 2020 at 21:28):

sorry, i thought I was responding to a message about the imo grand challenge posted in this channel, but it doesnt appear to make any UI difference

#### Alex J. Best (Sep 21 2020 at 21:38):

No problem, I wasn't intending to redirect you, just let you know about it if you weren't aware, as I dont know the answer to what you asked!

#### Kevin Buzzard (Sep 21 2020 at 21:52):

@Kevin Lacker we're always looking for volunteers to translate Olympiad statements and proofs into Lean

#### Jasmin Blanchette (Sep 24 2020 at 13:04):

Lean is on the cover of the CACM: https://mags.acm.org/communications/october_2020/MobilePagedReplica.action?pm=2&folio=Cover#pg1

Unfortunately it's the wrong Lean. :half_frown:

#### Rob Lewis (Sep 28 2020 at 16:35):

Lean and mathlib make an appearance toward the end of a long blog post from Wolfram. Skip to "Math beyond Euclid" if you just care about the Lean part!

#### Rob Lewis (Sep 28 2020 at 16:36):

@Joseph Myers may be interested as there's a focus on Euclidean geometry.

#### Rob Lewis (Sep 28 2020 at 16:42):

" What if one’s axiomatic structure seems great, but implies a few silly results, 1/0 = 0?"

#### Mario Carneiro (Sep 28 2020 at 17:29):

I feel like this theorem is making a joke of our naming convention

#### Kevin Buzzard (Sep 28 2020 at 17:31):

yeah but check out the shading

#### Kevin Buzzard (Sep 28 2020 at 17:31):

I think the joke goes the other way with add_pow

#### Joseph Myers (Sep 28 2020 at 19:34):

There were the discussions of whether we should use sq everywhere in place of square, which would make that name twelve characters shorter.

#### Mario Carneiro (Sep 28 2020 at 19:34):

I don't think we use square elsewhere

#### Mario Carneiro (Sep 28 2020 at 19:36):

there are a decent number of hits for sq, as well as pow_two and mul_self, which are more specific about the representation

#### Patrick Massot (Sep 28 2020 at 19:37):

This discussion of Pythagoras in Euclid vs MetaMath and Lean is so ridiculous. He should read Kevin's blog.

#### Mario Carneiro (Sep 28 2020 at 19:38):

but actually in this case I would simplify it quite a bit more than that, perhaps euclidean_geometry.pythag_dist_iff_angle

#### Joseph Myers (Sep 28 2020 at 19:38):

I probably got square from inner_self_eq_norm_square (but there are other uses, e.g. cos_square).

#### Mario Carneiro (Sep 28 2020 at 19:39):

I see a lot of hits for norm_sq but that's actually a separate function from norm * norm

#### Mario Carneiro (Sep 28 2020 at 19:41):

what is the reason that this theorem is presented using x * x instead of x ^ 2? I honestly feel bad for wolfram looking for the pythagorean theorem and finding such an unfamiliar looking statement with a crazy name

#### Rob Lewis (Sep 28 2020 at 19:42):

Should we change the name and break the link in the blog post already? :smile:

Yeah!

#### Mario Carneiro (Sep 28 2020 at 19:44):

oh wow, inner_product_geometry.norm_sub_square_eq_norm_square_add_norm_square_sub_two_mul_norm_mul_norm_mul_cos_angle is 110 characters

#### Patrick Massot (Sep 28 2020 at 19:45):

More seriously, I would be really nice to make sure the docs website uses notations. The actual source code looks much better.

#### Joseph Myers (Sep 28 2020 at 19:45):

Multiplication seems a bit more convenient to work with. If we wish to say ^ 2 is the preferred form in mathlib, it probably ought to be used in other places as well, such as inner_self_eq_norm_square. (Some inner product lemmas exist in both forms.)

#### Mario Carneiro (Sep 28 2020 at 19:46):

well I would say to prefer x ^ 2 because it is shorter and nicer looking, and add the x * x version if and when it leads to proof savings due to heavy use in that form

#### Mario Carneiro (Sep 28 2020 at 19:46):

For certain theorems in algebra.ring it makes sense to have the x * x version but we don't need every variation on every theorem

#### Mario Carneiro (Sep 28 2020 at 19:48):

Rob Lewis said:

Should we change the name and break the link in the blog post already? :smile:

I think you can edit blog posts

#### Mario Carneiro (Sep 28 2020 at 19:49):

I wonder how we can capture local notations in docgen; that sounds hard

#### Joseph Myers (Sep 28 2020 at 19:51):

The angle notation is local because that was requested in review when I first defined angles, but I'm not sure either angles or pi need to be local notations.

#### Rob Lewis (Sep 28 2020 at 19:52):

Mario Carneiro said:

I wonder how we can capture local notations in docgen; that sounds hard

I doubt it's doable without changes in C++. We have functions to get the environment at the point of a certain decl, but I don't think we can locally change the environment to run a tactic.

#### Reid Barton (Sep 28 2020 at 19:52):

Maybe pi should be local notation at least: https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/pi_n.lean#L69

#### Heather Macbeth (Sep 28 2020 at 19:53):

I think pi = 3.14... should not be global; the symbol is often used for projections in (eg) differential geometry

#### Rob Lewis (Sep 28 2020 at 19:53):

Oh, wait, maybe we can. Don't the simp linters do something like this?

#### Heather Macbeth (Sep 28 2020 at 19:53):

Reid Barton said:

Maybe pi should be local notation at least: https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/pi_n.lean#L69

snap

#### Mario Carneiro (Sep 28 2020 at 19:54):

I'm not saying we shouldn't use local notations, in fact almost every notation used in mathlib is either local or localized (which is the same as a local notation to lean). But that means that we have to do something radical to get these notations in docgen

#### Mario Carneiro (Sep 28 2020 at 19:56):

What ever happened to lean --doc?

#### Floris van Doorn (Sep 28 2020 at 19:56):

Rob Lewis said:

I doubt it's doable without changes in C++. We have functions to get the environment at the point of a certain decl, but I don't think we can locally change the environment to run a tactic.

You can write a function to open all locales, so that at least you print all localized notation. That should already be a big improvement. And we can even encourage authors to use localized notation even if it's for a single file to display them nicely in the docs.

#### Mario Carneiro (Sep 28 2020 at 19:57):

Aha, will lean do that? I haven't tried opening conflicting local notations before

#### Floris van Doorn (Sep 28 2020 at 19:57):

I think it will be a nightmare to parse anything in that case, but probably printing will go fine.

#### Rob Lewis (Sep 28 2020 at 19:58):

That's probably the easiest option here.

#### Rob Lewis (Sep 28 2020 at 19:58):

Does anyone know what https://leanprover-community.github.io/mathlib_docs/core/init/meta/module_info.html was added for?

#### Rob Lewis (Sep 28 2020 at 19:58):

I thought it was the simp linters but I don't see it used.

#### Patrick Massot (Sep 28 2020 at 19:59):

https://github.com/leanprover-community/lean/blame/master/library/init/meta/module_info.lean

#### Patrick Massot (Sep 28 2020 at 19:59):

Presumably Gabriel knows.

#### Mario Carneiro (Sep 28 2020 at 19:59):

https://github.com/leanprover-community/lean/pull/88

Aha

#### Joseph Myers (Sep 28 2020 at 20:04):

If someone would like to figure out what shorter names for everything should be, feel free to rename things (you'll probably want to do some renaming in inner product code alongside that for geometry). Likewise for shorter statements using ^ 2 (which might indicate a few lemmas elsewhere that could do with ^ 2 variants, but I expect the geometry lemmas themselves should only be stated with one of ^ 2 or *, not in both variants).

#### Joseph Myers (Sep 28 2020 at 20:08):

It would definitely be helpful for the style and naming conventions documentation to discuss these issues, however. (Conventions for choosing between multiple equivalent forms of a statement, and conventions for when you find the normal naming conventions produce a very long name.)

#### Sebastien Gouezel (Sep 28 2020 at 20:09):

If anyone wants to change name, could you please wait until #4057 is merged (which hopefully shouldn't be long now) to avoid conflicts?

#### Wojciech Nawrocki (Sep 28 2020 at 21:14):

Patrick Massot said:

This discussion of Pythagoras in Euclid vs MetaMath and Lean is so ridiculous. He should read Kevin's blog.

Which Xena post are you referring to?

The latest one

#### Patrick Massot (Sep 28 2020 at 21:16):

It's called "Thoughts on the Pythagorean theorem".

#### Wojciech Nawrocki (Sep 28 2020 at 21:18):

Ah!

Mario Carneiro said:

What ever happened to lean --doc?

I think it's about to go, as metaprogramming turned out to be a better approach.

#### Wojciech Nawrocki (Sep 28 2020 at 21:59):

There is probably still value in quantifying the differences in complexity between less-or-more synthetic proofs of morally the same theorem, and even more value in comparing them between different low-level formal systems.

#### Mario Carneiro (Sep 28 2020 at 22:01):

Well, if you wanted to make a fair comparison you would do a synthetic proof of the pythagorean theorem in lean

#### Mario Carneiro (Sep 28 2020 at 22:02):

and then it wouldn't bring the entire library along with it as dependency

#### Wojciech Nawrocki (Sep 28 2020 at 22:14):

Indeed, if you wanted to compare a synthetic proof in Euclid vs a synthetic proof in Lean. What we can take OP to be, though, is a quantitative comparison of a synthetic proof with a fully unfolded one (modulo tactic modules and so on). Whether that was or wasn't the author's intention is of course another matter.

#### Mario Carneiro (Sep 28 2020 at 22:23):

I am reminded of the 2+2=4 page on metamath, which talks about the number of steps needed to prove 2+2=4. Depending on how you count, it's either around 5-10, or a few hundred, or ~30000, or ~10^400

#### Mario Carneiro (Sep 28 2020 at 22:24):

which is to say, it's really important how you count

#### Mario Carneiro (Sep 28 2020 at 22:27):

I think this example makes it really clear that the measure says far more about your measurement apparatus than the object under study. Those numbers are not specific to the example 2+2=4

#### Wojciech Nawrocki (Sep 28 2020 at 22:53):

Thanks, that's some fun trivia! Yeah, to measure how much more orange oranges are than apples you need a good notion of colour and perhaps Wolfram's isn't, but I would still think that such comparisons could be made, at least in principle.

#### Mario Carneiro (Sep 28 2020 at 23:32):

It is possible to make such comparisons, but you have to control for a lot of factors. I recommend Freek's paper on the de Bruijn factor

#### Kevin Buzzard (Sep 29 2020 at 12:52):

Here's a funny idea. For people who are expecting things like binomial_theorem or pythagorean_theorem we could capitalise and define the term to mean the statement of the theorem

#### Kevin Buzzard (Sep 29 2020 at 12:53):

Once the theorem is proved in informal pdf land, the name becomes stamped on both the theorem and the proof so mathematicians are already confused about this sort of thing

#### Scott Morrison (Sep 30 2020 at 00:01):

I'm tempted! I'm a bit concerned about how we'd get from "here" to "there". How do we decide which theorems deserve named statements? Do we do that gradually? Do we allow the "definition of a statement" without the proof?

#### Yury G. Kudryashov (Sep 30 2020 at 00:40):

I think that we can allow "well-known"names as aliases

#### Mario Carneiro (Sep 30 2020 at 00:42):

I've said this elsewhere, but I think that for "named" theorems we should use the names, modified as appropriate to indicate syntactic differences when there are multiple versions of a theorem. The symbol-based name is only useful if that's the main identifying feature of the theorem, which makes it good for things like group lemmas but not so good for advanced maths theorems

#### Mario Carneiro (Sep 30 2020 at 00:44):

That is, we should ask the question "what is the most likely way someone is going to attempt to find this theorem" and name the theorem after the identifying features in the head of that hypothetical someone

#### Rob Lewis (Oct 01 2020 at 16:27):

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/

image.png

#### Reid Barton (Oct 01 2020 at 16:47):

The big image at the top of the article is like one of those "What I think I do" memes

#### Jesse Michael Han (Oct 01 2020 at 17:41):

Reid Barton said:

The big image at the top of the article is like one of those "What I think I do" memes

lean-meme-2.jpg

#### Kevin Buzzard (Oct 01 2020 at 17:59):

Just reading the "hacker-proof code" article and I love the correction at the end:

Correction: This article was revised on September 21 to clarify that in formally verified software, each statement follows logically from the preceding one, not from the next.

#### Chris Wong (Oct 02 2020 at 00:52):

Perhaps they took "backwards reasoning" too literally?

#### Joe Hendrix (Oct 02 2020 at 07:40):

I'm glad they clarified. I also find it funny the article is called "Hacker-Proof Code Confirmed", and has the quote “We are much more clear about what we can and cannot do.”

Formal methods can show code satisfies specific properties, but it's pretty much impossible to formalize what it means for a complex system to be "hacker proof".

#### Johan Commelin (Nov 01 2020 at 06:14):

Scott Aaronson wrote:

Matt #24:

Are you aware of the Flypitch project? They recently completed a formal proof of the independence of CH using the Lean theorem prover, which I thought was pretty cool.

Yes, I came across that in my reading on the subject, and was duly impressed!

#### Johan Commelin (Nov 12 2020 at 06:04):

The quanta article is on HN again: https://news.ycombinator.com/item?id=25060613#25066033

#### Alex J. Best (Nov 20 2020 at 12:57):

https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista/

#### Johan Commelin (Nov 20 2020 at 13:18):

Wow, Andrej's answer is really good!

#### Sebastian Ullrich (Nov 20 2020 at 13:58):

I like the last one as well

#### Reid Barton (Nov 20 2020 at 14:04):

so far no one except Kevin just now has tried to answer the actual question being asked

#### Reid Barton (Nov 20 2020 at 14:06):

Is it really true that metamath doesn't have stuff like ring? I thought some of our tactics were basically ported from metamath by Mario. I know they aren't part of the metamath "core system" (whatever that means) but it doesn't mean external automation doesn't exist.

#### Reid Barton (Nov 20 2020 at 14:16):

Kevin, in the downvoted answer, pretty much every sentence contains a statement which is either false or meaningless

#### Johan Commelin (Nov 20 2020 at 14:20):

It is also comparing Lean to HoTT, instead of to a system that implements HoTT.

#### Mario Carneiro (Nov 20 2020 at 20:15):

@Reid Barton It is strictly true that metamath + addons doesn't have the ring tactic, but that's mostly because the lack of it wasn't painful enough for me to get off my butt and write it. It does have norm_num which works on almost exactly the same principle. It wasn't painful enough for me in lean either, but it was for Kevin, so ring was born. There is no metamath kevin

#### Mario Carneiro (Nov 20 2020 at 20:18):

Speaking of which, I invite anyone to crash the metamath mailing list and chip in on this proposal for a new metamath proof assistant. If you have considered metamath but found it too difficult to use, what are the things you would like to see in a proof assistant for it?

#### Bryan Gin-ge Chen (Nov 20 2020 at 20:31):

FWIW I tried out MMJ2 but gave up after running into various text editing bugs. So I think something fairly minimal that runs in VS Code would get me interested enough to experiment more with metamath. I'm also happy to be a guinea pig if there's something with MM0 / MM1 that's worth trying out now, since I cloned the repo and set it up at one point but wasn't sure what I should do with it.

#### Mario Carneiro (Nov 20 2020 at 20:48):

You should be able to view and edit the .mm1 files in the MM0 repo if you install mm0-rs and the vscode extension

#### Mario Carneiro (Nov 20 2020 at 20:50):

what I learned from MMJ2 development (which I also mention in that post) is to never write your own text editor. It's way too much work and the result will be crap unless that's your only goal

#### Kevin Buzzard (Nov 20 2020 at 21:40):

Wait -- aren't you writing a theorem prover? That's easier?

#### Mario Carneiro (Nov 20 2020 at 21:47):

A text editor looks simple, but it has really strict performance constraints. Syntax highlighting was my white whale in mmj2. Getting it to work smoothly while being semantically aware is tremendously complex; I totally understand why all the standard syntax highlighters are dumb regexes now

#### Mario Carneiro (Nov 20 2020 at 21:51):

When you are just a server like lean or mm0-rs, you can let the editor do the UI work while you chug along at whatever pace you need, and then report errors later. If the UI thread got blocked while lean was working, it would be absolutely unusable

#### Mario Carneiro (Nov 20 2020 at 21:53):

I'm pretty sure lean is smaller than vscode in terms of lines of code

#### Johan Commelin (Nov 20 2020 at 21:53):

Maybe we should rewrite VScode in Lean... would certainly save some lines of code :oops:

#### Mario Carneiro (Nov 20 2020 at 21:54):

plus even vscode isn't doing the heavy lifting for UI work, it's an electron app, meaning it's leveraging a browser engine

#### Mario Carneiro (Nov 20 2020 at 22:01):

mmj2 uses a "collaborative editing" model, where you type some stuff, press a button and the computer edits the same text you are writing to insert more information. This makes it somewhat synchronous by design; after you press the button you need to wait for the result or else your input will be clobbered. Syntax highlighting works at an even higher frequency; it basically needs to run any time you type a character or even scroll around. Java text boxes weren't really designed to support that, and the result is super janky as Brian observed

#### Johan Commelin (Nov 23 2020 at 05:02):

@Mario Carneiro said:

Speaking of which, I invite anyone to crash the metamath mailing list and chip in on this proposal for a new metamath proof assistant. If you have considered metamath but found it too difficult to use, what are the things you would like to see in a proof assistant for it?

One question: is Metamath Zero sufficiently different from classical Metamath that it can't be pitched as the next great Metamath verifier?

One of my biggest "problems" with metamath is I think readability. Lean is pretty unique, in the sense that you can give a pseudorandom theorem statement to a mathematician who doesn't know Lean, and then they can understand the statement. (The definition of a group is completely understandable, infinitude of primes is very readable.) With metamath, I know that you shouldn't try to read the source code, but even the dedicated website that renders the readable form is not really readable to me.
So I guess that my point is: readability (of at least one rendered form of the library) is extremely important. I can now barely read coq, but I don't like their ascii-art syntax either. Lean really hit a sweet spot here, in my opinion.

Just my two lay cents.

#### Mario Carneiro (Nov 23 2020 at 06:26):

One question: is Metamath Zero sufficiently different from classical Metamath that it can't be pitched as the next great Metamath verifier?

It's a different formal system, which means that none of the accumulated metamath verifiers over the years will verify .mm0 files. So it's a question of whether to migrate to the new system, which is kind of an all or nothing proposition. That thread is concerned with how to integrate with the existing language, so that it can be used to help develop set.mm, for example.

One of my biggest "problems" with metamath is I think readability. Lean is pretty unique, in the sense that you can give a pseudorandom theorem statement to a mathematician who doesn't know Lean, and then they can understand the statement. (The definition of a group is completely understandable, infinitude of primes is very readable.) With metamath, I know that you shouldn't try to read the source code, but even the dedicated website that renders the readable form is not really readable to me.

The state of the art of metamath rendering right now is the "structured view" that you can see in examples like http://metamath.tirix.org/fsumf1o.html . (There is a "structured view" button in the top right of any metamath web page, but note that these files are hosted on an external website so sometimes the pages are missing.) Some of the plans I discuss in the thread have the possibility to improve rendering by associating notation to constructs in a tree-structured way, something that metamath.exe has historically not been able to do, limiting it to sequences of GIF images that you usually see (I think unicode is the new default though).

The other reason you might find metamath web pages unreadable is the high density of symbols due to the presentation style that puts every step on a separate line. I'm sure if you presented lean proofs like this it would also be quite dense (generally single lean steps take up a whole page for the context, so the full thing would be huge). I can imagine a variety of tool assisted ways to make this more focused. Perhaps we can do something like the lean tactic view, where you see one step at a time and can scroll around; I'm not sure how effective this would be.

#### Johan Commelin (Nov 23 2020 at 06:43):

But MM0 can verify all of set.mm, and it's fast. Is the difference between set.mm and set.mm0 so big that it would be a big hurdle for the metamath community to jump over? Apparently yes. I'm too much of an outsider to really help here.
But mm0 has a couple of major benefits (like mmc, etc) that you would loose if you would start building a new version of mm, right?

#### Johan Commelin (Nov 23 2020 at 07:03):

@Mario Carneiro Here's a more precise question: would it be possible to do lossless bidirectional translation between set.mm and the MM0 version?

#### Mario Carneiro (Nov 23 2020 at 07:05):

Not without some extra hacks or annotations. Metamath can express some things that MM0 can't

#### Mario Carneiro (Nov 23 2020 at 07:06):

in particular ambiguously parsable expressions and bound variables that may or may not be distinct

#### Mario Carneiro (Nov 23 2020 at 07:07):

set.mm0 is not very easy to read right now, as it loses all metamath notations

#### Mario Carneiro (Nov 23 2020 at 07:08):

also comments but that's not so hard to fix

#### Johan Commelin (Nov 23 2020 at 07:08):

One issue is that MM1 is a proof assistant for MM0, it doesn't currently support MM. One way I would like to support this is to be able to "import "foo.mm";" in an MM1 file, which will convert the MM theorems into MM1 and import them into the current file; this will make it easy to build on set.mm from within an MM0 development, but it doesn't "give back" to the MM database, it is a one way conversion (at least so far), and even if the reverse conversion were added it would probably not be the inverse map, resulting in ugly proofs after round-tripping.

#### Johan Commelin (Nov 23 2020 at 07:08):

I will read through that entire thread before opening my mouth again :face_palm: :smiley:

#### Mario Carneiro (Nov 23 2020 at 07:09):

The plan for now is to instead use mm0-rs the proof assistant, but "swap out the foundation" on it so that it works with metamath rules

#### Mario Carneiro (Nov 23 2020 at 07:10):

this might require some minor syntax changes but I think the majority of the UI can stay the same

#### Mario Carneiro (Nov 27 2020 at 01:03):

Not really lean, but I'm excited to unveil the new MM0 doc-gen HTML pages. I would be happy to take suggestions and modifications from some of the web-savvy folks behind the mathlib docs, because web design isn't my strong suit. Also ideas for more interactivity would be great.

#### Kevin Buzzard (Nov 28 2020 at 14:24):

More Buzzard propaganda: https://www.ams.org/journals/notices/202011/rnoti-p1791.pdf

#### Bryan Gin-ge Chen (Nov 28 2020 at 14:35):

The link to the web editor on the right column of page 1794 (p.4 in the PDF) does not seem to work.

Thanks!

#### Johan Commelin (Nov 28 2020 at 16:13):

@Kevin Buzzard We will now see about how Lean understands these concepts. Should that "about" be there?

#### Kevin Buzzard (Nov 28 2020 at 16:24):

That sentence does look a bit funny, yes

#### Kevin Buzzard (Nov 28 2020 at 16:25):

Stupid old media. I guess I just have to get in touch with AMS

#### Johan Commelin (Nov 28 2020 at 16:28):

contains over a quarter of a million lines of code :rofl:

#### Johan Commelin (Nov 28 2020 at 16:28):

@Kevin Buzzard You might want to update your mathlib (-;

#### Rob Lewis (Nov 28 2020 at 16:41):

It's a bit over 270k lines of non-whitespace, non-comment code in the src directory!

ok, fair enough

#### Johan Commelin (Nov 28 2020 at 17:15):

Nice touch that they used a picture of Martijn Heules work as background image for the "ad" next to your article.

#### Jasmin Blanchette (Nov 28 2020 at 21:06):

Coming soon to the Stedelijk Museum. ;)

#### Bryan Gin-ge Chen (Dec 24 2020 at 07:50):

I happened on an interesting blog post by Richard Lipton on @Kevin Buzzard's Notices article. Aside from calling Lean $L \exists \forall N$, he also expresses some skepticism about "formal verification as the answer to correctness", though the post ultimately ends on a hopeful note.

#### Johan Commelin (Dec 24 2020 at 08:22):

I see an opportunity for a new meme: "Lean is like marmite"...

#### Jason Rute (Dec 24 2020 at 13:19):

How about we insist that claimed proofs of P{=}NP or other famous conjectures must be presented using L\exists \forall N.

This sounds great until you realize all these people would be coming here to Zulip and likely complaining why Lean can’t obviously handle their proof. :slight_frown:

#### Jason Rute (Dec 24 2020 at 13:24):

Although to his credit, when the Princeton logician Edward Nelson thought he had a proof of the inconsistency of Peano Arithmetic he did plan to formalize it knowing that no one would believe him otherwise. (Luckily, in that case Terry Tao and others spotted an error in his logic after he stated the proof outline, and he retracted his claim.)

#### Julian Berman (Dec 24 2020 at 14:04):

I still don't get why we americans are so tickled by slight differences in British English.

#### Kevin Buzzard (Dec 24 2020 at 14:18):

Jason Rute said:

Although to his credit, when the Princeton logician Edward Nelson thought he had a proof of the inconsistency of Peano Arithmetic he did plan to formalize it knowing that no one would believe him otherwise. (Luckily, in that case Terry Tao and others spotted an error in his logic after he stated the proof outline, and he retracted his claim.)

This is exactly why pure mathematicians don't need theorem provers to do research -- the elders can play the game well enough in their heads.

#### Kevin Buzzard (Dec 24 2020 at 14:20):

Doing maths in your head is far more efficient because you don't have to get bogged down in the tedious details which the tactics still can't do but which the human knows will all work out fine (and are 99.99% likely to be correct).

#### Rob Lewis (Dec 24 2020 at 15:31):

Ugh, I can barely read this because of the $L\exists\forall N$ nonsense. He even writes that two words before the official blurb which says "Lean."

#### Julian Berman (Dec 24 2020 at 15:51):

Since I don't see it mentioned here ... @Kevin Buzzard you're also at the top of /r/math in Quanta's The Year's Biggest Breakthroughs in Math & Computer Science -- https://www.youtube.com/watch?v=HL7DEkXV_60

Oh wow!

#### Kenny Lau (Dec 24 2020 at 16:14):

Did you know that when you recorded the recording? @Kevin Buzzard

#### Kevin Buzzard (Dec 24 2020 at 16:24):

I had not realised that they were going to do that with it. I was told that it would be "part of an end-of-year round-up".

#### Faez (Dec 24 2020 at 17:44):

Julian Berman said:

Since I don't see it mentioned here ... Kevin Buzzard you're also at the top of /r/math in Quanta's The Year's Biggest Breakthroughs in Math & Computer Science -- https://www.youtube.com/watch?v=HL7DEkXV_60

I joined this chat after watching that video by quanta magazine. I've always felt a need for something like Library of Mathematics to help me learn and fill the gaps in my knowledge. And watching Kevin in that video got me real excited about Lean, and I went through whatever links related to lean I could find haha

#### Eric Wieser (Dec 24 2020 at 18:34):

As someone's whose gaps in knowledge span most of an undergrad mathematics degree, I've found that using lean to fill those gaps often results in me using names for things that confuse "real" mathematicians

#### Johan Commelin (Dec 24 2020 at 18:35):

ooh... is that good or bad news? would you mind giving some examples?

#### Eric Wieser (Dec 24 2020 at 18:40):

I could probably pull up the zulip thread, but I don't remember the context

#### Alena Gusakov (Dec 28 2020 at 15:28):

As someone's whose gaps in knowledge span most of an undergrad mathematics degree, I've found that using lean to fill those gaps often results in me using names for things that confuse "real" mathematicians

To be fair, "real" mathematicians also have differing conventions all the time, so I don't really see anything wrong with that

#### Jason Rute (Jan 05 2021 at 17:50):

Christian Szegedy just expressed interest in learning Lean. https://twitter.com/ChrSzegedy/status/1346189173196087296

#### Julian Berman (Jan 09 2021 at 21:00):

@Carl Friedrich Bolz-Tereick just mentioned (on an unrelated Twitch stream) that Mark Dickinson, who wrote Python 3.8's new math.isqrt function for computing integer-valued square roots, also wrote a Lean proof that it's correct: https://github.com/mdickinson/snippets/blob/master/proofs/isqrt/src/isqrt.lean

#### Bryan Gin-ge Chen (Jan 09 2021 at 21:05):

This is cool and well-documented! (An updated version would fit nicely into mathlib's archive/. Too bad there's no license.)

/me waves

#### Alex J. Best (Jan 27 2021 at 09:29):

https://mathoverflow.net/questions/382239/proof-that-a-cartesian-category-is-monoidal
is this the first time someone has answered an MO question in this way?

#### Johan Commelin (Jan 27 2021 at 09:31):

/me logs in to upvote

#### Jason Rute (Mar 03 2021 at 13:20):

In about 7 hours, at 3pm EST (UTC-5) on Zoom, I'm going to give a talk at the Harvard New Technologies in Mathematics seminar on our machine learned Lean gptf tactic and the PACT method we use to train the current version. (My understanding is that a number of members of that seminar have been learning Lean.) There will be a demo of gptf. Here is the abstract and Zoom link. I also think it will be recorded and put on YouTube. I think the best place to discuss this will be at the #lean-gptf stream (but we will be happy to field questions anywhere).

#### Alex J. Best (Mar 04 2021 at 04:41):

I think they usually take a few days to upload them but it should end up on https://youtube.com/playlist?list=PL0NRmB0fnLJQJ3fuIk3yVULtm6_JnQ_zI

#### Jason Rute (Mar 05 2021 at 23:36):

Also there are slides here.

#### Jason Rute (Mar 05 2021 at 23:37):

We'd love for you to try out the tool. Join the discussion at #lean-gptf (or go straight to https://github.com/jesse-michael-han/lean-gptf for setup instructions.)

#### Scott Morrison (Mar 08 2021 at 05:11):

https://github.com/jesse-michael-han/lean-gptf#importing-lean-gptf-as-a-dependency-for-your-own-project explains how to set it up as a dependency of a project. However this is not a viable approach for someone working directly in mathlib (e.g. many people here).

Do you have suggestions for using gptf regularly within mathlib?

#### Jason Rute (Mar 08 2021 at 13:18):

I moved this last discussion to it's own thread #lean-gptf > Using gptf in mathlib development

#### Anthony Bordg (Mar 10 2021 at 12:02):

A Replication Crisis in Mathematics?, an article published in The Mathematical Intelligencer that may interest some of you.

#### Kevin Buzzard (Mar 10 2021 at 19:06):

Nice :-) When I was having my midlife crisis in 2017-18 I was very worried about mathematics but having talked to a lot of people recently about this, I am now much more assured about the current state of pure maths.

#### Anthony Bordg (Mar 14 2021 at 09:45):

Kevin Buzzard said:

Nice :-) When I was having my midlife crisis in 2017-18 I was very worried about mathematics but having talked to a lot of people recently about this, I am now much more assured about the current state of pure maths.

Hello @Kevin Buzzard ,

thanks.
There may be a misunderstanding here, it's not really about the current state of pure maths, but about the current state of peer review. Of course, the problem is that both are intertwined in subtle ways.

#### Joe Hendrix (Mar 14 2021 at 20:26):

Rather than focusing on the benefits of higher assurance from formalized computer mathematics, I wonder if the main benefit will be enabling collaboration on a larger and more rapid scale.
As a computer scientist, it is impressive the way the folks in the mathematics community are able to remotely collaborate on the proof process for mathlib and the condensed mathematics work. Is Lean facilitating that collaboration or is that more common in mathematics than computer science?

#### Kevin Buzzard (Mar 14 2021 at 20:35):

In collaborating on research we mostly work on our own or in groups of at most 3. But mathlib and the condensed stuff are of a different nature -- this is not people working together to make new mathematics, this is people translating old mathematics, and so there is a huge group of people who knows the maths well and it's easy to work on your own thing and then find that other people are using it. The condensed stuff is basically being led by Johan Commelin and he constantly makes it clear what needs doing, and people find their own sub-projects (e.g. I messaged him this morning to say "I have a few hours today, what shall I do?" and he pointed me to a lean file and a page of a maths pdf and I just got on with it).

#### Joe Hendrix (Mar 14 2021 at 23:28):

@Kevin Buzzard That makes sense. I don't know of corresponding analogs in computer science/software engineering, but I can see how that enables a more distributed and larger effort. For software, there is no group I know of out to formalize something like Windows 95.

A slightly different angle on selling this to mathematicians would be if formalization accelerated acceptance of an idea. e.g., if the condensed mathematics formalization work convinced people the work was good and well-founded faster than traditional peer review. I suspect proof assistants have a ways to go before that pans out. That's how I'd eventually like to be able to convince people of the value of formal methods in software -- a client/end-user can trust a new system or software because we have rigorous evidence that it works as intended even though the traditional social processes (e.g, existing system developers) are trying to convince that person to be skeptical.

#### Kevin Buzzard (Mar 14 2021 at 23:32):

People are convinced by condensed mathematics because a Fields Medallist who just proved the local Langlands conjectures wrote it down, and preliminary study groups all over the world didn't reveal any problems.

#### Joe Hendrix (Mar 14 2021 at 23:33):

Seems like a good reason.

#### Julian Berman (Mar 14 2021 at 23:34):

For software, there is no group I know of out to formalize something like Windows 95.

Maybe something like Jepsen (https://aphyr.com/tags/Jepsen) is an analog in computer science? Someone (in this case one person really, aphyr), a piece of software, trying to increase the correctness of distributed system software, but each individual software component driven by its own small groups, and generally being pre-existing systems?

#### Joe Hendrix (Mar 15 2021 at 00:00):

I hadn't heard of Jepson, but that seems relevant. It seems like somebody doing a more rigorous analysis than most pen testing or fuzzing. I think there are a lot of small analogues like that in computer science where a person or group (like Google Project Zero). I guess the Linux kernel and Debian are also analogues given the huge number of people from different backgrounds collaborating to make a reliable system that gets adoption even though they use tests and other software engineering practices rather than formalization.

#### Kevin Buzzard (Mar 15 2021 at 00:00):

It's probably also worth saying that I don't really know of anything else going on in mathematics which is like this whole mathlib adventure. We have these polymath projects, an idea of collaborative mathematics set up by Gowers which worked very well, and of course we have mathoverflow, but the mathlib project is not really like either of these things.

#### Julian Berman (Mar 15 2021 at 00:07):

What about e.g. The Princeton Companion to Mathematics?

#### Julian Berman (Mar 15 2021 at 00:08):

If you remove the formalization part it's another case of getting a whole lot of mathematicians to pool together their respective fields into one cohesive "view" of math as a whole

#### Julian Berman (Mar 15 2021 at 00:09):

@Joe Hendrix you might like OSS-Fuzz too I guess, if you haven't seen it: https://github.com/google/oss-fuzz/ -- I think there's a bunch of pockets of people trying to take some systemic approach to a technique they think improves general software reliability and then trying to run it on a bunch of other peoples' projects

#### Julian Berman (Mar 15 2021 at 00:09):

(in that case fuzz testing obviously)

#### Kevin Buzzard (Mar 15 2021 at 00:12):

Julian Berman said:

What about e.g. The Princeton Companion to Mathematics?

What about it? I wrote the article on modular forms in there :D But I didn't really look at many of the other articles. Isn't it just basically a worse version of Wikipedia?

#### Julian Berman (Mar 15 2021 at 00:15):

Oh! Did you, interesting! I don't know, I guess as opposed to Wikipedia which spreads/expands "arbitrarily" based on whatever people are editing it seemed more like the companion was an attempt to "evenly" cover the subfields in some systematic way. But yeah I'm not sure where I was going with that relative to mathlib, it was just another example of collaborative mathematics that came to mind.

#### Kevin Buzzard (Mar 15 2021 at 00:16):

I was super-skeptical about the whole idea even at the time. I wrote 2 articles in the final version I think, but I never looked at the book or bought a copy -- I was just thinking "why are all these old people fussing about making a massive book when we have Wikipedia?" Wikipedia was just beginning to catch on at the time.

#### Julian Berman (Mar 15 2021 at 00:17):

Somehow it played a small part in me getting a math degree so I always felt a small bit of debt to it, even though I understood very little of what was in it

#### Julian Berman (Mar 15 2021 at 00:18):

I was in college when it came out, and it was just at the time I needed to decide on a major, and unlike wikipedia it was easier to leaf through that and get a picture for all of the subject at once or something rather than the more haphazard clicking through links

#### Joe Hendrix (Mar 15 2021 at 00:31):

Joe Hendrix you might like OSS-Fuzz too I guess, if you haven't seen it: https://github.com/google/oss-fuzz/

My main interest is finding good arguments for formal methods adoption. I'm a big fan of tools such as Lean and think part of it will be just doing interesting work using such tools. Kevin's point though that condensed mathematics is already accepted by the social processes (including Peter Scholze's involvement) is useful so I don't am less likely to make dumb arguments.

#### Peter Nelson (Mar 18 2021 at 14:14):

I will be giving a talk on my efforts to formalize matroids in lean at 3PM EDT on Monday March 22. The talk will be mostly aimed at combinatorialists rather than formalizers (it will include a fair amount of evangelizing) , but I thought I'd share the link here. The zoom password is my surname followed by the second-smallest term in nat with the usual ordering.

http://matroidunion.org/

#### Bryan Gin-ge Chen (Mar 18 2021 at 15:23):

@Peter Nelson I won't be able to attend live, will the talk be recorded?

#### Julian Berman (Mar 18 2021 at 16:01):

Is the matroid code somewhere accessible to other folks (yet?)? I forget if you mentioned the plans for that in the Lean Together talk

#### Peter Nelson (Mar 18 2021 at 17:42):

https://github.com/e45lee/lean-matroids

Around 10000 loc - a lot of it is basic API stuff I wrote while still learning, so it will be certainly possible to tighten up. The main theorems proved are the matroid intersection theorem (matroid/intersection-union/matroid_inter.lean) and Kung's lemma ( matroid/uniform_minor/kung.lean). Mathematically nothing impressive, but getting to the point where I could reasonably state and prove these results took longer than I imagined...

#### Kevin Buzzard (Mar 18 2021 at 18:06):

Hey Kung's Lemma https://github.com/e45lee/lean-matroids/blob/master/src/matroid/uniform_minor/kung.lean#L92-L142 has come out really nicely -- and it's great that you have documented some of these proofs.

Speaking from experience, it's extremely difficult to keep up with mathlib, it moves too fast. You should PR this work or it will die.

#### Peter Nelson (Mar 18 2021 at 18:53):

I would like to PR it - at the moment, I really don't know where to start, though!

#### Peter Nelson (Mar 18 2021 at 18:53):

I have been updating mathlib regularly and fixing the small issues that arise - is that not a sustainable approach?

#### Kevin Buzzard (Mar 18 2021 at 18:54):

it's fine as long as you're happy doing that forever.

#### Kevin Buzzard (Mar 18 2021 at 18:55):

The point is that after you PR it, anyone who breaks it has to fix it themselves, so you don't have to do it.

#### Scott Morrison (Mar 18 2021 at 21:54):

Updating mathlib regularly yourself is only sustainable during the period you are actively developing the code. As soon as it's "finished", it will likely start to rot.

#### Scott Morrison (Mar 18 2021 at 21:59):

Start with small PRs. e.g. presumably everything in https://github.com/e45lee/lean-matroids/blob/master/src/prelim/set.lean can come across without prerequisites (possibly with some fraction already existing under different names).

#### Peter Nelson (Mar 19 2021 at 14:39):

Thanks - I will look into cleaning the basic stuff up and making it PR-ready.

One concern I have is with stuff in the project that is just kinda kooky. For instance, I use a function called size rather than finset.card (or really, fincard, which I'm waiting to find its way in). The difference is that size is int-valued rather than nat-valued, and the reason for this choice is because subtracting sizes from eachother and other int-valued expressions happens all the time, and I never want to worry about nat subtraction. The alternative would involve a bunch of fussy bookkeeping before each invocation of linarith.

And size gets used from the very beginning to do everything. I'm very comfortable with this decision for my project, but I don't imagine it would suit mathlib very well to have a separate API simply for the coercion of finset.card or fincard to int. Is there a workable solution to this?

#### Julian Berman (Mar 22 2021 at 20:46):

@Peter Nelson your talk was nice to watch thanks for sharing the invite.

#### Alena Gusakov (Mar 23 2021 at 00:42):

I would like to PR it - at the moment, I really don't know where to start, though!

I can help with PRs! I still have yet to really dive into what you wrote so that would be a good excuse for me to do so

#### Peter Nelson (Mar 24 2021 at 12:10):

https://youtu.be/wMRrSWsZSFM

About an hour long - I talk about proof assistants in general, and the lean-matroids project. The highlight is where I give an incorrect definition of prime number in the demo without noticing.

#### Yakov Pechersky (May 05 2021 at 20:58):

https://crismathsblog.blogspot.com/2021/04/is-my-computer-better-than-me-at-math.html?m=1

#### Kevin Buzzard (May 05 2021 at 21:09):

Oh nice! I'm involved with that competition.

#### Yaël Dillies (May 06 2021 at 06:54):

I found this problem particularly elegant. My proof went on writing the perpendicular and parallel components, and checking that the LHS and RHS were exactly one term away from each other.

#### Yaël Dillies (May 06 2021 at 08:33):

As usual with scalar product inequalities, you can get it by expanding the norm of a carefully chosen element.

Last updated: May 07 2021 at 00:30 UTC