Zulip Chat Archive

Stream: general

Topic: Lean in the wild


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

view this post on Zulip Andrew Ashworth (Nov 29 2018 at 08:42):

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

view this post on Zulip Johannes Hölzl (Dec 04 2018 at 17:16):

and another one: https://twitter.com/scottfleischman/status/1069965177641160707

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 07:17):

https://www.reddit.com/r/math/comments/a3zujc/the_xena_project_i_would_like_to_see_the_main/

view this post on Zulip Johan Commelin (Dec 08 2018 at 10:41):

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

view this post on Zulip Johan Commelin (Dec 08 2018 at 10:42):

Anyway, congrats with the visibility!

view this post on Zulip Kenny Lau (Dec 08 2018 at 10:54):

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

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

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

view this post on Zulip Mario Carneiro (Feb 06 2019 at 11:03):

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

view this post on Zulip Rob Lewis (Feb 06 2019 at 11:06):

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

view this post on Zulip Mario Carneiro (Feb 06 2019 at 11:14):

actually I think you're right

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

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

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

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 12:26):

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

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

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 12:27):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:28):

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

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 12:28):

yeah but look at the set theorists.

view this post on Zulip Johan Commelin (Feb 12 2019 at 12:28):

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

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 12:28):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:28):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:29):

you can, that's kind of the point

view this post on Zulip Johannes Hölzl (Feb 12 2019 at 12:29):

Most of analysis works in HOL.

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:29):

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

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

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

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 12:29):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:30):

you just can't call it a dependent type

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 12:30):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:30):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:30):

no dependent types here

view this post on Zulip Mario Carneiro (Feb 12 2019 at 12:30):

doesn't matter how fancy X and Y are

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 20 2019 at 20:14):

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

view this post on Zulip Scott Morrison (Mar 20 2019 at 21:19):

Pretty cool, Kevin! I hope people read this.

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

view this post on Zulip Patrick Massot (Mar 20 2019 at 21:23):

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

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

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

view this post on Zulip Andrew Ashworth (Mar 20 2019 at 22:24):

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

view this post on Zulip Andrew Ashworth (Mar 20 2019 at 22:24):

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

view this post on Zulip Andrew Ashworth (Mar 20 2019 at 22:25):

It is a decades-long crisis :sunglasses:

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

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

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 13:20):

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 13:20):

This sort of thing has come up before

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

view this post on Zulip Simon Hudon (Mar 29 2019 at 13:24):

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

view this post on Zulip Kenny Lau (Mar 29 2019 at 13:28):

hey I wrote that code :P maybe I should answer

view this post on Zulip Johan Commelin (Mar 29 2019 at 13:28):

You are taking a break from Lean (-;

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 13:50):

https://stackoverflow.com/questions/55014276/how-to-remove-a-universal-quantifier-in-lean one two weeks ago

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

view this post on Zulip Simon Hudon (Mar 29 2019 at 14:40):

... so the opposite of redirecting people here

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 15:40):

https://twitter.com/JSEllenberg/status/1111248659063205899

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 15:41):

Jordan tweeted to his 11.7K followers :D

view this post on Zulip Johan Commelin (Mar 29 2019 at 15:41):

Did he just misunderstand what happened?

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 15:43):

I am pretty sure that he did not :-)

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 15:43):

he's just being a wag

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 16:46):

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

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

view this post on Zulip Johan Commelin (Mar 29 2019 at 19:12):

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

view this post on Zulip Johan Commelin (Mar 29 2019 at 19:13):

So that's also quite some stuff from other chapters

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

view this post on Zulip Kevin Buzzard (May 12 2019 at 17:12):

https://twitter.com/johncarlosbaez/status/1127616867391066113

view this post on Zulip Kevin Buzzard (May 12 2019 at 21:56):

@Patrick Massot there is some chat after Baez' tweet about your graph: https://twitter.com/JadeMasterMath/status/1127615276151783424 . Do you do Twitter?

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

view this post on Zulip Kevin Buzzard (May 21 2019 at 23:32):

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

view this post on Zulip Mario Carneiro (May 21 2019 at 23:38):

not a single tweet. sounds about right

view this post on Zulip Mario Carneiro (May 21 2019 at 23:40):

lots of followers though, haha

view this post on Zulip Kevin Buzzard (Jun 04 2019 at 19:48):

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

view this post on Zulip Scott Morrison (Jun 04 2019 at 20:07):

I commented, including inviting people here ...

view this post on Zulip Johannes Hölzl (Jun 06 2019 at 18:05):

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

view this post on Zulip Simon Hudon (Jun 06 2019 at 18:12):

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

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

view this post on Zulip Simon Hudon (Jun 06 2019 at 18:31):

All papers have authors who are or have been at CMU

view this post on Zulip Simon Hudon (Jun 06 2019 at 18:38):

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

view this post on Zulip Johannes Hölzl (Jun 06 2019 at 18:39):

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

view this post on Zulip Simon Hudon (Jun 06 2019 at 18:40):

That answers my question

view this post on Zulip Patrick Massot (Jun 06 2019 at 19:07):

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

view this post on Zulip Mario Carneiro (Jun 06 2019 at 19:09):

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

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 19:15):

I once managed to get a problem onto the IMO!

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 19:15):

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

view this post on Zulip Patrick Massot (Jun 06 2019 at 19:22):

We need you to get Lean to win the contest!

view this post on Zulip Patrick Massot (Jun 06 2019 at 19:23):

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

view this post on Zulip Mario Carneiro (Jun 06 2019 at 19:26):

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

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 19:26):

that would be good

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 19:26):

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

view this post on Zulip Patrick Massot (Jun 06 2019 at 19:27):

I need to suggest defining Lebesgue integral

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

view this post on Zulip Patrick Massot (Jun 06 2019 at 19:33):

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

view this post on Zulip Mario Carneiro (Jun 06 2019 at 19:33):

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

view this post on Zulip Mario Carneiro (Jun 06 2019 at 19:33):

but it's not hard to do

view this post on Zulip Patrick Massot (Jun 06 2019 at 19:36):

How can it be half an hour and overcomplicated?

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

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

view this post on Zulip Reid Barton (Jun 06 2019 at 19:42):

I think at this point it just needs typing in

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

view this post on Zulip Mario Carneiro (Jun 06 2019 at 19:47):

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

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

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

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

view this post on Zulip Tim Daly (Jun 07 2019 at 00:57):

Who controls this website?

view this post on Zulip Mario Carneiro (Jun 07 2019 at 01:03):

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

view this post on Zulip Mario Carneiro (Jun 07 2019 at 01:04):

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

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

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

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

view this post on Zulip Tim Daly (Jun 07 2019 at 02:18):

In theory I've created a correct pull request.

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

view this post on Zulip Simon Hudon (Jun 07 2019 at 12:38):

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

view this post on Zulip Kevin Buzzard (Jun 07 2019 at 12:55):

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

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

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

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

view this post on Zulip Kevin Buzzard (Jun 13 2019 at 08:29):

https://galoisrepresentations.wordpress.com/2019/06/12/harris-versus-buzzard/

view this post on Zulip Kevin Kappelmann (Jun 13 2019 at 09:30):

Is that face-off on the 20th of June in Paris recorded by any chance?

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 13:28):

I was thinking of talking about what makes a mathematician tick.

view this post on Zulip Kevin Buzzard (Jun 30 2019 at 22:22):

https://twitter.com/derKha/status/1145412656632930304

view this post on Zulip Scott Morrison (Jun 30 2019 at 22:37):

I use \mapsto inside an expression.

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Simon Hudon (Jul 01 2019 at 02:14):

Does that issue arise often?

view this post on Zulip Johan Commelin (Jul 01 2019 at 02:14):

Well, maybe we don't hear those users, because they don't even consider Lean atm...

view this post on Zulip Johan Commelin (Jul 01 2019 at 02:14):

Is .\ a faithful ASCII rendition of lambda?

view this post on Zulip Johan Commelin (Jul 01 2019 at 02:15):

.\ x. e :scream_cat:

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

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

view this post on Zulip Mario Carneiro (Jul 01 2019 at 02:27):

I would be happy to see \mapsto, although it might be tricky to parse

view this post on Zulip Keeley Hoek (Jul 01 2019 at 02:35):

ATTACK OF ZE SEMICOLONS

view this post on Zulip Keeley Hoek (Jul 01 2019 at 02:35):

https://github.com/leanprover/lean4/commit/5c4ec3082099a7e1b008ced0db162c7cac16663a

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

view this post on Zulip Tim Daly (Jul 01 2019 at 03:06):

Guy Steele on logic notation: https://www.youtube.com/watch?v=dCuZkaaou0Q

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

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

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

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

view this post on Zulip Keeley Hoek (Jul 01 2019 at 09:38):

(x : nat, y : int) ↦ x + y

view this post on Zulip Keeley Hoek (Jul 01 2019 at 09:39):

The java compiler can parse that

view this post on Zulip Keeley Hoek (Jul 01 2019 at 09:39):

(I mean an isomorphic expression)

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

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

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

view this post on Zulip Patrick Massot (Jul 01 2019 at 11:24):

What about using python's λ x: e? At least it's not a period

view this post on Zulip Andrew Ashworth (Jul 01 2019 at 11:30):

we can make everybody unhappy and do λx ↦ e

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

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

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

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

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

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

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

view this post on Zulip Jeremy Avigad (Jul 01 2019 at 20:14):

It is possible to get used to anything.

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

view this post on Zulip Patrick Massot (Jul 01 2019 at 20:38):

No, we use 1 000 000.

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

view this post on Zulip Andrew Ashworth (Jul 17 2019 at 22:48):

ooh, if I have time, I want to check this out

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

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 08:16):

https://arxiv.org/abs/1907.07801

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2019 at 12:15):

The relevant code seems to be here: https://github.com/NeilStrickland/itloc

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Sep 02 2019 at 16:34):

@Kevin Buzzard Gijswijt's name is missing on p33

view this post on Zulip Kevin Buzzard (Sep 02 2019 at 17:23):

Noo!

view this post on Zulip Kevin Buzzard (Sep 02 2019 at 17:23):

:-(

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

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

view this post on Zulip Johan Commelin (Sep 02 2019 at 17:30):

Wow, that's some really good editing!

view this post on Zulip Kevin Buzzard (Sep 02 2019 at 17:32):

The London Mathematical Society runs on a shoestring.

view this post on Zulip Johan Commelin (Sep 02 2019 at 17:32):

Can they still fix it? Or is it already printed?

view this post on Zulip Kevin Buzzard (Sep 02 2019 at 17:33):

I have no idea. I'll ask.

view this post on Zulip Kevin Buzzard (Sep 04 2019 at 03:50):

It will be fixed online when people are back from holidays

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

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

view this post on Zulip Olli (Sep 26 2019 at 16:06):

https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually

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

view this post on Zulip Kevin Buzzard (Sep 26 2019 at 16:07):

That's just a completely click-baity title which does not represent my views.

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

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

view this post on Zulip William Whistler (Sep 26 2019 at 16:18):

Is that a made-up quote?

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

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

view this post on Zulip Kevin Buzzard (Sep 26 2019 at 16:23):

Well, we live and learn :-/

view this post on Zulip Rob Lewis (Sep 26 2019 at 16:23):

Heh, it's not the worst thing Vice has ever published.

view this post on Zulip Kevin Buzzard (Sep 26 2019 at 16:23):

:-)

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

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

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

view this post on Zulip Johan Commelin (Sep 27 2019 at 04:44):

@Kevin Buzzard Time for a rectification blogpost? :grimacing: :wink:

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

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

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

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

view this post on Zulip Johan Commelin (Sep 27 2019 at 11:42):

But Frank hasn't provided a proof of his counterclaim. Not even a "mathematical" proof (-;

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

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

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

view this post on Zulip Kevin Buzzard (Sep 27 2019 at 14:23):

Yes.

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

view this post on Zulip Chris Hughes (Sep 27 2019 at 22:36):

My phone showed me this today https://www.popularmechanics.com/science/math/a29252622/is-math-wrong/

view this post on Zulip Kevin Buzzard (Sep 28 2019 at 12:39):

Good to see it mentions Lean!

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

view this post on Zulip Jesse Michael Han (Sep 29 2019 at 17:03):

kevin just hit # 1 on hacker news: https://news.ycombinator.com/item?id=21107706

view this post on Zulip Kevin Buzzard (Sep 29 2019 at 21:17):

Amazing what a clickbait headline can do!

view this post on Zulip Kevin Buzzard (Sep 29 2019 at 21:17):

TPIL is #12! That's a good thing.

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

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

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

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

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

view this post on Zulip Tim Daly (Sep 30 2019 at 11:00):

"pile of sand" (POS) ...

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:01):

Mathlib is currently in the process of documenting definitions and major theorems

view this post on Zulip Tim Daly (Sep 30 2019 at 11:01):

How long have you been using Lean?

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:01):

But I think one can go overboard on the other side

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:02):

There was a time when I had not yet used Lean for a very long time...

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

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

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:04):

Etc...

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

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

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:16):

If only Knuth were to write an ITP...

view this post on Zulip Tim Daly (Sep 30 2019 at 11:17):

Or a text that explains BDDs for solvers :-)

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

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

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:20):

The average math paper from <1950s is unreadable for us.

view this post on Zulip Tim Daly (Sep 30 2019 at 11:21):

Yeah, I struggled with Frege's papers due to notation

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

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:24):

Tim, that's simply not true

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:25):

There are dozens of lemmas in the library that are exactly the opposite of being creative

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:25):

They are there only to handhold the system

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:25):

I think you mean "thousands"

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:27):

Right, that's a better way of putting it

view this post on Zulip Tim Daly (Sep 30 2019 at 11:27):

Well, it will then grow into the millions if Kevin Buzzard's dream comes true.

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:27):

"mathlib does the piddling details so you don't have to"

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:28):

group.lean is not group theory. It is basic highschool algebra

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:28):

nothing in that file has a name in math

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:28):

it is not representative of all of math

view this post on Zulip Tim Daly (Sep 30 2019 at 11:29):

Does it have an "idea" in math? And is that "idea" properly communicated in 16 characters?

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:29):

although coming from a CAS background you might become disproportionately interested in that material

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:30):

but mathematicians are looking much further afield

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:30):

no, it does not have an "idea"

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:30):

its meaning is completely described by the statement of the theorem itself

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:30):

a * (a^-1 * b) = b is just that

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

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

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

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:32):

again, group.lean is not representative

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:32):

look around

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

view this post on Zulip Tim Daly (Sep 30 2019 at 11:33):

Are you suggesting that there ARE books in Lean?

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:33):

TPIL?

view this post on Zulip Tim Daly (Sep 30 2019 at 11:33):

I'm reading that.

view this post on Zulip Tim Daly (Sep 30 2019 at 11:34):

Ah, well. I'm done.

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 11:52):

No. That is not the key question.

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

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

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

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:55):

Johan didn't say Lean, he said ITPs

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:55):

what is it that the ITP community lacks right now that is preventing world domination?

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

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

view this post on Zulip Mario Carneiro (Sep 30 2019 at 11:56):

Tim, that kind of happened with lean 3

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

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

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

view this post on Zulip Tim Daly (Sep 30 2019 at 12:00):

Books, however, count.

view this post on Zulip Johan Commelin (Sep 30 2019 at 12:00):

It depends...

view this post on Zulip Johan Commelin (Sep 30 2019 at 12:00):

... on the contents.

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

view this post on Zulip Mario Carneiro (Sep 30 2019 at 12:02):

once it becomes sufficiently relevant it won't be career suicide anymore

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

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

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

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

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

view this post on Zulip Johan Commelin (Sep 30 2019 at 12:14):

It is extremely small, fast, and very flexible in its foundations

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

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

view this post on Zulip Tim Daly (Sep 30 2019 at 12:18):

As a mathematician, why aren't you using Axiom?

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (Sep 30 2019 at 13:13):

You could also just reimplement selected algorithms in lean

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

view this post on Zulip Tim Daly (Sep 30 2019 at 13:42):

Indeed, the point is to prove the Axiom algorithms correct with respect to a specification.

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

view this post on Zulip Keeley Hoek (Oct 01 2019 at 03:11):

But the lean course will exist, Kevin! :D

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

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

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

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

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

view this post on Zulip Patrick Massot (Oct 05 2019 at 09:28):

@Kevin Buzzard you should leave a comment pointing to your Fermat blog post there.

view this post on Zulip Kevin Buzzard (Oct 05 2019 at 18:40):

rofl I just tried, and it was rejected as spam ;-)

view this post on Zulip Patrick Massot (Oct 05 2019 at 18:57):

Internet is so wonderful...

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

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

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

view this post on Zulip Mario Carneiro (Oct 06 2019 at 10:05):

He gives an argument, although I don't particularly buy it

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

view this post on Zulip Mario Carneiro (Oct 06 2019 at 10:07):

it's not all about the chinese room

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

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

view this post on Zulip Kevin Buzzard (Oct 24 2019 at 08:27):

http://chalkdustmagazine.com/features/can-computers-prove-theorems/

view this post on Zulip Luca Seemungal (Oct 24 2019 at 08:39):

"it's not hard to get Lean running on a computer" :joy::joy:

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

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

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

view this post on Zulip Johan Commelin (Oct 24 2019 at 11:58):

Lol, it's a nice easter egg, right?

view this post on Zulip Johan Commelin (Oct 24 2019 at 11:58):

I mean, it really fits in the theme

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

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

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

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

view this post on Zulip Johan Commelin (Oct 24 2019 at 12:19):

Too bad that Zulip doesn't have a "crazy trousers" emoji....

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

view this post on Zulip Johan Commelin (Oct 24 2019 at 12:35):

@Simon Hudon @Mario Carneiro who's the boss here? Can we make an exception :octopus: :tools: :zulip: :joy_cat:

view this post on Zulip Bryan Gin-ge Chen (Oct 24 2019 at 13:35):

@Kevin Buzzard @Mohammad Pedramfar The natural number game is looking great! Congrats!

view this post on Zulip Kevin Buzzard (Oct 24 2019 at 13:36):

Great! So now let's do the complex number game.

view this post on Zulip Kevin Buzzard (Oct 24 2019 at 13:36):

you import the reals, and then have to define everything.

view this post on Zulip Kevin Buzzard (Oct 24 2019 at 13:36):

unfortunately all of the proofs are "ext;ring" :-/

view this post on Zulip Kevin Buzzard (Oct 24 2019 at 13:37):

maybe I should think of a better game

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

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

view this post on Zulip Luca Seemungal (Oct 24 2019 at 13:46):

I suppose one could turn a whole undergrad degree into a game...

view this post on Zulip Johan Commelin (Oct 24 2019 at 14:01):

I think @Edward Ayers created a bunch of alternative Lean logos some time ago

view this post on Zulip Johan Commelin (Oct 24 2019 at 14:03):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Leaked.20Lean.204.20Logos

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

view this post on Zulip Kevin Buzzard (Oct 27 2019 at 08:45):

and now this (on Mario's metamath paper):
https://news.ycombinator.com/item?id=21358674

view this post on Zulip Mario Carneiro (Oct 27 2019 at 08:49):

I was on the front page for a while :D

view this post on Zulip Kevin Buzzard (Oct 27 2019 at 09:23):

I regard these things as small victories for the formal proof verification community

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

view this post on Zulip Chris Hughes (Nov 01 2019 at 20:10):

IMG_20191101_144932.jpg

view this post on Zulip Chris Hughes (Nov 01 2019 at 20:10):

Lean related graffiti in room 342

view this post on Zulip Miguel Raz Guzmán Macedo (Nov 02 2019 at 05:13):

Nice IMO grand challenge!

Is there a prize?

view this post on Zulip Bryan Gin-ge Chen (Nov 02 2019 at 05:16):

Sure, see: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/IMO.20Grand.20Challenge/near/175143187

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

view this post on Zulip Mario Carneiro (Nov 05 2019 at 09:27):

The formalization mentions obtain?

view this post on Zulip Mario Carneiro (Nov 05 2019 at 09:27):

but also #check

view this post on Zulip Mario Carneiro (Nov 05 2019 at 09:28):

The lean version that was used exists outside the linear flow of time

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

view this post on Zulip Kevin Buzzard (Nov 05 2019 at 09:52):

"we use Lean 3 to prove that Lean 4 works". Cunningly avoiding Goedel.

view this post on Zulip Mario Carneiro (Nov 05 2019 at 09:58):

wait, I don't think that's the direction that avoids Goedel

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

view this post on Zulip Kevin Buzzard (Nov 05 2019 at 12:15):

I'll take that as a vote for "one tactic instead of two please"

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

view this post on Zulip Johan Commelin (Nov 12 2019 at 17:23):

@Sebastien Gouezel Congratulations! :octopus: :cake:

view this post on Zulip Sebastien Gouezel (Nov 12 2019 at 17:34):

Thank you!

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

view this post on Zulip Mario Carneiro (Jan 03 2020 at 20:51):

first 40 minutes: why is the hello world example broken

view this post on Zulip Simon Cruanes (Jan 03 2020 at 20:59):

This person needs to hear about mm0, as a more modern foundation than metamath :p

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

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

view this post on Zulip Tim Daly (Jan 26 2020 at 15:31):

Oh SWEET! You've "cracked the code". I can build on that.

view this post on Zulip Bryan Gin-ge Chen (Jan 26 2020 at 16:30):

@James King made a thread about his guide here.

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

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

view this post on Zulip Kevin Buzzard (Jan 26 2020 at 18:37):

I did notice that yes :-)

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

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

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

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 11:34):

http://aarinc.org/Newsletters/130-2020-02.html#zulip

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

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

view this post on Zulip Simon Cruanes (Feb 13 2020 at 20:45):

Next IJCAR is in Paris, it's the right time to attend! :croissant: :baguette:

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

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

view this post on Zulip Johan Commelin (Feb 22 2020 at 21:15):

@Kevin Buzzard hits frontpage on HN again: https://news.ycombinator.com/item?id=22390486

view this post on Zulip Patrick Massot (Feb 22 2020 at 21:16):

Who did he provoked this time?

view this post on Zulip Johan Commelin (Feb 22 2020 at 21:18):

Just his blogpost from over a week ago (-;

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

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 21:15):

Job ad should be out by the end of the week :D

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

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

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

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

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

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2020 at 05:24):

See also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Wrote.20a.20blog.20post.20about.20Lean :slight_smile:

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 17:55):

Hitchhikers Guide Lean book now on front page of hacker news

view this post on Zulip Anne Baanen (Apr 07 2020 at 07:49):

Here is the comment section: https://news.ycombinator.com/item?id=22794533

view this post on Zulip Johan Commelin (Apr 07 2020 at 07:49):

They are saying silly things over there

view this post on Zulip Johan Commelin (Apr 07 2020 at 07:50):

Like you can't do epsilon delta proofs in Lean

view this post on Zulip Johan Commelin (Apr 07 2020 at 07:50):

Clearly didn't read TFA before commenting

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

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

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

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

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

view this post on Zulip Marc Huisinga (Apr 08 2020 at 16:00):

third entry for me

view this post on Zulip Alex J. Best (Apr 08 2020 at 16:00):

third for me after pearson and matlab

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

view this post on Zulip Alex J. Best (Apr 08 2020 at 16:02):

Its non-deterministic though, simply refreshing changes the order for me.

view this post on Zulip Marc Huisinga (Apr 16 2020 at 23:29):

"The Mechanization of Mathematics" by Jeremy Avigad

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

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

view this post on Zulip Johan Commelin (May 11 2020 at 08:33):

@Markus Himmel Congratulations! I'm looking forward to seeing the snake lemma in mathlib!

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

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

view this post on Zulip 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 baa,
  have : f a = b, by commutativity,
  commutativity
end

view this post on Zulip Johan Commelin (May 11 2020 at 08:54):

That is so cool!

view this post on Zulip Johan Commelin (May 11 2020 at 08:57):

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

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

view this post on Zulip Patrick Massot (May 11 2020 at 09:00):

How much of all this is in mathlib?

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

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

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

view this post on Zulip Patrick Massot (May 11 2020 at 09:14):

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

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

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

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

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

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

view this post on Zulip Scott Morrison (May 11 2020 at 16:08):

(although this wasn't actually completely blocking progress)

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

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

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

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

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

view this post on Zulip Jalex Stark (May 13 2020 at 00:59):

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

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

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

view this post on Zulip Jalex Stark (May 13 2020 at 01:28):

Is lean code not human readable?

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

view this post on Zulip Mario Carneiro (May 13 2020 at 01:38):

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

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

view this post on Zulip Mario Carneiro (May 13 2020 at 01:39):

but it's not for the untrained human probably

view this post on Zulip Jalex Stark (May 13 2020 at 01:44):

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

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (May 15 2020 at 19:17):

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

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

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

view this post on Zulip Kevin Buzzard (Jul 06 2020 at 19:34):

https://twitter.com/littmath/status/1280213422995648513?s=20

view this post on Zulip Bryan Gin-ge Chen (Jul 06 2020 at 19:47):

This reply made me laugh: https://twitter.com/fried_brice/status/1280224147168063488

More like 6 days, I think...

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

view this post on Zulip Andrew Ashworth (Jul 07 2020 at 04:29):

They are already present, in the semiconductor industry

view this post on Zulip Andrew Ashworth (Jul 07 2020 at 04:30):

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

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

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

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

view this post on Zulip Johan Commelin (Jul 07 2020 at 04:35):

Just wait till the end of summer :four_leaf_clover:

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

view this post on Zulip Kenny Lau (Jul 07 2020 at 04:53):

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

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

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

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 08:35):

Later he just changed the Constitution

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

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

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

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:17):

https://pbelmans.ncag.info/blog/2020/08/31/fortnightly-links-112/
This blog is read by a lot of algebraic geometers and number theorists.

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

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:32):

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

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

view this post on Zulip Gabriel Ebner (Aug 31 2020 at 18:33):

Is this really ∃ x y z, true?

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

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

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:34):

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

view this post on Zulip Gabriel Ebner (Aug 31 2020 at 18:34):

I find the source code equally hard to read.

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:34):

The bit with the carrier and opens is better.

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:34):

But I agree that i has a very ugly type.

view this post on Zulip Gabriel Ebner (Aug 31 2020 at 18:35):

The i is fine IMHO.

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:35):

In maths it is written as USpecRU \cong Spec R

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:36):

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

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

view this post on Zulip Johan Commelin (Aug 31 2020 at 18:37):

That's a de-Bruijn factor of about 80

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

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

view this post on Zulip Ian Riley (Aug 31 2020 at 18:43):

Thanks @Johan Commelin

view this post on Zulip Patrick Massot (Aug 31 2020 at 20:32):

Johan Commelin said:

https://pbelmans.ncag.info/blog/2020/08/31/fortnightly-links-112/
This blog is read by a lot of algebraic geometers and number theorists.

I knew we needed to update the overview page today.

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

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

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 13:24):

https://www.youtube.com/watch?v=gAuvVPw6_CQ

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 13:24):

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

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

view this post on Zulip Adam Topaz (Sep 17 2020 at 13:47):

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

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

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

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 13:49):

I want them to look more like Lean

view this post on Zulip Adam Topaz (Sep 17 2020 at 13:49):

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

view this post on Zulip Reid Barton (Sep 17 2020 at 13:51):

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

view this post on Zulip Adam Topaz (Sep 17 2020 at 13:51):

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

view this post on Zulip Reid Barton (Sep 17 2020 at 13:51):

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

view this post on Zulip Adam Topaz (Sep 17 2020 at 13:51):

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

view this post on Zulip Adam Topaz (Sep 17 2020 at 13:53):

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

view this post on Zulip Adam Topaz (Sep 17 2020 at 13:53):

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

view this post on Zulip 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 N\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 (N,Q\mathbb{N}, \mathbb{Q}, etc) strike an excellent balance: they are elegant and unintrusive.

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

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 14:13):

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

view this post on Zulip 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 Z\mathbf{Z} and Q\mathbf{Q} look better than Z\mathbb{Z} resp. Q\mathbb{Q}.

view this post on Zulip Adam Topaz (Sep 17 2020 at 14:14):

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

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

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 16:46):

https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/

view this post on Zulip Alexandre Rademaker (Sep 21 2020 at 20:09):

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

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

view this post on Zulip Alex J. Best (Sep 21 2020 at 21:26):

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

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

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

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:52):

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

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

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

view this post on Zulip Rob Lewis (Sep 28 2020 at 16:36):

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

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 17:29):

lol, he linked to docs#euclidean_geometry.dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two

view this post on Zulip Mario Carneiro (Sep 28 2020 at 17:29):

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

view this post on Zulip Kevin Buzzard (Sep 28 2020 at 17:31):

yeah but check out the shading

view this post on Zulip Kevin Buzzard (Sep 28 2020 at 17:31):

I think the joke goes the other way with add_pow

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 19:34):

I don't think we use square elsewhere

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

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

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

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

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

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

view this post on Zulip Rob Lewis (Sep 28 2020 at 19:42):

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

view this post on Zulip Patrick Massot (Sep 28 2020 at 19:42):

Yeah!

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 19:49):

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

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

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

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

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

view this post on Zulip Rob Lewis (Sep 28 2020 at 19:53):

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

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

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 19:56):

What ever happened to lean --doc?

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 19:57):

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

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

view this post on Zulip Rob Lewis (Sep 28 2020 at 19:58):

That's probably the easiest option here.

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

view this post on Zulip Rob Lewis (Sep 28 2020 at 19:58):

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

view this post on Zulip Patrick Massot (Sep 28 2020 at 19:59):

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

view this post on Zulip Patrick Massot (Sep 28 2020 at 19:59):

Presumably Gabriel knows.

view this post on Zulip Mario Carneiro (Sep 28 2020 at 19:59):

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

view this post on Zulip Rob Lewis (Sep 28 2020 at 20:01):

Aha

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

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

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

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

view this post on Zulip Patrick Massot (Sep 28 2020 at 21:15):

The latest one

view this post on Zulip Patrick Massot (Sep 28 2020 at 21:16):

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

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 21:28):

For the lazy: https://xenaproject.wordpress.com/2020/09/19/thoughts-on-the-pythagorean-theorem/

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

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 22:02):

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

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

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 22:24):

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

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

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

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

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

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

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

view this post on Zulip Yury G. Kudryashov (Sep 30 2020 at 00:40):

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

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

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 16:27):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 16:28):

image.png

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

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

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

view this post on Zulip Chris Wong (Oct 02 2020 at 00:52):

Perhaps they took "backwards reasoning" too literally?

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

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

view this post on Zulip Johan Commelin (Nov 12 2020 at 06:04):

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

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 13:18):

Wow, Andrej's answer is really good!

view this post on Zulip Sebastian Ullrich (Nov 20 2020 at 13:58):

I like the last one as well

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

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

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 14:20):

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 21:40):

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

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

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

view this post on Zulip Mario Carneiro (Nov 20 2020 at 21:53):

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 21:53):

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

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

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

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

I haven't forgotten about this... I'm just too busy atm :sad: (I hope it will be better in February :worried:)

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.

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

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

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

view this post on Zulip Mario Carneiro (Nov 23 2020 at 07:05):

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

view this post on Zulip Mario Carneiro (Nov 23 2020 at 07:06):

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

view this post on Zulip Mario Carneiro (Nov 23 2020 at 07:07):

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

view this post on Zulip Mario Carneiro (Nov 23 2020 at 07:08):

also comments but that's not so hard to fix

view this post on Zulip Johan Commelin (Nov 23 2020 at 07:08):

Aah, I just see that you answered this in the google groups thread:

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.

view this post on Zulip Johan Commelin (Nov 23 2020 at 07:08):

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

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

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

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

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 14:24):

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

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

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 14:51):

Thanks!

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

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 16:24):

That sentence does look a bit funny, yes

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 16:25):

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

view this post on Zulip Johan Commelin (Nov 28 2020 at 16:28):

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

view this post on Zulip Johan Commelin (Nov 28 2020 at 16:28):

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

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

view this post on Zulip Johan Commelin (Nov 28 2020 at 17:14):

ok, fair enough

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

view this post on Zulip Jasmin Blanchette (Nov 28 2020 at 21:06):

Coming soon to the Stedelijk Museum. ;)

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

view this post on Zulip Johan Commelin (Dec 24 2020 at 08:22):

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

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

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

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

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

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

view this post on Zulip Rob Lewis (Dec 24 2020 at 15:31):

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

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

view this post on Zulip Kevin Buzzard (Dec 24 2020 at 16:13):

Oh wow!

view this post on Zulip Kenny Lau (Dec 24 2020 at 16:14):

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

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

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

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

view this post on Zulip Johan Commelin (Dec 24 2020 at 18:35):

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

view this post on Zulip Eric Wieser (Dec 24 2020 at 18:40):

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

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

view this post on Zulip Jason Rute (Jan 05 2021 at 17:50):

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

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

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

view this post on Zulip Kevin Buzzard (Jan 09 2021 at 21:05):

Mark is my mathematical brother (we share an advisor), and he was hanging out on the zulip a year or two ago asking questions about this.

view this post on Zulip Carl Friedrich Bolz-Tereick (Jan 09 2021 at 21:06):

/me waves

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

view this post on Zulip Johan Commelin (Jan 27 2021 at 09:31):

/me logs in to upvote

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

view this post on Zulip Alexandre Rademaker (Mar 04 2021 at 03:42):

Can you share the link of the YouTube video??

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

view this post on Zulip Alex J. Best (Mar 05 2021 at 14:54):

Looks like its now up https://www.youtube.com/watch?v=EXpmbAfBNnw&ab_channel=HarvardCMSA @Alexandre Rademaker

view this post on Zulip Jason Rute (Mar 05 2021 at 23:36):

Also there are slides here.

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Joe Hendrix (Mar 14 2021 at 23:33):

Seems like a good reason.

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

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

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

view this post on Zulip Julian Berman (Mar 15 2021 at 00:07):

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

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

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

view this post on Zulip Julian Berman (Mar 15 2021 at 00:09):

(in that case fuzz testing obviously)

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

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

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

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

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

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

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

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

view this post on Zulip Peter Nelson (Mar 18 2021 at 15:23):

It'll be on youtube, yes.

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 18:54):

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

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

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

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

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

view this post on Zulip Julian Berman (Mar 22 2021 at 20:46):

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

view this post on Zulip Peter Nelson (Mar 22 2021 at 20:49):

Thanks! I'll post the youtube link when it's uploaded

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

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

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

view this post on Zulip Kevin Buzzard (May 05 2021 at 21:09):

Oh nice! I'm involved with that competition.

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

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

view this post on Zulip Chris Hughes (Jun 08 2021 at 13:40):

Dominic Cummings (former chief adviser to Boris Johnson) has tweeted about the Liquid Tensor Experiment https://twitter.com/Dominic2306/status/1402249206967025664?s=20

view this post on Zulip Patrick Massot (Jun 08 2021 at 14:00):

Is it like we have our Scott Morrison and the rest of the world have another one? Or is it the same Dominic Cummings?

view this post on Zulip Johan Commelin (Jun 08 2021 at 14:04):

Is this good or bad news :scream: :oops: :thinking:

view this post on Zulip Yaël Dillies (Jun 08 2021 at 14:05):

Maybe we can now pretend to the millions of pounds Kevin wanted for internships?

view this post on Zulip Patrick Stevens (Jun 08 2021 at 14:14):

Patrick Massot said:

Is it like we have our Scott Morrison and the rest of the world have another one? Or is it the same Dominic Cummings?

(If that question was serious, it's the same one)

view this post on Zulip Patrick Massot (Jun 08 2021 at 14:15):

It was not serious, Chris's message was very clear.

view this post on Zulip Eric Rodriguez (Jun 08 2021 at 14:21):

If only this gave some funding to us!

view this post on Zulip Kevin Buzzard (Jun 08 2021 at 15:29):

In fact Cummings was one of the people behind the £300,000,000 of mathematics funding (some of which is supposed to be for "out there" projects) which the UK has been given by government to cover up the gigantic holes left in science funding by Brexit. I am currently in the process of applying for some of this money...

view this post on Zulip Johan Commelin (Jun 18 2021 at 19:36):

For those not following the condensed stream: https://www.nature.com/articles/d41586-021-01627-2

view this post on Zulip Anatole Dedecker (Jun 18 2021 at 19:45):

Capture-décran-du-2021-06-18-21-44-04.png :sweat_smile:

view this post on Zulip Johan Commelin (Jun 18 2021 at 19:46):

Also, the "Cardinals" labels ended up pointing to a small island containing Zorns lemma

view this post on Zulip Marc Huisinga (Jun 18 2021 at 20:00):

Lean was originally created by a computer scientist at Microsoft Research in Redmond, Washington

is unfortunately unspecific. :(

view this post on Zulip Johan Commelin (Jun 18 2021 at 20:01):

Yes, I'm sorry about that. Both Kevin and me stressed a more specific version. :sad:

view this post on Zulip Patrick Massot (Jun 18 2021 at 21:09):

I guess this is a preliminary version that they wanted to publish online too fast. Hopefully there will be a printed version with Leo's name and a fixed image (to be 100% clear: the labels were completely rewritten by the journal).

view this post on Zulip Yaël Dillies (Jun 18 2021 at 21:12):

Commelin and Scholze decided to call their Lean project the Liquid Tensor Experiment, in an homage to progressive-rock band Liquid Tension Experiment

Wait, wasn't that a joke?

view this post on Zulip Yaël Dillies (Jun 18 2021 at 21:12):

Not many rock bands get their name into Nature!

view this post on Zulip Patrick Massot (Jun 18 2021 at 21:17):

Johan's version of the labels is at https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/Actual.20graph/near/242583715

view this post on Zulip Patrick Massot (Jun 18 2021 at 21:18):

The last nice touch is they sent me an email asking for permission to use my image, but they used it before I answer the email (and I took less than 12 hours to answer).

view this post on Zulip Johan Commelin (Jun 19 2021 at 04:32):

Yaël Dillies said:

Commelin and Scholze decided to call their Lean project the Liquid Tensor Experiment, in an homage to progressive-rock band Liquid Tension Experiment

Wait, wasn't that a joke?

It was a serious joke :crazy:

view this post on Zulip Marc Huisinga (Jun 19 2021 at 16:39):

hn frontpage: https://news.ycombinator.com/item?id=27559917
r/math: https://www.reddit.com/r/math/comments/o3caqq/mathematicians_welcome_computerassisted_proof_in/

view this post on Zulip Marc Huisinga (Jun 19 2021 at 16:44):

I sometimes wonder why the setoid hell github issue still comes up all the time on HN on just about every post related to Lean

view this post on Zulip Johan Commelin (Jun 19 2021 at 16:44):

It seems to mightily piss off the Coq community

view this post on Zulip Marc Huisinga (Jun 19 2021 at 16:52):

Yeah, and it's not a particularly great example of communication between the different theorem prover communities, so it would be neat if folks could just let it rest.

view this post on Zulip Eric Rodriguez (Jun 19 2021 at 17:30):

It comes up really easily whenever you google Lean, it was one of the first things I saw about it

view this post on Zulip Eric Rodriguez (Jun 19 2021 at 17:30):

So that's probably why

view this post on Zulip Marc Huisinga (Jun 19 2021 at 17:36):

Eric Rodriguez said:

It comes up really easily whenever you google Lean, it was one of the first things I saw about it

Hm, not for me. That said, the person who posted it this time on HN is also the same person that posted the issue back then on github.

view this post on Zulip Kevin Buzzard (Jun 19 2021 at 18:19):

Part of the problem is stupid things I said in 2019 when I had no idea about the CS aspects of things and could not explain properly why lean was a better fit for Scholze mathematics -- at the time it was simply obvious to me and I had no idea why because i never used Coq, I had just seen what they had achieved and felt that lean could easily do something completely different. I really tried to apologise for my actions in my INRIA talk last year. It is not my intent to create enemies of any kind. I am not horrible, I am just quite autistic and occasionally say or do stupid things without thinking about the consequences of my actions. I do not bear a grudge against anyone who said anything about me in the Coq community. I think that what is happening now in Lean now with the Scholze challenge speaks far louder than "man in stupid trousers says all maths is wrong" or "ignorant non-CS person says Lean is better than Coq". I am much better able to express myself now and my views are far more refined and educated.

view this post on Zulip Jasmin Blanchette (Jun 23 2021 at 20:30):

Slashdotted: https://science.slashdot.org/story/21/06/23/1922202/mathematicians-welcome-computer-assisted-proof-in-grand-unification-theory

view this post on Zulip Riccardo Brasca (Jun 25 2021 at 12:47):

https://www.raiplayradio.it/audio/2021/06/La-prova-del-software-c8c16121-e94c-49ca-bbdc-951e30162f5e.html

This is me speaking (in Italian) about the LTE in a pop science program at the radio. If you understand what I say I apologize for all the people that are not mentioned, and for all the slightly false things I said... I guess if we want to talk to the general public we have to make some compromise.

view this post on Zulip Riccardo Brasca (Jun 25 2021 at 12:47):

But don't miss the Liquid Tension Experiment music at the beginning!

view this post on Zulip Patrick Massot (Jun 25 2021 at 12:53):

Did we get any reaction at all from the musicians of LTE?

view this post on Zulip Riccardo Brasca (Jun 25 2021 at 12:59):

I don't think so, but you should ask @Kevin Buzzard

view this post on Zulip Kevin Buzzard (Jun 25 2021 at 13:40):

I don't think so :-(

view this post on Zulip Kevin Buzzard (Jun 25 2021 at 13:45):

Oh wow -- they spoke to Silvia de Toffoli in your interview Riccardo! She has a PhD in knot theory under Sullivan and now works in the philosophy department at Princeton! She definitely knows what she's talking about when it comes to proof assistants :-) Her recent article "Groundwork for a Fallibilist Account of Mathematics" (available here) is a really well-thought-out description of what human mathematics actually is in practice.

view this post on Zulip Riccardo Brasca (Jun 25 2021 at 13:54):

I read the paper yesterday, it is really really nice!
I just realized that the only people mentioned in the interview are myself (well, just because I was speaking) and Peter. This is of course ridiculous, I am really sorry for that.

view this post on Zulip Yaël Dillies (Jun 25 2021 at 14:52):

Ahah! I'm not speaking Italian, but I can basically read everything because it's so close to French! I'm just stumbling on what in the world could a sviluppator be.

view this post on Zulip Julian Berman (Jun 25 2021 at 15:03):

wiktionary says "developer"

view this post on Zulip Horatiu Cheval (Jun 25 2021 at 15:20):

Yes, I noticed many times "s-" has the role of a negation prefix in Italian, like "de-" or "un-" in English. With that, it's pretty nice how it matches "developer" :)

view this post on Zulip Eric Rodriguez (Jun 25 2021 at 15:30):

I mean, what is a "veloper"?

view this post on Zulip Johan Commelin (Jun 25 2021 at 15:33):

"velo" means cycle in French, so my guess is "cyclist"

view this post on Zulip Horatiu Cheval (Jun 25 2021 at 15:42):

Maybe it has to do with something along the lines of "wrapping things" then, and the developer does the opposite. Better not derail this thread into etymological considerations though. Etymology is not formalized, I think :)

view this post on Zulip Riccardo Brasca (Jun 25 2021 at 15:44):

Yes, "sviluppatore = developer". I didn't try to explain the difference between a Lean developer and someone who contributes to mathlib

view this post on Zulip Yaël Dillies (Jun 25 2021 at 16:10):

Horatiu Cheval said:

Maybe it has to do with something along the lines of "wrapping things" then, and the developer does the opposite. Better not derail this thread into etymological considerations though. Etymology is not formalized, I think :)

I think you're very much on point! sviluppatore seems to come from Medieval French velopper, which gave envelopper and envelop.

view this post on Zulip Jason Rute (Jun 28 2021 at 11:32):

I'm not sure this is "in the wild", and but the coq zulip has a topic: First Theorem Prover War asking for why to choose Coq vs Lean vs Isabelle. The title looks like it is intended to start a ITP flame war, so beware...

view this post on Zulip Huỳnh Trần Khanh (Jun 28 2021 at 13:51):

bad example, I made that thread :joy: and that was more like an honest question than an attempt to start a flame war :joy:

view this post on Zulip Kevin Buzzard (Jun 28 2021 at 14:46):

It was clearly an attention-grabbing headline but this chat is usually a bit more formal and maybe the Coq one is too. Feel free to hurl stuff like that around on the Discord all you like :-)

view this post on Zulip Jason Rute (Jul 02 2021 at 21:18):

E535F051-CA90-49FB-AE66-36A68263207B.jpg

view this post on Zulip Jason Rute (Jul 02 2021 at 21:19):

9DCEC371-E26B-4872-ACFD-C4A45B3B9A4C.jpg

view this post on Zulip Marc Huisinga (Jul 08 2021 at 15:10):

The Lean 4 Theorem Prover and Programming Language

view this post on Zulip Eric Wieser (Jul 08 2021 at 17:23):

If only there were some way to display monospace text in the browser without resorting to images. I'm sure springer will innovate online publishing in that area soon, with all those subscription fees (/s).

(Obviously the criticism is aimed entirely at the publishers and not the authors)

view this post on Zulip Kevin Buzzard (Jul 08 2021 at 17:39):

I particularly liked this bit:

bug.png

Presumably the displayed image is not what is supposed to be displayed? I agree that the images are horrible and also agree that there's probably nothing the authors can do about this. I found the constant change of font size particularly jarring.

view this post on Zulip Kevin Buzzard (Jul 08 2021 at 17:44):

The pdf in the e-book is lovely though, and doesn't have that random inputlst29 thing either, so this is just Springer screwing up the paper :-(

view this post on Zulip Johan Commelin (Jul 12 2021 at 07:53):

For those of you who like German: https://ondemand-mp3.dradio.de/file/dradio/2021/07/09/mathematiker_peter_scholze_computer_sucht_denkfehler_dlf_20210709_1648_cac56406.mp3

view this post on Zulip Jasmin Blanchette (Jul 15 2021 at 14:30):

Earlier today Leo presented his Lean 4 system description, written with Sebastian Ullrich, at the CADE 2021 conference.

view this post on Zulip Jasmin Blanchette (Jul 15 2021 at 14:31):

Here's the paper. Oh I see it's above. :smile:

view this post on Zulip Jason Rute (Jul 16 2021 at 10:51):

I noticed yesterday that the Nature article "Mathematicians welcome computer-assisted proof in 'grand unification' theory." appears to be missing. I've tried the link above and the DOI link https://doi.org/10.1038/d41586-021-01627-2 . It says "Server Error", so hopefully it is just that. I've also tried to search on the Nature site. It doesn't show up in all searches (for example searching by the Author), but it show up when searching for the title. In that case, same server error. (And to be clear, other articles work fine on nature.). Google can still find the pdf of the original published version. Anyway, if someone knows the author (or a Nature editor), they might want to point this out.

view this post on Zulip Kevin Buzzard (Jul 16 2021 at 10:56):

I've just emailed the author of the article. Thanks for pointing this out!

view this post on Zulip Jason Rute (Jul 16 2021 at 10:58):

I also just decided to send an email to the address on the server error page. Can't hurt.

view this post on Zulip Jason Rute (Jul 16 2021 at 12:07):

It works now. I got a pretty quick response from that support email.

view this post on Zulip Kevin Buzzard (Jul 16 2021 at 20:29):

https://twitter.com/3blue1brown/status/1416106848751558658

view this post on Zulip Kevin Buzzard (Jul 28 2021 at 15:59):

https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/

view this post on Zulip Yaël Dillies (Jul 28 2021 at 16:09):

I like the import tree illustration! It's of course ridiculously small compared to the real thing, but it gets the gist of it.

view this post on Zulip Johan Commelin (Jul 28 2021 at 16:26):

My apologies that many people involved didn't get a mention :sad:
I've posted a comment below the article that lists people that were actively involved in the project. I hope it gets accepted by Quanta soon.

view this post on Zulip Riccardo Brasca (Jul 28 2021 at 16:37):

Wow, great article!

view this post on Zulip Johan Commelin (Jul 28 2021 at 17:09):

https://news.ycombinator.com/item?id=27984471 (no discussion yet)

view this post on Zulip Eric Rodriguez (Jul 28 2021 at 19:30):

/r/math: https://www.reddit.com/comments/otdclo

view this post on Zulip Patrick Massot (Jul 28 2021 at 21:21):

How did we went from "I spent much of 2019 obsessed with the proof of this theorem" (from Peter's first blog post) to "Scholze worked out himself during a consuming week in July 2019"?

view this post on Zulip Eric Rodriguez (Jul 28 2021 at 21:36):

Yeah, I was very curious about that too.

view this post on Zulip Adam Topaz (Jul 28 2021 at 21:37):

We could probably ask the author about all of these things... (at least someone with the same name has been on this zulip chat in the past)

view this post on Zulip Adam Topaz (Jul 28 2021 at 21:44):

By the way, do quanta articles ever actually have comments on them? I see the disqus box at the bottom, but I don't recall ever seeing any article there actually have any comments.

view this post on Zulip Eric Rodriguez (Jul 28 2021 at 21:45):

Their "puzzle" ones often do

view this post on Zulip Yaël Dillies (Jul 28 2021 at 21:47):

Ghuuuu, I just understood that Disqus = discuss. The joke took 2 years to go through my French-speaking mind.

view this post on Zulip Mac (Jul 29 2021 at 02:03):

@Yaël Dillies Well I am a native English-speaker and never realized that either until you mentioned it! :rolling_on_the_floor_laughing: I never thought to pronounce the 'qu' as 'cu'. (I always wanted to turn it into dis-quis.)

view this post on Zulip Peter Scholze (Jul 29 2021 at 16:48):

Patrick Massot said:

How did we went from "I spent much of 2019 obsessed with the proof of this theorem" (from Peter's first blog post) to "Scholze worked out himself during a consuming week in July 2019"?

I repeatedly told him that the proof-at-large was a) really joint with Dustin and b) really occupied us for a year. (Well, it was kind of done after that week, but writing it up only occured towards the end of the year, and certainly my mind wasn't at rest until it was written.) But it's also true that a part of the proof, and essentially the one you've now formalized (ie Lecture 9) is something where I've spent a week as described in the article. I think for this story he decided he'll just focus on the latter...

view this post on Zulip Peter Scholze (Jul 29 2021 at 16:50):

(So there was a lot of preparatory work (eg, everything in Lectures 6-8, but also the rough setup of Lecture 9) until I decided that this week, I'll push and get it done.)

view this post on Zulip Julian Berman (Aug 04 2021 at 08:59):

It appears Lean and Johan are mentioned on the Condensed mathematics wikipedia page now: https://en.wikipedia.org/wiki/Condensed_mathematics#History

view this post on Zulip Kevin Buzzard (Aug 04 2021 at 09:21):

Ages ago I added a "this theorem has been formalised in Lean" sentence to the Cap Set Wikipedia page -- I think that such statements are of interest to the community.

view this post on Zulip Filippo A. E. Nuccio (Aug 04 2021 at 11:24):

It is a great thing, although I believe it would be more accurate to state that in 6 months only a part of the whole Clausen-Scholze paper has been formalized.

view this post on Zulip Riccardo Brasca (Aug 04 2021 at 16:12):

https://siliconreckoner.substack.com/p/on-the-implications-of-scholzes-liquid?fbclid=IwAR2aPno11mrXweweivDUakzAkl8JOw-DM_VXjgo-I_wTlAOb2DgSJ7QXcyk

view this post on Zulip Patrick Massot (Aug 05 2021 at 14:32):

Harris's writings on this topic are becoming a recurring joke. His new imaginary opponents are people formalizing maths without having fun. He lives in a different world, completely disconnected from reality.

view this post on Zulip Patrick Massot (Aug 05 2021 at 14:53):

He seems to have a special talent here, it's difficult to be so far away from reality. I very distinctly remember thinking during LT2021 that I never attended a traditional math conference with so many talks mentioning fun and enjoyment. I can't wait for the blog post where QHarris will explain that formalizers need to sacrifice children to AI beings during their satanic masses.

view this post on Zulip Johan Commelin (Aug 05 2021 at 15:47):

Apparently comments can be posted here: https://mathematicswithoutapologies.wordpress.com/2021/08/04/new-entry-on-substack-newsletter-on-scholzes-liquid-tensor-experiment/

view this post on Zulip Johan Commelin (Aug 05 2021 at 15:47):

Not saying that we should do that. Just want to point out the possibility

view this post on Zulip Marc Huisinga (Aug 05 2021 at 16:36):

Patrick Massot said:

I very distinctly remember thinking during LT2021 that I never attended a traditional math conference with so many talks mentioning fun and enjoyment.

He does quote @Kevin Buzzard as someone who "gets it", so maybe he agrees that the folks working on formalization now are enjoying it, but worries that it will not stay that way? In any case, I agree that it's a weird litmus test. I don't think that "mechanized mathematicians" who work in the area for a living (or simply because they want to guarantee correctness) instead of enjoyment are more likely to ruin the fun for regular mathematicians, which is the only thing I can think of as to why he'd use this as the litmus test for a good colleague.

A lot of it seems to be directed at ATP, but the other criticism of ITP in that post that I can see is that formalization may result in mainstream mathematics that is easy to understand by computers and not easy to understand by humans, and that less rigid notions of proof may end up being rejected outright:

Would mathematicians who refuse to adapt — for example, because they find the rigidity of the system an obstacle to expressing their ideas — be forced to resort to samizdat, or even blogs, to get their work published?

I think one of the goals of ITP is to close this gap, so that less rigid notions of proof can still be used for formalization. Hence whether this concern is justified depends on whether ITP manages to close the gap and the success of ITP in mainstream mathematics.

view this post on Zulip Kevin Buzzard (Aug 05 2021 at 20:48):

Just to be clear, Michael and I are very old friends :-) We work in the same area of number theory

view this post on Zulip Peter Scholze (Aug 05 2021 at 22:20):

I'm seeing Michael again (in person, I believe) at an Oberwolfach conference this month. Looking forward to lots of fun conversations :wink:

view this post on Zulip Mac (Aug 06 2021 at 02:20):

Marc Huisinga said:

A lot of it seems to be directed at ATP, but the other criticism of ITP in that post that I can see is that formalization may result in mainstream mathematics that is easy to understand by computers and not easy to understand by humans

Since when was mainstream mathematics ever "easy to understand by humans" !? :rolling_on_the_floor_laughing:

At least for me, ass a computer scientist, I would find the computer formalization a marked improvement in mainstream mathematics approachability and readability, Admittedly, that still wouldn't help the vast majority of people who find computer science just as esoteric as math, but I am not sure it could possibly be any worse than the status quo.

(Please note, this is all said in a spirit of levity and is not meant to be a serious inflammatory critique of mathematics.)

view this post on Zulip Kevin Buzzard (Aug 06 2021 at 06:58):

From many mathematician's viewpoints, mathlib looks like a library where there are theorems stated and the statements are pretty easy to understand, and then there are the proofs which look incomprehensible. So it is nothing like a marked improvement in readability. Of course this can be fixed by learning the language but this is not something that one would expect the mathematician of 2021 to do in general -- they already learnt how to decipher the heiroglyphics in maths papers and they don't want to learn a completely new way of doing it.

view this post on Zulip Patrick Massot (Aug 06 2021 at 09:41):

Of course what Kevin describes is the current state of affairs, but this is a transitory phase. In the end rendered Lean proofs will be much easier to read than traditional proofs.

view this post on Zulip Oliver Nash (Aug 06 2021 at 10:52):

I admit I have spent much more time writing Lean proofs than reading them and much more time reading informal proofs that writing them. However one thing I already prefer about reading a Lean proof is that I know it's correct.

view this post on Zulip Oliver Nash (Aug 06 2021 at 10:53):

Every time I'm struggling to understand an informal proof, part of me is wondering "maybe it's just wrong, or maybe the gap is non-trivial, or maybe the gap is fine as long as you're an expert in pseudoholomorphic curves, or noncommutative geometry, or algebraic stacks, or harmonic analysis, or ...".

view this post on Zulip Eric Rodriguez (Aug 06 2021 at 11:08):

Yes, the fact that I can just use F12 to see the proof for something that's supposedly trivial is life-changing

view this post on Zulip Jason Rute (Aug 06 2021 at 13:06):

I admit that the trouble I find with his posts is that they are long, and fully of flowery prose and side remarks. I can’t for the life of me get the main point, much less the argument for that point. I think after my second reading is that he is saying this: What people in the computer proof world talk about (at least in the articles and statements he reads about this topic) is “progress” and the technological advancements that would come from formal proofs or computer generated proofs. In his mind however, the main point of pure mathematics (and life in general) is the enjoyable activity of the pursuit of knowledge. He admits that both Kevin Buzzard and John Harrison share this view, so he might be arguing more about either the way this is presented in articles or a fear that math will be less fun in the future when formalization has taken over. I certainly have heard this argument before (and much more succinctly!). I think it is a view that shouldn’t be taken lightly.

view this post on Zulip Jason Rute (Aug 06 2021 at 13:22):

However, I do think one needs to be careful not to conflate ITPs and ATPs too much. They are of a very different flavor and I think they will effect mathematics in different ways. Also, I think that one talks about mathematics being taken over by machines, no one talks about how this will be a gradual process. When Szegedy talks about a decade he isn’t probably talking about Sholze level research (or really any research involving building new branches and tools in mathematics). Also I don’t think Szegedy is talking about mathematicians loosing their jobs. But he is also talking about a real noticeable advancement in the field of ATP as it relates to research mathematics.

view this post on Zulip Filippo A. E. Nuccio (Aug 06 2021 at 13:39):

Beyond @Jason Rute 's troubles with Harris' prose and remarks (and pompous quotations), what disturbs be most is
1) That he speaks for "mathematicians", as in his bold sentence What pure mathematicians find valuable about what we do is precisely that it provides a kind of understanding whose value is not determined by the logic of the market.: as a mathematician myself, I can say that my position towards the "logic of the market" is different from Harris';
2) In general, the level of political economy he needs for the lens through which our work is looked at;
3) When he says "Far from heralding a step toward making digitization routine, then, Scholze's initiative clearly expressed an intention to reserve such a step for exceptional circumstances. And there are reasons to digitize with caution. As historian Stephanie Dick observed in her study of early efforts to digitize mathematics, In developing theorem-proving software, practitioners endowed mathematical objects with computational properties - they were translated into dynamic, algorithmic, discrete things.": I might be too naif myself, but I have never seen in Scholze's initiative any "clear intention to reserve such a step for exceptional circumstances". I thought that he wanted to be sure of his theorem with Clausen, and was probably also a bit curious of the efforts needed for such a task, but it comes to me as a surprise to read that in Scholze's mind digitization must be done with caution. I wonder whether Harris has directly asked Scholze about this (as an aside: I am not sure that the quotation from Dick advocates for this caution neither, but this is another point).

view this post on Zulip Patrick Massot (Aug 07 2021 at 10:11):

Jason, I understand that Harris fears that math would become less fun with proof assistants. But he simply has no evidence to support that claim, only his fantasies.

view this post on Zulip Jason Rute (Aug 07 2021 at 12:36):

I think his points are poorly argued, but it is not an unrealistic fear. Right now interactive formal proving is fun because it is new, it is ambitious, it is optional, and it is decoupled from discovering the proofs. But imagine a world where it becomes required for publication like LaTeX is. (Of course the technology is not even close at that point.) I could see some areas of math fitting naturally into this world. Whereas others could be much harder and painful (probability theory comes to mind). I’m just saying that when we think of outreach to mathematicians, I imagine some of them likely have this fear in the back of their mind, and we shouldn’t be too dismissive.

view this post on Zulip Jason Rute (Aug 07 2021 at 12:39):

As far as automated theorem proving, I’ve often heard the fear that it could take away the beauty of math. For example, here is a quote from some private correspondence I’ve had:

I agree that advances in machine learning give us a lot to think about. I sometimes worry that everything we love about mathematics -- the clever ways that the right conceptualizations extend our cognitive reach -- are just crutches that we humans have developed to cope with the fact that we can't fit everything in our heads at once, and that we'll eventually give up and leave it to the cloud and machine learning will do everything we need.

view this post on Zulip Mac (Aug 08 2021 at 07:26):

@Jason Rute Honestly, I, as a computer scientist share much the same concerns about machine learning. I find that as machine learning has improved, it seems popular to just toss it a problem and hope it magically figures out a solution without the user ever having to understand the solution themselves. In fields where this works, it tends to decrease interest in research to fully conceptualize or formalize the problem as the machine can just produce the desired results.

When it comes to ATPs, though, I would think this would be a bit less of a concern. One can at least inspect the generated proof to figure out the way the machine got from point A to point B. Most other applications of machine learning don't have that luxury.

view this post on Zulip Filippo A. E. Nuccio (Aug 09 2021 at 17:44):

Jason Rute said:

I think his points are poorly argued, but it is not an unrealistic fear. Right now interactive formal proving is fun because it is new, it is ambitious, it is optional, and it is decoupled from discovering the proofs. But imagine a world where it becomes required for publication like LaTeX is. (Of course the technology is not even close at this point.) I could see some areas of math fitting naturally into this world. Whereas others could be much harder and painful (probability theory comes to mind). I’m just saying that when we think of outreach to mathematicians, I imagine some of them likely have this fear in the back of their mind, and we shouldn’t be too dismissive.

I certainly don't want to be dismissive, but I often imagine a world where some kind of formalisation becomes necessary, and I actually find it very nice! Of course this should not happen suddenly, and each community must find it natural before requesting this as a standard. But in the long run I simply see it as a very good thing, precisely as LaTeX. But I wonder if I am too naif.

view this post on Zulip Adam Topaz (Aug 12 2021 at 13:44):

This starts in 3 hours, in case anyone is interested.
https://researchseminars.org/talk/ToposInstituteColloquium/33/

view this post on Zulip Johan Commelin (Aug 12 2021 at 13:57):

The talk got the following labels :rofl: Computer science algebraic topology category theory logic

view this post on Zulip Adam Topaz (Aug 12 2021 at 13:58):

Johan Commelin said:

algebraic topology

:thinking:

view this post on Zulip David Michael Roberts (Aug 12 2021 at 14:11):

Totally is algebraic topology.

view this post on Zulip Reid Barton (Aug 12 2021 at 17:22):

I just want to point out that the youtube stream currently has 37 viewers

view this post on Zulip Adam Topaz (Aug 12 2021 at 17:31):

too many people wanted to verify this... it's up to 45

view this post on Zulip Bolton Bailey (Aug 13 2021 at 00:13):

Recording seems to be here https://www.youtube.com/watch?v=alByz_LoANE

view this post on Zulip Patrick Massot (Aug 13 2021 at 09:46):

Kevin, could you share your slides?

view this post on Zulip Kevin Buzzard (Aug 13 2021 at 11:08):

I made them in reveal-md so it's a little tricky.

view this post on Zulip Kevin Buzzard (Aug 13 2021 at 11:12):

slides.pdf

Will this do?

view this post on Zulip Yaël Dillies (Sep 08 2021 at 09:04):

Guess what I found in my science magazine... image.png

view this post on Zulip Yaël Dillies (Sep 08 2021 at 09:05):

For those who can't read French
Proof assistants get a hold on real maths
The judgement of those automatic (ahem) programs will be soon unbounded. A machine (understand the LTE people) validated for the first time a very high level demonstration (in analytical geometry), when up to now only repetitive or standard proofs were validated (hum... not really).

view this post on Zulip Riccardo Brasca (Sep 08 2021 at 09:09):

Which magazine is it?

view this post on Zulip Yaël Dillies (Sep 08 2021 at 09:10):

Epsiloon. It's been created 6 months ago from all the journalists who left Science & Vie (the editor changed ~2 years ago and has dubious practices).

view this post on Zulip Yaël Dillies (Sep 08 2021 at 09:11):

This is in n°2 p. 13

view this post on Zulip Riccardo Brasca (Sep 08 2021 at 09:11):

Merci !

view this post on Zulip Johan Commelin (Sep 08 2021 at 10:21):

Hmmm, it's nice that they mention this, but it's a bit sad that they got half of the statements fronw.

view this post on Zulip Reid Barton (Sep 14 2021 at 13:52):

I googled for paracompact lattice and the top result was https://leanprover-community.github.io/mathlib_docs/topology/paracompact.html

view this post on Zulip Adam Topaz (Sep 14 2021 at 13:54):

That's the goal right?

view this post on Zulip Yaël Dillies (Sep 14 2021 at 13:55):

Taking over the Internet? Yes :octopus:

view this post on Zulip Riccardo Brasca (Sep 14 2021 at 13:59):

Are you sure it isn't Google that knows you like Lean? For me the Lean page is the fifth one, and doing it over TOR it's not even in the first page :unamused:

view this post on Zulip Reid Barton (Sep 14 2021 at 14:00):

oh, could be

view this post on Zulip Johan Commelin (Sep 14 2021 at 14:02):

big brother (-;

view this post on Zulip Reid Barton (Sep 14 2021 at 14:06):

I usually don't use google as my first choice search engine so I forgot about that

view this post on Zulip Johan Commelin (Sep 14 2021 at 14:10):

but it reads your emails, so it still knows what you like (-;

view this post on Zulip Kevin Buzzard (Sep 14 2021 at 15:50):

Typing mathlib into duckduckgo (which I think is not remembering what I've clicked on in the past) it was the case for many months that the top link was to mathlib github, but as of a week so ago it's been sending me to the API documentation, which I thought was cool

view this post on Zulip Anne Baanen (Sep 22 2021 at 19:20):

The amazing news about the Hoskinson Center has spread to Reddit

view this post on Zulip Jeremy Avigad (Sep 30 2021 at 13:38):

Here's an interesting blockchain verification project that uses Lean: https://twitter.com/CairoLang/status/1443522554551996427?s=20. (No relation to Hoskinson and the center, just a fun side project for me.)

view this post on Zulip Jeremy Avigad (Oct 08 2021 at 17:40):

Has anyone seen this? https://codegolf.meta.stackexchange.com/questions/23916/language-of-the-month-for-october-2021-lean

view this post on Zulip Johan Commelin (Oct 08 2021 at 17:47):

@Jeremy Avigad see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Code.20Golf.20LOTM

view this post on Zulip Jeremy Avigad (Oct 26 2021 at 01:45):

On Wednesday, I'll be part of an informal discussion/presentation of formalization to an audience of blockchain developers that are new to the topic: https://www.crowdcast.io/e/in-mathematics-we-trust/register. I don't really know what to expect, but everyone is welcome to attend.

view this post on Zulip Patrick Massot (Oct 26 2021 at 13:13):

Also tomorrow, I'll give a talk about Lean at https://cmsa.fas.harvard.edu/tech-in-math/. It seems you need to ask for secret Zoom information (that I don't have...) if you want to attend.

view this post on Zulip Johan Commelin (Oct 26 2021 at 13:30):

Do you know where to ask?

view this post on Zulip Jason Rute (Oct 26 2021 at 13:31):

Just email Michael Douglas, listed at the top of that website.

view this post on Zulip Patrick Massot (Oct 26 2021 at 13:44):

If you want to actually attend the talk and get an answer then you should forward it to me.

view this post on Zulip Michael R Douglas (Oct 26 2021 at 13:47):

The zoom link is
https://harvard.zoom.us/j/99651364593?pwd=Q1R0RTMrZ2NZQjg1U1ZOaUYzSE02QT09
There is a password "cmsa" but you shouldn't need it if you type the link exactly.

view this post on Zulip Michael R Douglas (Oct 26 2021 at 13:49):

2 PM Eastern Time

view this post on Zulip Johan Commelin (Oct 26 2021 at 13:49):

Which is if I didn't make a timezone-calculation-error. (Edit: I did. Should be fine now.)

view this post on Zulip Rob Lewis (Oct 26 2021 at 13:51):

I think you did --

view this post on Zulip Johan Commelin (Oct 26 2021 at 13:51):

Aah, did you have a DST change already?

view this post on Zulip Rob Lewis (Oct 26 2021 at 13:51):

Are we in that annoying window where we're still on DST and you're not?

view this post on Zulip Riccardo Brasca (Oct 26 2021 at 13:52):

I think Rob is correct

view this post on Zulip Riccardo Brasca (Oct 26 2021 at 13:52):

A friend of mine in Montreal says it's almost 10am there

view this post on Zulip Johan Commelin (Oct 26 2021 at 13:52):

Ooh, it seems we're still both on DST but I just can't count.

view this post on Zulip Johan Commelin (Oct 26 2021 at 13:53):

There's a reason why I use Lean :rofl:

view this post on Zulip Scott Morrison (Oct 26 2021 at 23:28):

And Jeremy's talk is at .

view this post on Zulip Hunter Monroe (Dec 24 2021 at 21:12):

Lean made Quanta’s list of top mathematical developments in 2021 https://www.quantamagazine.org/the-year-in-math-and-computer-science-20211223/

view this post on Zulip Kevin Buzzard (Dec 24 2021 at 21:14):

Yeah, as did Ana Caraiani, who's four doors down from me at Imperial :-)

view this post on Zulip Johan Commelin (Dec 25 2021 at 04:56):

Does that mean that Lean made it two years in a row?

view this post on Zulip Hunter Monroe (Dec 25 2021 at 14:33):

Yes the second year in a row https://www.quantamagazine.org/the-year-in-math-and-computer-science-20201223/

view this post on Zulip Junyan Xu (Dec 26 2021 at 04:38):

DeepMind not mentioned??

view this post on Zulip Kalle Kytölä (Dec 27 2021 at 12:45):

I can't help but mention that one of the highlighted Quanta articles of 2021 featured both my PhD supervisor (Antti Kupiainen) and my former PhD student (Eveliina Peltola) :big_smile:. On the topic of counting doors, Eveliina is also nowadays CC doors from me on the same corridor at Aalto, where CC is a small positive constant, which is perhaps just a bit worse than Kevin's constant 44. :grinning_face_with_smiling_eyes:.

Ok, that was not Lean-related... But the mathematical topic of that Quanta article was probabilistic / constructive quantum field theory, and my longer term hope/goal is that mathlib's probability theory will catch up with at least some such uses in mathematical physics!

view this post on Zulip Yaël Dillies (Jan 12 2022 at 11:04):

Zulip describes Lean as an ATP, should we correct them? https://chat.zulip.com/case-studies/lean/

view this post on Zulip Arthur Paulino (Jan 12 2022 at 14:35):

IDK about their reach, but might be worth it just to avoid spreading misinformation

view this post on Zulip Reid Barton (Jan 12 2022 at 15:02):

I can contact whoever wrote this, what do we want it to say? "automated proof system" -> "interactive theorem prover"?

view this post on Zulip Bhavik Mehta (Jan 12 2022 at 16:09):

It already says "Lean is an interactive theorem-prover" later in the article; so that should be acceptable!

view this post on Zulip Reid Barton (Jan 20 2022 at 14:17):

https://github.com/zulip/zulip/pull/20848, I guess it will go live eventually

view this post on Zulip Alex J. Best (Jan 25 2022 at 22:05):

I'm honestly not sure what is happening but Wolfram seems to be streaming constructing some sort of Lean / Metamath import graphs on twitch https://www.twitch.tv/stephen_wolfram ?

view this post on Zulip Yaël Dillies (Jan 25 2022 at 22:07):

Sorry, you posted to the wrong topic.

view this post on Zulip Yaël Dillies (Jan 25 2022 at 22:08):

It's not Lean in the wild, it's wild Lean.

view this post on Zulip Arthur Paulino (Jan 25 2022 at 22:49):

This looks like a fun answer to "why formalize mathematics"

view this post on Zulip Yaël Dillies (Jan 25 2022 at 22:53):

"so that Stephen Wolfram can make funny diagrams"? :rofl:

view this post on Zulip Arthur Paulino (Jan 25 2022 at 22:57):

more like "being able to visualize how mathematics comes together"

view this post on Zulip Arthur Paulino (Jan 25 2022 at 22:59):

We rarely have the chance to see something like this when we're so focused on figuring out particular vertices

view this post on Zulip Junyan Xu (Jan 26 2022 at 02:37):

It seems the latest video is all about Metamath and I can't find where Lean is mentioned. BTW @Mario Carneiro was featured in this episode about Metamath.

view this post on Zulip Alex J. Best (Jan 26 2022 at 13:45):

Indeed it seems they mostly looked at metamath, I only saw this part way through so wasn't sure what was going on, one of his open windows (on the left 40 mins in https://www.twitch.tv/videos/1275782376) is definitely experiments with the lean decl graph, but maybe that was from a different day or something

view this post on Zulip Mauricio Collares (Jan 26 2022 at 14:47):

Probably related to https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/ (Ctrl-F "mathlib")

view this post on Zulip Eric Rodriguez (Jan 26 2022 at 14:59):

Interesting that set.mm has more theorems yet far less definitions

view this post on Zulip Yakov Pechersky (Jan 27 2022 at 05:15):

https://arxiv.org/abs/2201.08364

view this post on Zulip Yakov Pechersky (Jan 27 2022 at 05:16):

Not sure if this has been shared, maybe in the Lean for teaching stream. Happy to discuss it in a sibling thread. Edit: upon reading it, I think it's worth discussing only until section 4, inclusive. I think the later sections are not of substance that deal with mathlib-related issues.

view this post on Zulip Arthur Paulino (Jan 27 2022 at 19:31):

Has anyone seen this article?
The Central Dogma of Mathematical Formalism

view this post on Zulip David Wärn (Jan 27 2022 at 19:59):

I wish I hadn't

view this post on Zulip Chris B (Jan 27 2022 at 20:07):

I read this twice when Kevin retweeted it; I had a hard time discerning the author's point and it took me a second go to realize it wasn't my fault. They seem to be upset that proponents of formalism are promoting something as "proof" that lacks the elements of his definition of "proof" (as elucidated in the quote about Wiles). I haven't met anyone who thinks these concepts of proof are really in direct competition for anything, so I'm not sure what they're upset about.

view this post on Zulip Bolton Bailey (Jan 27 2022 at 20:09):

I found the anecdote about Theorem 2.5.6 funny.

view this post on Zulip Arthur Paulino (Jan 27 2022 at 20:15):

I had a hard time discerning the author's point

I second that. My best guess is that the author is upset about how formalization turns mathematics into a mechanical thing

view this post on Zulip Sebastian Ullrich (Jan 27 2022 at 20:20):

There's a POPL panel on proof assistants with Kevin and others going on right now btw https://www.youtube.com/watch?v=Oqc2_TEyeaU

view this post on Zulip Henrik Böving (Jan 27 2022 at 21:23):

Sebastian Ullrich said:

There's a POPL panel on proof assistants with Kevin and others going on right now btw https://www.youtube.com/watch?v=Oqc2_TEyeaU

They did mention proof by reflection on the topic of proof automation, I've never heard that before I think, do we have stuff like that in Lean I can take a look at? Or some non-Lean ressources people would recommend?

view this post on Zulip Anne Baanen (Jan 27 2022 at 21:32):

There is a tactic#ring2 that works by reflection. Also the Coq library MathComp is extensively based on reflection.

view this post on Zulip Eric Rodriguez (Jan 27 2022 at 21:34):

Henrik Böving said:

Sebastian Ullrich said:

There's a POPL panel on proof assistants with Kevin and others going on right now btw https://www.youtube.com/watch?v=Oqc2_TEyeaU

They did mention proof by reflection on the topic of proof automation, I've never heard that before I think, do we have stuff like that in Lean I can take a look at? Or some non-Lean ressources people would recommend?

https://alectryon-paper.github.io/bench/books/proof-by-reflection.html is a nice read; I was hoping to do this in Lean someday but I never got to it

view this post on Zulip Anne Baanen (Jan 27 2022 at 21:35):

In Lean 3, you don't really want to use reflection because it moves computation from the relatively fast vm to the slower kernel. I understand Lean 4 has special support for fast proofs by reflection, and Coq definitely supports it well.

view this post on Zulip Henrik Böving (Jan 27 2022 at 21:37):

Oh? I mainly work with Lean 4 so I'd definitely be interested in that, do you have some source for that claim I could dig further into?

view this post on Zulip Anne Baanen (Jan 27 2022 at 21:40):

I don't know if it's written somewhere else, but the main feature in Lean 4 is the reduceBool operator: https://github.com/leanprover/lean4/blob/master/src/Init/Core.lean#L1035

view this post on Zulip Mario Carneiro (Jan 27 2022 at 21:43):

Note that reduceBool goes a bit further than proof by reflection in the lean 3 sense. It is more like "trusting #eval", it is an extra axiom and it goes outside the regular type theory (external verifiers can't follow it)

view this post on Zulip Mario Carneiro (Jan 27 2022 at 21:45):

A smaller step toward faster kernel computation in lean 4 (which does not require new axioms) is that bignums are now part of the kernel spec: the nat.add and nat.mul functions work directly on nat literals represented as bignums in the kernel so they are orders of magnitude faster than lean 3.

view this post on Zulip Bryan Gin-ge Chen (Jan 27 2022 at 21:54):

Given the caveats stated there, have we discussed whether we'll be allowing reduceBool in mathlib after the port?

view this post on Zulip Mario Carneiro (Jan 27 2022 at 21:55):

Here's another example just to make the point about what you have to trust:

@[implementedBy Bool.false]
def truish := true

theorem truthy : truish = true := rfl
theorem falsy : truish = false := by nativeDecide

theorem contradiction : False := Bool.noConfusion falsy

#print axioms contradiction
-- 'contradiction' depends on axioms: [Lean.ofReduceBool]

view this post on Zulip Mario Carneiro (Jan 27 2022 at 21:58):

I wonder whether there should be an attribute for "(un)trusted implementedBy", such that proofs by reduceBool are only allowed to use the trusted ones. (There are other reasons to use implementedBy where the concern is more about good codegen than proving, and so you probably want to default to untrusted.)

view this post on Zulip Patrick Massot (Jan 27 2022 at 21:58):

Arthur Paulino said:

Has anyone seen this article?
The Central Dogma of Mathematical Formalism

You don't need to read it, the author name is enough. The best you can do is to either ignore him or consider him as a running joke if you like that kind of jokes.

view this post on Zulip Alex J. Best (Jan 27 2022 at 23:21):

Eric Rodriguez said:

https://alectryon-paper.github.io/bench/books/proof-by-reflection.html is a nice read; I was hoping to do this in Lean someday but I never got to it

I tried to do some parts of this a little while ago, maybe not the cleanest implementation ever but I think I had a more or less working monoid tactic if you are interested https://github.com/leanprover-community/mathlib/blob/alexjbest/reflection_experiments2/src/tactic/myring.lean

view this post on Zulip Kevin Buzzard (Jan 27 2022 at 23:29):

I tweeted about Michael Harris's article because he's a good friend of mine and I think his point that in 20 years' time all our proofs won't compile any more is worth noting. Obviously we have very different views on other things but he's a very respected figure in my community -- he proved the local Langlands conjectures for GL(n) with my advisor, for example.

view this post on Zulip Eric Rodriguez (Jan 27 2022 at 23:53):

Alex J. Best said:

Eric Rodriguez said:

https://alectryon-paper.github.io/bench/books/proof-by-reflection.html is a nice read; I was hoping to do this in Lean someday but I never got to it

I tried to do some parts of this a little while ago, maybe not the cleanest implementation ever but I think I had a more or less working monoid tactic if you are interested https://github.com/leanprover-community/mathlib/blob/alexjbest/reflection_experiments2/src/tactic/myring.lean

this is really cool, thanks for sharing Alex!

view this post on Zulip Patrick Massot (Jan 28 2022 at 08:09):

Kevin Buzzard said:

I tweeted about Michael Harris's article because he's a good friend of mine and I think his point that in 20 years' time all our proofs won't compile any more is worth noting. Obviously we have very different views on other things but he's a very respected figure in my community -- he proved the local Langlands conjectures for GL(n) with my advisor, for example.

I don't think you're helping your old friend with such tweets. People should have the right to slowly decline in the shadow without other being invited to watch the show. It reminds me the last years of Atiyah when everybody knew he hadn't prove the big theorem he was claiming to have proven but people we still inviting him to talk about his "proof" in prestigious conferences simply because of his past achievements. I thought that was sad and shameful.

view this post on Zulip Peter Scholze (Jan 28 2022 at 08:46):

Patrick Massot said:

Kevin Buzzard said:

I tweeted about Michael Harris's article because he's a good friend of mine and I think his point that in 20 years' time all our proofs won't compile any more is worth noting. Obviously we have very different views on other things but he's a very respected figure in my community -- he proved the local Langlands conjectures for GL(n) with my advisor, for example.

I don't think you're helping your old friend with such tweets. People should have the right to slowly decline in the shadow without other being invited to watch the show. It reminds me the last years of Atiyah when everybody knew he hadn't prove the big theorem he was claiming to have proven but people we still inviting him to talk about his "proof" in prestigious conferences simply because of his past achievements. I thought that was sad and shameful.

Well, I don't think the situations are comparable. Michael is still alive and kicking in his mathematics. [And I believe he's always had a tendency for philosophical considerations that are at times difficult to follow.]

view this post on Zulip Anne Baanen (Jan 28 2022 at 10:40):

I would like at least to defend some of the ideas of the post. The central thesis I distilled is that this currently trendy branch of mathematical formalism, that a proof is a proof iff it can be transformed into a formal arrangement of symbols checked for syntactic correctness by an automated process, is merely an ideology that can/should/will be subverted by another. (I use ideology here in a more epistemological sense, as a set of beliefs that define which topics are considered useful to know, discuss or research.) Formalism certainly is not a universally accepted standpoint, even though it would be in the interest of the ITP community to agree with it unanimously.

What I really miss in the post is engaging with previous iterations of debates on mathematical formalism — getting rid of the details about computers and cryptocurrency I can imagine Brouwer writing such an essay against Hilbert. So what makes the current situation interesting? Are there differences in kind or degree to that of the early 20th century?

view this post on Zulip Anne Baanen (Jan 28 2022 at 10:43):

To be provocative: the Lean community's reaction to the post is a proof in itself of the thesis that formalism is an ideology :grinning:

view this post on Zulip Yaël Dillies (Jan 28 2022 at 10:55):

Maybe it's an ideology, but for me it's just so much fun!

view this post on Zulip Anne Baanen (Jan 28 2022 at 11:02):

Indeed, that's another aspect that is not really touched upon in the article: you can be a formalizer without being a formalist.

view this post on Zulip Arthur Paulino (Jan 28 2022 at 11:40):

Talking about provocativeness, the "iff" that the author talks about (from Avigad's speech) might be a bit hard on professional mathematicians who don't enjoy formalization and are not willing to formalize their results

view this post on Zulip Marc Huisinga (Jan 28 2022 at 11:52):

Anne Baanen said:

Indeed, that's another aspect that is not really touched upon in the article: you can be a formalizer without being a formalist.

This is exactly my issue with Harris' article and a previous one I had read as well. It feels like he's criticizing ITP by criticizing a strawman of the ITP community - there are certainly ITP folks with a hard formalist position, ones who think that formalized proofs should replace peer-reviewed formal proofs in natural language or ones who think that mathematics should be done by AI, but I don't think that these are positions held in general by the ITP community, or that they are even the main reasons why people are interested in ITP.
This may in part be due to the running theme of his blog, with ITP being just one of multiple areas that he's commenting on from the same perspective, thus limiting the scope.

I'd also be more sympathetic to the article if the points were made less rhetorically (i.e. they'd read less like an LSD trip :-)), and I didn't feel like I'm spending more time trying to understand the points in the article than the author spent time writing it.

view this post on Zulip Joe Hendrix (Jan 28 2022 at 17:34):

I personally found the article interesting. It may be a bit meandering and have some strawman arguments, but the author was careful to insist this was about his values. I've certainly heard FM researchers express disdain for results that haven't been formally specified and verified. It's usually younger researchers and not the majority, but a sometimes vocal subgroup.
I really like the field, but think it would be a tragedy if reviewers were to reject papers with interesting ideas that were not fully backed by formal proof. That would only serve to further limit what could be expressed and considered, and academic CS is often too narrow as is in my opinion.

view this post on Zulip Jeremy Avigad (Jan 28 2022 at 19:07):

I have to say, I was somewhat taken aback by being characterized as putting forth a "militant but unsubstantiated attempt to ventriloquize mathematics." It's far from straightforward to try to extract from the post a clear understanding of what Harris' concerns are, and the extent to which they are incompatible with the aims of the Lean and mathlib community. I will leave it to others to engage in that debate. But, for the record, I'd like to point out that the quotation is taken from the first section of this paper:
http://philsci-archive.pitt.edu/16725/1/reliability.pdf
I hope that readers of the post will at least have the courtesy of reading that before weighing in on whether the snippet is militant and unsubstantiated.

view this post on Zulip Jeremy Avigad (Jan 28 2022 at 19:14):

A clarification: by "that," I mean only the first section of the paper, which spells out the view that Harris (seems to be) attacking.

view this post on Zulip Patrick Massot (Jan 28 2022 at 19:21):

Jeremy, you shouldn't worry too much. Harris is really making a fool of himself. I haven't read that last blog post because there so many interesting things to do instead, but the previous iterations were even more a caricature of Harris than a caricature of us.

view this post on Zulip Patrick Massot (Jan 28 2022 at 19:21):

He knows very well that the ideas he is attacking do not exist.

view this post on Zulip Henrik Böving (Jan 28 2022 at 19:50):

If that was the case, why is he doing it then?

view this post on Zulip Kevin Buzzard (Feb 02 2022 at 18:38):

https://openai.com/blog/formal-math/

view this post on Zulip Reid Barton (Feb 02 2022 at 18:53):

Very cool.

view this post on Zulip Reid Barton (Feb 02 2022 at 18:53):

I'm curious how nlinarith can prove Schur's inequality because I thought the difference of the two sides was not a sum of squares of polynomials.

view this post on Zulip Reid Barton (Feb 02 2022 at 19:04):

Not directly Lean-related but feels appropriate to mention this blog post from today as well:
https://deepmind.com/blog/article/Competitive-programming-with-AlphaCode

view this post on Zulip Stanislas Polu (Feb 02 2022 at 19:32):

Reid Barton said:

I'm curious how nlinarith can prove Schur's inequality because I thought the difference of the two sides was not a sum of squares of polynomials.

@Reid Barton my best guess is that prompted with the sq_nonneg arguments it finds another way to get to the proof not necessarily stepping through anything Schur's like?

view this post on Zulip Yakov Pechersky (Feb 02 2022 at 19:52):

Maybe this is for the mathlib ML channel, but given that the model can now prove statements, perhaps it can be modified to invent new tactics. What I mean by that, is create sensible subgoals, and extrapolate what steps it would like to take. Then if there are sequences of tactic states it would like to take, and that occurs often, maybe that's a missing tactic in our conceptual vocabulary that would be good to have. Stan, have you done training/validation where you ablate lemmas or tactics available to the model?

view this post on Zulip Arthur Paulino (Feb 02 2022 at 19:56):

Not only tactics, but also some more granular key lemmas

view this post on Zulip Mac (Feb 03 2022 at 02:37):

After reading Harris's article, the thing that struck me was that he seems to be confusing/conflating proof verification vs proof construction and logical vs rhetorical argument. The former is evidence by his rigorous vs heuristic distinction (which is exactly the separation between proof verification and construction lie) and the latter is by his artifact vs social process distinction (which is exactly where the separation between logical and rhetorical argument lie).

view this post on Zulip Mac (Feb 03 2022 at 02:47):

It also slightly concerns me that Harris thinks mathematical proof is primarily a social process (i.e., rhetoric). While it is true that arguments for parts of mathematics are fundamentally rhetorical in nature (i.e., belief in the plausibility of first principles like the law of the excluded middle), the hope (as I see it) is that rest of mathematics follows objectively/logically from these principles and is not merely a matter of rhetorical consensus.

view this post on Zulip Kevin Buzzard (Feb 03 2022 at 08:24):

Rhetorical consensus has a big part to play in practice (bigger than what some in the CS world realise, I suspect). As a formalist I would argue that logical deduction should have something to do with it but thinking about it now I think that one could argue that when it comes to getting your paper published all you're asking is that the referees say it's fine, and if none of them read section 4 properly because it was technical and they were busy then maybe Harris has a point that rhetorical consensus is actually what's going on in practice

view this post on Zulip Vincent Beffara (Feb 03 2022 at 08:48):

The "social construct" part also means that what you write as a proof in a paper is not a proof, but a discourse intended to mean something along the lines of "let me convince you that somewhere in the cavern exists a proof of my result, if you wanted to recover it you would start from first principles and do this, that and the other thing, but of course this is not doable in practice" and so a large part is convincing other mathematicians rather than actually writing a proof.

What is changing now is that the "of course this is not doable in practice" is becoming less and less true :smile:

view this post on Zulip Johan Commelin (Feb 03 2022 at 11:51):

Kevin Buzzard said:

https://openai.com/blog/formal-math/

Now discussed on HN: https://news.ycombinator.com/item?id=30181636

view this post on Zulip Julian Berman (Feb 11 2022 at 01:19):

Also discussed now by Yannic Kilcher: https://www.youtube.com/watch?v=McpjrsHrEY4#t=11m30s

view this post on Zulip Kevin Buzzard (Feb 15 2022 at 16:41):

There's an undergraduate conference in a few weeks https://sites.google.com/view/imatmt2022/ in the UK; it's a yearly thing, it's online this year. They get a bunch of UG speakers and a couple of bigshots and have a two day event. Of the 25 or so talks (covering pure and applied mathematics), three undergraduates chose to speak about Lean. Furthermore, none of those undergraduates are from Imperial! We have Yael (Cambridge), and then Hernan Ibarra Mejia from Sheffield (presumably they talked to Neil Strickland) and then Paul Lezeau from Warwick who worked with Damiano. I find this very exciting because it means this stuff is catching on with the younger generation.

view this post on Zulip David Michael Roberts (Mar 05 2022 at 01:40):

Sebastian Ullrich said:

There's a POPL panel on proof assistants with Kevin and others going on right now btw https://www.youtube.com/watch?v=Oqc2_TEyeaU

It's unfortunate that video is now private. Is there a public archived version?

view this post on Zulip Chris B (Mar 05 2022 at 01:48):

@David Michael Roberts https://www.youtube.com/watch?v=O15dbvEDApg

view this post on Zulip Jason Rute (Mar 06 2022 at 00:50):

More stuff on the recent OpenAI work solving Olympiad like problems in Lean. This is a video by Yannic Kilcher covering the paper. (I haven’t watched it yet.) https://m.youtube.com/watch?v=lvYVuOmUVs8&feature=youtu.be

view this post on Zulip Jason Rute (Mar 06 2022 at 00:51):

@Jesse Michael Han @Stanislas Polu Do we have an interview with you and Yannic to look forward to? (Lately his videos have been paired with author interviews so that is why I ask.)

view this post on Zulip Jason Rute (Mar 06 2022 at 01:11):

I should have watched the first 5 minutes before saying anything. He says right at the beginning that tomorrow he will release another video interviewing @Stanislas Polu about the paper.

view this post on Zulip Junyan Xu (Mar 06 2022 at 17:38):

https://www.youtube.com/watch?v=kl3aBni87jg

view this post on Zulip Adam Topaz (Mar 19 2022 at 18:36):

The game is afoot...

https://twitter.com/EgbertRijke/status/1505168608615354369?s=20&t=3aXnrqzJz6f9egLwjzTxAQ

view this post on Zulip Ruben Van de Velde (Mar 19 2022 at 18:38):

Are we comparing lines of code? Because I have some golfing I can revert :)

view this post on Zulip Kevin Buzzard (Mar 19 2022 at 18:38):

I think that competition is healthy.

view this post on Zulip Adam Topaz (Mar 19 2022 at 19:03):

IMO The true competition is to define π1et(P1{0,1,})\pi_1^{\mathrm{et}}(\mathbb{P}^1 \smallsetminus \{0,1,\infty\}) and prove that it's the profinite completion of the free group on two generators, using the fewest lines of code.

view this post on Zulip Arthur Paulino (Mar 19 2022 at 19:22):

no linebreaks

view this post on Zulip Kevin Buzzard (Mar 19 2022 at 20:22):

Well at least we know where to start there -- define an etale morphism of schemes.

view this post on Zulip Adam Topaz (Mar 19 2022 at 20:34):

I mentioned that result because it's something that I think is only possible with a large unified library like mathlib. The argument goes through the Riemann existence theorem, so it involves not just algebraic geometry, but also complex manifolds and algebraic topology.

view this post on Zulip Kevin Buzzard (Mar 19 2022 at 20:39):

Well Jujian is working on GAGA ;-) I see what you mean though. It is really hard to imagine that this sort of thing can be done in any way other than the way we're approaching it.

view this post on Zulip Kevin Buzzard (Mar 24 2022 at 10:52):

Not really "in the wild" but Heather is talking in London Learning Lean today at , about Fourier series in mathlib. See https://researchseminars.org/talk/LondonLearningLean/7/ for Zoom details.

view this post on Zulip Riccardo Brasca (Mar 30 2022 at 20:11):

If I understand correctly this, Kevin's talk at the ICM will be at

view this post on Zulip Bryan Gin-ge Chen (Apr 21 2022 at 18:26):

Fredrik Johansson's blog post "Things I would like to see in a computer algebra system" recently hit the front page of Hacker News. I think we've had a few discussions here about computer algebra in Lean, and this might be of interest. (It also mentions Lean/mathlib).

view this post on Zulip Yaël Dillies (Apr 21 2022 at 18:31):

Large but lean

Well, Lean is pretty lean.

view this post on Zulip Johan Commelin (Apr 21 2022 at 18:38):

Here's the HN discussion: https://news.ycombinator.com/item?id=31101332

view this post on Zulip Henrik Böving (Apr 21 2022 at 18:51):

Yaël Dillies said:

Large but lean

Well, Lean is pretty lean.

:= by rfl

view this post on Zulip Jason Rute (May 25 2022 at 00:51):

I don't know if this is still counting as "in the wild", but there is another AI for theorem proving paper using Lean. This one is by Meta AI (along with @Gabriel Ebner and @Amaury Hayat). I made a topic to discuss it in #Machine Learning for Theorem Proving > Paper: HyperTree Proof Search for Neural Theorem Proving.

view this post on Zulip Leonardo de Moura (May 25 2022 at 16:34):

Thanks for sharing. It is awesome that @Gabriel Ebner is one of the co-authors.


Last updated: May 27 2022 at 01:03 UTC