Lean in the wild

Stream: general

[Johannes Hölzl]

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

[Andrew Ashworth]

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

[Johannes Hölzl]

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

"Our choice of Lean as the language for the formalisation of this paper has been a consequence of a failed attempt at embedding two-level type theory in the Agda proof assistant." Adventures in Formalisation https://arxiv.org/pdf/1811.11317.pdf p.124

- Scott Fleischman (@scottfleischman)

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

Anyway, congrats with the visibility!

[Kenny Lau]

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

[Bryan Gin-ge Chen]

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

[Rob Lewis]

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

[Mario Carneiro]

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

[Rob Lewis]

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

[Mario Carneiro]

actually I think you're right

[Kevin Buzzard]

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

[Scott Morrison]

A slightly unusual "Lean in the wild" story:

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

[Johannes Hölzl]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

yeah but look at the set theorists.

[Johan Commelin]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

you can, that's kind of the point

[Johannes Hölzl]

Most of analysis works in HOL.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

you just can't call it a dependent type

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

no dependent types here

[Mario Carneiro]

doesn't matter how fancy X and Y are

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johannes Hölzl]

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

[Kevin Buzzard]

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

[Scott Morrison]

Pretty cool, Kevin! I hope people read this.

[Scott Morrison]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

It is a decades-long crisis :sunglasses:

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

This sort of thing has come up before

[Kevin Buzzard]

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

[Simon Hudon]

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

[Kenny Lau]

hey I wrote that code :P maybe I should answer

[Johan Commelin]

You are taking a break from Lean (-;

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Simon Hudon]

... so the opposite of redirecting people here

[Kevin Buzzard]

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

[Kevin Buzzard]

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

Sweet, I’ve been replaced! https://twitter.com/johannes2007/status/1111213919895539712

- Jordan Ellenberg (@JSEllenberg)

[Kevin Buzzard]

Jordan tweeted to his 11.7K followers :D

[Johan Commelin]

Did he just misunderstand what happened?

[Kevin Buzzard]

I am pretty sure that he did not :-)

[Kevin Buzzard]

he's just being a wag

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

So that's also quite some stuff from other chapters

[Johan Commelin]

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

[Kevin Buzzard]

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

For more on Kevin Buzzard, Johan Commelin, and Patrick Massot's project to put the definition of perfectoid space into Lean, go here: https://leanprover-community.github.io/lean-perfectoid-spaces/ Thanks to @HigherGeometer for bringing this to my attention. Follow him (David Roberts) for news on advanced math!

- John Carlos Baez (@johncarlosbaez)

[Kevin Buzzard]

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

@johncarlosbaez Do you know what the closeness of different definitions represents here?

- Jade Master (@JadeMasterMath)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

not a single tweet. sounds about right

[Mario Carneiro]

lots of followers though, haha

[Kevin Buzzard]

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

[Scott Morrison]

I commented, including inviting people here ...

[Johannes Hölzl]

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

[Simon Hudon]

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

[Johannes Hölzl]

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

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

[Simon Hudon]

All papers have authors who are or have been at CMU

[Simon Hudon]

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

[Johannes Hölzl]

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

[Simon Hudon]

That answers my question

[Patrick Massot]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I once managed to get a problem onto the IMO!

[Kevin Buzzard]

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

[Patrick Massot]

We need you to get Lean to win the contest!

[Patrick Massot]

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

[Mario Carneiro]

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

[Kevin Buzzard]

that would be good

[Kevin Buzzard]

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

[Patrick Massot]

I need to suggest defining Lebesgue integral

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

but it's not hard to do

[Patrick Massot]

How can it be half an hour and overcomplicated?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

I think at this point it just needs typing in

[Patrick Massot]

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

[Mario Carneiro]

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

[Tim Daly]

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

[Rob Lewis]

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

[Tim Daly]

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

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

[Tim Daly]

Who controls this website?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Tim Daly]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Tim Daly]

In theory I've created a correct pull request.

[Kevin Buzzard]

I commented, including inviting people here ...

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

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

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

[Simon Hudon]

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

[Kevin Buzzard]

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

[Simon Hudon]

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

[matt rice]

def unimportant := true
def important := false
def not_unimportant : ¬ unimportant ↔ important
:= iff.intro
         (λ _ : ¬unimportant,
                        have  ¬true → false, from (λ h, h $ by trivial),
                        have unimportant = true, by refl,
                        have ¬true, from (eq.substr ‹unimportant = true› ) ‹¬ unimportant›,
                        show important, from ‹¬ true → false› ‹¬ true› )
         (λ _ : important, false.elim ‹important›)
#print axioms not_unimportant

i'm still not convinced nihilism is all that constructive though

[Tim Daly]

Leonardo de Moura at PLSE 2016: The Lean Theorem Prover https://www.youtube.com/watch?v=69ytTKfSSgc

[Kevin Buzzard]

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

[Kevin Kappelmann]

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

[Johan Commelin]

I don't know, but if it's in France it will probably be dubbed in French

[Kevin Buzzard]

https://www.youtube.com/watch?v=aZHbnQlFOn4 My general audience talk with a bunch of Lean in.

[Tim Daly]

re; Squares Tessellate Tait, "Truth and Proof: The Platonism of Mathematics" http://logic.harvard.edu/EFI_Tait_PlatonismInMathematics.pdf

[Kevin Buzzard]

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

https://itp19.cecs.pdx.edu/invited-speakers/

So now 6 Lean talks ;-)

[Reid Barton]

Do you know what you'll talk about, or will you decide at 3 AM the night before?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

the ideal lambda syntax is

- Sebastian Ullrich (@derKha)

[Scott Morrison]

I use \mapsto inside an expression.

[Simon Hudon]

I don't like the idea that there would be significant notational differences between for all and lambda. I think we shouldn't have a completely different syntax for each binder. If we pick ., we should use it for forall, exists, etc

[Jesse Michael Han]

One of Lean's syntactic idiosyncrasies is the use of a comma separator in lambdas and other binders.

one of my reviewers complained about this exact thing:

How is this tuple parsed?  For me it looks like a 5-uple!
  Apparently, Lean has some magic binding rules where the comma gets a
  different binding strength if it was preceded by a λ!? ...
  [What were the designers of Lean thinking here??]

in retrospect, it is indeed hilarious:

def check : (pSet : Type (u+1)) → bSet 𝔹
| ⟨α,A⟩ := ⟨α, λ a, check (A a), λ a, ⊤⟩

[Reid Barton]

Yeah, I also noticed how crazy/ambiguous-looking the , , , syntax is when trying to explain some Lean code to a non-Lean user

[Reid Barton]

But I don't have a Twitter account so I don't get a vote :not_allowed: :bird:

[Andrew Ashworth]

Yeah, I can't vote either. But the traditional separator is the period, so I'd vote for that. And it should also be used for all the other logical quantifiers, like Simon mentioned.

[Reid Barton]

if we're thinking outside the box syntaxwise, a lot of people wouldn't mind having the Greek letter λ available as a variable name

[Simon Hudon]

from the perspective, \mapsto doesn't use a letter so that frees up lambda but it does use an arrow which we always seem to run out of. Plus, my aforementioned point about homogeneity

[Reid Barton]

there are also some alternative Unicode lambdas (see under "Mathematical Lambda" at https://en.wikipedia.org/wiki/Lambda) but I don't know how well supported they are

[Simon Hudon]

We could keep the same lambda for functional abstractions and let people find other unicode lambdas for their local purposes

[Mario Carneiro]

I would actually prefer to use backslash than unicode lambda (but with lambda available as alternate notation). It would be nice if the core syntax didn't use so much unicode, since this makes it difficult for those that don't want to use a lean-approved editor

[Simon Hudon]

Does that issue arise often?

[Johan Commelin]

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

[Johan Commelin]

Is .\ a faithful ASCII rendition of lambda?

[Johan Commelin]

.\ x. e :scream_cat:

[Johan Commelin]

Btw, I would be a fan of having infix \mapsto available. It's used all over the place in maths, so it doesn't feel like "sacrificing" an arrow.

[Scott Morrison]

Yeah --- I'd be pretty upset seeing someone use \mapsto to mean anything else, so arguably it's already taken.

[Mario Carneiro]

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

[Keeley Hoek]

ATTACK OF ZE SEMICOLONS

[Keeley Hoek]

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

[Mario Carneiro]

Sigh. I wish there weren't so many meaningless syntax changes. I don't really care what the syntax is, but I like consistency and these changes should be considered in the light of all the people that will have to learn the new syntax. I hope there is at least a rationale posted for all these things at some point

[Tim Daly]

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

[Tim Daly]

For example, does [x/y]e mean substitute x for y in e or substitute y for x in e? Guy did a survey.

[Andrew Ashworth]

I would actually prefer to use backslash than unicode lambda (but with lambda available as alternate notation). It would be nice if the core syntax didn't use so much unicode, since this makes it difficult for those that don't want to use a lean-approved editor

there are non-unicode alternatives for lambda, though? Just like coq, I think you can type fun or assume for lambda, and so forth. The implication arrow is the very awesome ->. I mean, you probably know this, so I'm not quite following.

[Patrick Massot]

For example, does [x/y]e mean substitute x for y in e or substitute y for x in e? Guy did a survey.

This issue is what confused me every single time I read or watched explanations about lambda-calculus.

[Patrick Massot]

I'm very close to creating a Twitter account only for the purpose of voting here. @Sebastian Ullrich wouldn't it make more sense to have a GitHub vote? You could created and issue with one message per proposition, and we can use the emoji reactions to vote. I think the period option is really awful. I don't know any language (I mean real language, not programming language) where period is used for anything else than ending a sentence. In what sense does λ x. eends after x?!? Of course every mathematician would vote for x ↦ e but I'd be happy to keep λ x, e if it is important for CS people.

[Keeley Hoek]

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

[Keeley Hoek]

The java compiler can parse that

[Keeley Hoek]

(I mean an isomorphic expression)

[Sebastien Gouezel]

Period is used in Isabelle. It took me a lot of time to get used to the comma in Lean, and in the end I think I prefer the period because the comma is already used to separate expressions in anonymous constructors. My point is rather that I would like to have two different symbols here, be it . , or , ; say.

[Sebastian Ullrich]

@Patrick Massot The wording of the poll should imply that it isn't meant to be taken very seriously, nor will its outcome influence our decision

[Sebastian Ullrich]

@Sebastien Gouezel I'm not convinced we should unnecessarily include syntax variations (ASCII alternatives are quite useful, OTOH). In practice, whatever syntax TPIL uses will be used by 95% of all users. But you're welcome to override the builtin notation in Lean 4 if you want to.

[Patrick Massot]

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

[Andrew Ashworth]

we can make everybody unhappy and do λx ↦ e

[Simon Hudon]

@Andrew Ashworth That looks dicey. To be sure everyone is unhappy, let's put the lambda at the end

[Simon Hudon]

@Patrick Massot I'm not too wild about this possibility because : is also used for type annotations. λ v : e : e would be valid and possibly ambiguous. You could require brackets around v : e but I prefer those brackets to be optional

[Johannes Hölzl]

@Sebastian Ullrich I think Sebastien didn't mean two syntaxes at the same time, but to have a syntax where the tuple "comma" is different from the binder "dot".

[Johannes Hölzl]

While I would also prefer the " fun x. t" instead of "fun x, t" I think this would be another unnecessary syntax change.

[Sebastian Ullrich]

I think Sebastien didn't mean two syntaxes at the same time, but to have a syntax where the tuple "comma" is different from the binder "dot".

Ah, I see.

[Marc Huisinga]

would it really be that difficult to (possibly automatically) convert the old syntax to a new syntax in all important lean resources?
are there many existing lean resources that cannot be easily converted?

[Jeremy Avigad]

I like the period, but probably because it is common in the CS literature and I have gotten used to it. @Patrick Massot here in the US we write 3.1415... I guess you Europeans sometimes write 1.000.000 for one million.

[Jeremy Avigad]

It is possible to get used to anything.

[Tim Daly]

The problem is that this isn't fully "a free choice", since some of these will eventually be published in papers and books. Hopefully the syntax can be understood by non-lean readers.

[Patrick Massot]

No, we use 1 000 000.

[Rob Lewis]

This might not count as "in the wild" since it's from MSR, but: https://sf.snu.ac.kr/aliveinlean/ https://sf.snu.ac.kr/publications/aliveinlean.pdf

[Andrew Ashworth]

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

[Andrew Ashworth]

right now I'm researching how much work it would be to write a program that traverses Clang ASTs and feeds floating point expressions to Herbie, and then spit out the analysis. So maybe not directly related, but somewhat...

[Kevin Buzzard]

https://arxiv.org/abs/1907.07801

[Bryan Gin-ge Chen]

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

[Koundinya Vajjha]

In particular, we have implemented interaction with the lean theorem prover, whereby the export format of lean is used (via trepplein) to generate code in our implementation of HoTT. This allows us to start with a library for learning as well as a target for natural lannguage processing.

http://siddhartha-gadgil.github.io/ProvingGround/

[Neil Strickland]

I'd be interested in thoughts about the arrangement of code for this sort of thing. I think it's desirable to have a static snapshot on the arxiv and a maintained repository on github. Certainly some of the code on my github repository could move into mathlib. We could have a policy and/or aspiration that all code supporting a published paper should move into mathlib. Or we could have a separate repository for that purpose, but still under leanprover-community and set up with travis so we can maintain compatibility with mathlib.

[Andrew Ashworth]

It's a little ambitious to expect everybody to keep their code up to date. An arxiv submission should contain git hashes of any dependent packages. Probably also a specific Lean version number too, in order to ensure reproducibility, maybe using Elan? Then even if the paper is read years later the code should still work without squiggly lines.

[Andrew Ashworth]

It would be best if ArXiv would host everything needed to make a reproducible paper, but I can imagine the storage costs would be immense, especially for papers in physical science with large datasets... :/

[Floris van Doorn]

On The FOM (foundations of mathematics) mailing list there is a short thread about the NP = PSPACE problem. People are trying to formalize their claimed proof that NP = PSPACE in Lean:

In order to avoid incomplete versions, I and my students,
are formalizing our version in LEAN. Only after each relevant part is
formalized and checked there will be an article published it in arxiv

According to Wikipedia, this claim is "widely suspected" to be false.

[Kevin Buzzard]

I wrote a short piece about Lean for the London Mathematical Society newsletter, and it has just appeared: https://www.lms.ac.uk/sites/lms.ac.uk/files/files/NLMS_484_for-web_0.pdf (pages 32 to 36).

[Johan Commelin]

@Kevin Buzzard Gijswijt's name is missing on p33

[Kevin Buzzard]

Noo!

[Kevin Buzzard]

:-(

[Kevin Buzzard]

Well it's only missing once, it is there the second time, and it's also clearly a typo rather than me claiming that it's Ellenberg only because of the dangling "and".

[Kevin Buzzard]

Oh! Gijswijt's name is in the version I sent them! So they have removed it for some reason -- as well as making the Lean code on p32 look a bit horrible (this is some png rescaling issue perhaps).

[Johan Commelin]

Wow, that's some really good editing!

[Kevin Buzzard]

The London Mathematical Society runs on a shoestring.

[Johan Commelin]

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

[Kevin Buzzard]

I have no idea. I'll ask.

[Kevin Buzzard]

It will be fixed online when people are back from holidays

[Reid Barton]

If minor edits are still relevant: "It is just is a" near the end of the first page

[Kevin Buzzard]

Thanks. The person who's making the changes is away until Monday so I believe I might still be able to get this fixed.

[Olli]

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

[Kevin Buzzard]

?? How did they get from "I think there is a non-zero chance that some of our great castles are built on sand" to "Number Theorist Fears All Published Math Is Wrong" ?? @Rob Lewis this is the guy we were talking about at ITP.

[Kevin Buzzard]

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

[Olli]

Yep, I ran into it on Twitter posted by a non-mathematician, clearly it is clickbait and how they get their clicks and their ad revenue

[William Whistler]

“I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,” Buzzard told Motherboard while he was attending the 10th Interactive Theorem Proving conference in Portland, Oregon, where he gave the opening talk.

[William Whistler]

Is that a made-up quote?

[Kevin Buzzard]

How can I check? :-/ I was in a hotel room in Portland talking to him on the phone. It's not very good English, that's for sure.

[William Whistler]

Hard at this point, if you don't remember or have a record. They might've rolled their question and your response into the quote, or something like that.

[Kevin Buzzard]

Well, we live and learn :-/

[Rob Lewis]

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

[Kevin Buzzard]

:-)

[William Whistler]

Even "arguing that we must begin to rely on AI to verify proofs" is quite clickbaity. Not all software is AI, for heaven's sake.

[Simon Hudon]

But to be fair, Kevin does put a lot of software in the same basket, going so far as to ask "Why isn't Lean smart enough to figure it out?" inviting the classification of interactive provers as AI technology

[Jeremy Avigad]

I had the foresight to ask him to check back with me over any quotes he wanted to use. So at least I sound sane (if not nearly as exciting).

[Johan Commelin]

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

[Johan Commelin]

I'm not so much concerned about the general public, or clickbaity titles. More about the mathematical community that doesn't speak with you on a daily basis.

[Kevin Buzzard]

I'm a bit snowed under at the minute, teaching starts next week, but I'll see what I can do

[Kevin Buzzard]

I'm not so much concerned about the general public, or clickbaity titles. More about the mathematical community that doesn't speak with you on a daily basis.

I think you're probably more concerned than I am :-) I think that when I was younger I would have been running around panicking, but now I understand the internet much better and it seems to me that most Lean stuff on the internet is sane, and then this one piece is a bit more extreme but it will just disappear into the general noise. I think much more interesting is Frank Calegari's claim that some humans completely understand the proof of Fermat's Last Theorem, so I wrote a blog post about that instead. What do you think @Johan Commelin ? I can't quite work out if you're being serious. I mention the Vice article a bit at the beginning.

https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/

[Johan Commelin]

@Kevin Buzzard I think the first paragraph of your blogpost settles it in a nice and relaxed way (-;

[Johan Commelin]

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

[Patrick Massot]

I just ran into François Charles in the corridor and stopped me to tell me: "I saw in newspapers that your collaborator says every maths is wrong". He was smiling though.

[Kevin Buzzard]

What can you do :-) Given that you yourself found omissions in Bourbaki, maybe all maths _is_ wrong :-)

[Patrick Massot]

Of course François heard about this on Twitter. Did you put links to your blog post there?

[Kevin Buzzard]

Yes.

[Joe Hendrix]

I think reporters generally run with quotes they think they need to drive views. Being very measured in responses just means no news.

[Chris Hughes]

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

[Kevin Buzzard]

Good to see it mentions Lean!

[matt rice]

I guess my interest in proof checking stems from a very different thing, where we have a general proof that something is (unprovable? -- i dont want to say false), but in special cases can be proven true, the general cases tend to throw shade on the special case, and the special case tends to require a lot of setup... It's probably best if I just give an example...

like the idea that nand has no inverse and loses information, but in the case where nand is the partial application of a reversible universal logic gate like a fredkin gate, or a toffoli gate the complete gate has an inverse. I like proof checkers for their ability to convey all these special assumptions, when trying to convey a counterintuitive truth ... This is somewhat the dual of Kevin's what if its false when we think it true I guess.

[Jesse Michael Han]

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

[Kevin Buzzard]

Amazing what a clickbait headline can do!

[Kevin Buzzard]

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

[Kevin Buzzard]

What I am manifestly relieved about is that most people actually seem to be completely avoiding saying "this guy is clearly an idiot, clearly all published maths is not wrong". It's like today's kids are somehow immune to the clickbait, or forget it instantly or something.

[Kevin Buzzard]

Oh! Because of hacker news rules, apparently they changed the headline from the clickbaity one to "Number theorist fears many proofs widely considered to be true are wrong ". That's closer to the truth, but perhaps "some proofs" would be better.

[Kevin Buzzard]

The whole thing is great. People are talking about Lean, people are talking about theorem provers, this is just what we need to get young people interested in the area.

[Johan Commelin]

This comment from Hacker News is quite a marvel:

IMO the final paper had too much technical jargon which was convoluting some simple concepts.

This is symptomatic of IMHO the biggest single problem with the world of mathematics today. This discipline should be about developing ideas based on rigorous foundations and logic, which is a useful and important purpose. Once you have understood those ideas, even "advanced" results often seem quite simple and intuitive, and we can take that understanding and apply it to other work if helps us to make useful progress. However, the amount of needlessly obscure terminology, poor notation and just plain bad writing in formal papers make the whole field absurdly inaccessible, even to many who might have no trouble understanding the underlying concepts and important results.

Just imagine what would happen if we tried to write engineering specs or software the way postgraduate mathematics research is done. We'd be trying to debug source code where every identifier was a single character, taken from one of three or four different alphabets, with several of them looking similar enough to mistake one for another, with a bunch of combining accent modifiers on top that were used to fundamentally change the semantics of the program, interspersed with comments by someone who needs a remedial class in basic writing skills, full of technical terminology that is defined in terms of other technical terminology from other software packages, except that sometimes the meaning is subtly different in this context but that isn't noted anywhere on the screen at the time, resulting in needing to spend half an hour doing a depth-first-search of all the definitions only to find that a function whose only identifier is the name of the developer who wrote the second version (because the first person to work on it already has another function bearing their name) is actually equivalent to what a programmer would write as

const DAYS_IN_WEEK := 7

I write this as someone who studied mathematics to a high level and has touched on the field many times since in connection with heavily mathematical software development. It's the worst sort of closed-world gate-keeping, and we could do so much better, but sadly inertia and vested interests are not our friends in this matter.

https://news.ycombinator.com/item?id=21109440

[Tim Daly]

Mathematica won in the computer algebra field for a simple reason. It had the best documentation. The learning curve for any computer algebra system is quite steep and all of the other systems relied on "learn by trial".

Now look at Lean. Take, for example, group.lean. It is a wall of text. Finding a theorem relies on odd names like mul_eq_of_eq_inv_mul. The whole of the "communication" with people, such as it is, is contained in that name. Programmers made the mistake of this "pile of sane" (POS) approach, witness the "src", "inc", "tst", and (usually empty) "doc" directories with "semantic naming" like parser.c, SMTFuns.pl, or catsim.ml.

Suppose, instead, there was a group theory textbook in latex. The textbook explains the ideas in natural language. It contains all of the lemmas in group.lean, each one with a paragraph or so of explanation. The lemmas are in named "chunks", basically a verbatim block with a name. Lemmas should only be accepted when they contain a paragraph or section in the group theory volume.

Now you have a book, with a table of contents, a table of equations, chapters, sections, paragraphs, an index, and a bibliography, all hyperlinked and searchable. Since each lemma is in a named verbatim chunk you can extract any or all lemmas automatically, letting the compiler do it. You can find relevant lemmas by looking in the table of contents or the index.

Code to extract a named chunk is 170 lines of C. Axiom already uses this technology.

The idea is called "literate programming" (Knuth). You write for people, and incidently, write for the machine. And, as a benefit, you get a book to publish, which counts on your resume rather than a file of code that doesn't.

[Tim Daly]

"pile of sand" (POS) ...

[Johan Commelin]

I'm quite happy that 20 pesky little trivial lemmas all fit on one screen. If all of those trivialities came with a paragraph of documentation, I think it would be harder to find something for me.

[Johan Commelin]

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

[Tim Daly]

How long have you been using Lean?

[Johan Commelin]

But I think one can go overboard on the other side

[Johan Commelin]

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

[Johan Commelin]

Documentation is important. But it's not the reason why mathematicians aren't jumping on board. It simply isn't

[Tim Daly]

It took me 10 courses and 3 years to be able to read current research papers, many of which contain whole pages of nothing but greek rules.

[Johan Commelin]

And if I ask the mathematician in the office next to me why he doesn't use Lean, he'll ask me... do you have the K-theory of coherent sheaves on a scheme?

[Johan Commelin]

If I ask someone on the floor below me, they'll want to know if special holonomy groups are in our library...

[Johan Commelin]

Etc...

[Tim Daly]

I'm one of the authors of Axiom. Axiom was a commercial competitor to Mathematca and Maple. It was considered "one of the big 3". I got a lot of feedback from professors who taught using computer algebra, including those who contributed to Axiom. Documentation mattered for teaching and students kept using what they knew.

[Johan Commelin]

That's the main obstruction. The fact that we don't have étale cohomology groups, or even just the discriminant of a number field, or whatever.

[Tim Daly]

Take a calc textbook. Shake out all of the equations and paste them on index cards. Throw away the words. Now teach calculus from the index cards. The group.lean file is "just the equations", i.e. just the index cards. If all of mathematics were reduced to a wall of 200-character named lemmas I'm not sure it would get much use.

[Kevin Buzzard]

I don't know who's right. My experience talking to mathematicians is the same as Johan -- they're not interested because the things they do aren't there. However in 5 years' time when they are there, documentation will most definitely be an issue. Whether it contributes now or not is something I don't know. I am trying to write documentation for maths undergraduates, but progress is slow because I have a busy job :-/

[Tim Daly]

I can read group.lean because I've done group theory for years. I have no idea what the other lemmas mean or how to use them.

[Johan Commelin]

Take an introductory textbook on group theory. Shake out all the theorems and lemmas and paste them on index cards. Throw away all the words. Now try to find a corresponding entry for each index card in group.lean. For >50% of the index cards, you won't find an entry. On the other hand, for 90% of the lines in group.lean, you won't find an index card...

[Tim Daly]

I'm suggesting that the "library" format for lean is books, not files. Of course the group theory "book" would be written to hold the current lemmas surrounded by paragraphs (useful for word searching). New lemmas would update the book. I'm not suggesting "decorating" an existing group theory book with the lemmas.

[Tim Daly]

Latex was written in lterate programming style in the 70s and is still maintained, mostly because you can read and understand it. Almost every program I've written in the last half century is gone, despite being quite useful for current things, such a remotely monitoring data centers.

[Johan Commelin]

If only Knuth were to write an ITP...

[Tim Daly]

Or a text that explains BDDs for solvers :-)

[Johan Commelin]

Tim, how is Lean different from Coq, Isabelle, whatever? Why are there more pure mathematicians in this small and young community than in the others?

[Tim Daly]

The documentation problem isn't a problem now. It shows up as a problem once the origianl authors leave the project. Witness the tens of thousands of dead projects on github, sourceforge, and savannah.

[Tim Daly]

Well, Benjamin Pierce taught COQ courses in Oregon, which is where I started learning it. And he has a textbook which I can use.

[Johan Commelin]

Many math papers and textbooks are "dead" in that sense. Also, it doesn't answer my question.

[Johan Commelin]

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

[Tim Daly]

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

[Keeley Hoek]

One clear problem is that probably 5% to at most 10% (just a guess, an authority can jump in if they please) of the lemmas in mathlib are actually even stated in a mathematics book. At the very least, in mathlib proofs of important and hard, "real", propositions and theorems are often chopped up in order to remain manageable. I think just the act of stating many of the broken-up pieces as they are phrased in lean would be totally unbearable to read in a mathematics book. Imagine, for example, such a direct translation of https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/sylow.lean
So much is "obvious". That's not even to say it's not worth checking---it just stands in the way of understanding.

[Tim Daly]

But then I've struggled with recent papers for the same reason (look up Guy Steele's talk on logic notation)

[Tim Daly]

Keeley, lemmas are where proofs get creative. A few words about why it is needed gives a clue but a few lines of Lean does not.

[Johan Commelin]

Tim, that's simply not true

[Johan Commelin]

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

[Johan Commelin]

They are there only to handhold the system

[Mario Carneiro]

I think you mean "thousands"

[Johan Commelin]

Usually, page of code after a new definition is just scaffolding. Stuff that mathematicians don't even unconsciously think about when writing a detailed introductory text.

[Mario Carneiro]

I would say not that they are handholding for the system, rather they are there to bring the system up to a basic level of competence, so that you don't have to worry about extremely piddling details for your next project

[Johan Commelin]

Right, that's a better way of putting it

[Tim Daly]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

nothing in that file has a name in math

[Mario Carneiro]

it is not representative of all of math

[Tim Daly]

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

[Mario Carneiro]

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

[Mario Carneiro]

but mathematicians are looking much further afield

[Mario Carneiro]

no, it does not have an "idea"

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

you can give the property a name if you want, but it's just a thing that is true

[Marc Huisinga]

but even if it does grow to millions, most of those lemmas wouldn't benefit much from extensive documentation.
i suppose the normal workflow is the following: you encounter a technical issue in one of your proofs that is intuitively obvious but would be bothersome to prove. you use library_search or some other lemma search tool to resolve the technicality, and then go on with your proof.
there's really not much beyond the lemma type that matters.

[Tim Daly]

I'm just trying to suggest that there might be methods for the Lean project to survive once the original authors leave. 10,000 lemmas in flat files like group.lean is completely unmaintainable.

[Mario Carneiro]

again, group.lean is not representative

[Mario Carneiro]

look around

[Mario Carneiro]

documentation is much more important in places where it's not bleeding obvious why the theorem is true

[Tim Daly]

Are you suggesting that there ARE books in Lean?

[Mario Carneiro]

TPIL?

[Tim Daly]

I'm reading that.

[Tim Daly]

Ah, well. I'm done.

[Mario Carneiro]

I have heard a lot of praise for that book, specifically as it relates to documentation making it easy to get into lean

[Mario Carneiro]

I think we are all aware of the importance of documentation, and there is a push for more high level documentation in mathlib

[Johan Commelin]

Tim, I am sincerely interested in your thoughts on why there are disproportionately many pure mathematicians in the Lean community compared to other prover-communities. Even though Lean is the youngest of them all.

[Tim Daly]

I'm in "the lean community" because Jeremy Avigad taught a class, so I know how to use it. I want to use it underneath Axiom as my proof engine and Jeremy has been most helpful with that. Without Jeremy's help I probably couldn't even read the group.lean file.

[Tim Daly]

Axiom has over 10,000 functions and 1100 "typeclasses". I fully understand how hard it is to maintain the mathematics, the compiler, and the interpreter. Why when I open-sourced Axiom, it had about 3 useful comments in total. Who would possibly need more?

[Tim Daly]

Who doesn't understand Risch integration with radical field extensions? Why bother to even include a reference to a paper?

[Tim Daly]

Lean is following the same path Axiom took. I'm trying to suggest ideas that keep it from becoming an open source project maintained by one person and used by 4 on odd months.

[Tim Daly]

Axiom was developed at IBM Research, contains the results of many PhD theses, costs an extimated 42 million dollars to develop, and involved mathematicians worldwide.

[Sebastien Gouezel]

You can have a look at more recent files, where we are precisely trying to enforce more documentation, but at places where it is useful -- i.e., there are nonobvious definitions or design decisions. For instance https://github.com/leanprover-community/mathlib/blob/master/src/geometry/manifold/manifold.lean, that I wrote recently and for which the more than 100 comments in the PRs made me vastly improve the documentation. Does it correspond to what you are looking for, or how would you envision things for better documentation?

[Tim Daly]

The key question is, what discipline is required in development so that when Lean has 100,000 lemmas, 5,000 theorems, and dozens of fields of mathematics, it can still be maintained by people who have no idea what a homology is.

[Johan Commelin]

No. That is not the key question.

[Johan Commelin]

The key question is: why are pure mathematicians not using ITPs on a large scale right now?

[Tim Daly]

Sebastien, I'm quite fond of literate programming. We all understand books, how to write them, how to navigate them, how to orgainzie them, and how to index them. It is trivial to extract code from a latex document.

[Tim Daly]

Johan, that's where we differ. Axiom's motto is "The 30 Year Horizon". I'm looking at what Axiom needs to be in 30 years, say as a trusted computational oracle for proof systems. You're looking at enlarging the community this month. So we're talking about different objectives.

[Mario Carneiro]

Johan didn't say Lean, he said ITPs

[Mario Carneiro]

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

[Tim Daly]

If you were given Lean and everyone else left, could you maintain it and extend it? The C++ code is quite clever.

[Johan Commelin]

If I were given all maths textbooks in the world, and everyone left... all I could do was sit on top of them...

[Mario Carneiro]

Tim, that kind of happened with lean 3

[Johan Commelin]

Tim, I never said "this month". But I do know that (i) we are moving towards 30 years later one month at a time, and (ii) it takes more than documentation of trivialities to get mathematicians interested.

[Johan Commelin]

Why do you think I started using Lean, and why am I still using it? Because of superb documentation?

[Tim Daly]

Someone working in Cubical Type Theory isn't going to find much support. And since academic promotions never measure code output (withness William Stein) there is no upside to writing Lean theories.

[Tim Daly]

Books, however, count.

[Johan Commelin]

It depends...

[Johan Commelin]

... on the contents.

[Mario Carneiro]

there you've stumbled on one part of our plan for world domination - first fix the financial incentives by making mathematicians care about computers and formal mathematics

[Mario Carneiro]

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

[Tim Daly]

I worked with Gilbert Baumslag, the leader of the field of Infinite Group Theory. He wrote 125 papers on the subject. I open-sourced Magnus, which automates Infinite Group Theory calculations. I THINK there were 3 users.

[Tim Daly]

Convincing mathematicans to use computers (the source of all frustration) is like convincing cats to use the internet. You can barely get them to do a google search as it takes time away from their next paper.

[Tim Daly]

I feel it is like the transition from the 19th to the 20th century. 19th century mathematicians resisted the idea of proofs. 20th century mathematicians resist the idea of ITP. Progress in science is measured one funeral at a time.-- Max Planck. So design your system for the 30 year horizon so it is possible to maintain it by non-authors and non-experts.

[Tim Daly]

If you want ITP mathematicians you have to grow them. So you need courses. You need documentation. You need degrees which recognize programs as well as papers and books. Current mathematicians are successfully set in their ways and they know where credit lies.

[Johan Commelin]

Why do you want to use Lean as backend for Axiom? Wouldn't metamath be a lot better for your use case?

[Johan Commelin]

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

[Johan Commelin]

The checker is so small that if you write 3000 lines of comments, you will have a paragraph per line of code.

[Tim Daly]

I'm looking at several systems (COQ, AGDA, IDRIS, HOL, ISABELLE). HOL88 is interesting because it is implemented in Common Lisp and I can embed it in Axiom directly (which is also Common Lisp). Lean is interesting in particular due to Jeremy Avigad. I used it a bit and now I'm trying to communicate between it and the compiler. Axiom is typed everywhere, at every level, and is dependently typed so I need a robust system.

[Tim Daly]

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

[Andrew Ashworth]

FWIW I figure most people don't use ITPs because being formal is a chore. Nobody cares about Bourbaki, and nobody cares about convincing a computer they are correct. In that sense they are a solution in search of a problem. I think they will take off once we true believers formalize enough math and develop enough useful tactics that the software starts being a net gain in productivity as opposed to a 10x reduction.

[Tim Daly]

Andrew, I'm not sure how far tactics can carry you toward that goal. The undecidability issue is an issue. Axiom uses heuristics at runtime to resolve type questions that can't be computed at compile time. I expect to run into the same issue once I try to prove some of Axiom's algorithms correct. Also, tactics have to somehow be related to the specification language of the algorithms and I'm not sure what to think about that connection yet. It is still an "open research question" for me.

[Tim Daly]

Most Lean work isn't proving algorithms, of course, so I'm out in left field near the corn silo.

[Tim Daly]

Also, note that there is almost no person in common in the bibliographic references in ITP and Computer Algebra. James Davenport seems to be the only crossover I can name. There are 2 "silos" of computational mathematics and the computer algebra people I know can't read the logic literature.

[Tim Daly]

The Axiom Sane project (Sane is a synonum for rational, coherent, judicial, and sound) is trying to build a bridge between these two fields, merging computer algebra and theorem proving machinery.

[Andrew Ashworth]

I see that Axiom wants to call Lean under the hood. Is it feasible that I could call Axiom from Lean and get a proof certificate for things that a CAS can do? For example, I would love to call out to a cylindrical alg decomp algorithm, or matrix decomposer alg, or symbolic integrator.

[Andrew Ashworth]

I guess in these cases it's difficult since not only the result needs to be returned, but also the sequence of transformations that lead up to it

[Tim Daly]

Andrew, that's exactly the goal of the Axiom Sane project. Axiom should be a trusted oracle for computing algorithms. Libraries like complex numbers, computing primes, doing CAD, etc. are easy in Axiom but providing a trusted algorithm and a proof certificate is the center of the research question. The oracle response should provide the answer and a proof that the checker can check

[Tim Daly]

I can't imagine trying to encode the Risch integration algorithm in Lean. It requires too much algorithmic machinery, most of it at the PhD thesis level. But it already exists in Axiom.

[Tim Daly]

The idea of "encoding all of mathematics" doesn't seem to mention the computer algebra field. Certain algorithms (e.g. Buchberger's algorithm) seem to have been proven but the whole subject of Infinite Group Theory, which is mostly non-terminating procedures, doesn't seem to fit into the proof systems easily.

[Mario Carneiro]

I think that Andrew's suggestion is the more profitable angle here. Rather than attempt to have lean be a component of axiom, see if you can modify axiom to produce certificates of its results that can then be checked in a theorem prover like lean

[Mario Carneiro]

You could also just reimplement selected algorithms in lean

[Mario Carneiro]

The problem with treating Axiom as a black box is that you don't trust it, and the very purpose of the project seems to be to make it more trustworthy. The only way you can achieve that is either by whiteboxing the algorithm and proving it correct, or by having the algorithm validate any outputs it gives by producing proofs alongside.

[Tim Daly]

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

[Kevin Buzzard]

If you want ITP mathematicians you have to grow them. So you need courses. You need documentation. You need degrees which recognize programs as well as papers and books. Current mathematicians are successfully set in their ways and they know where credit lies.

I am taking a risk in my job by not producing the standard research papers which I used to produce. My justification for this is that I am attempting to put courses together. But I won't be able to change our UG maths degree, other than by adding a pure Lean course to it (which I no doubt will try to do at some point). It will still just be one of many.

[Keeley Hoek]

But the lean course will exist, Kevin! :D

[Tim Daly]

Survey question: What is the biggest concern developers have about open source:

Result: Perhaps the clearest finding from this question is that 46% of respondents indicated risk about how well packages will be maintained into the future is either a major or a moderate obstacle

https://thenewstack.io/what-is-the-biggest-concern-developers-have-about-open-source/

[Luca Seemungal]

@Kevin Buzzard Speaking about Lean courses, have you finished docs for the incoming freshers / is it viewable by us? I'm a Warwick second year and am fairly interested in this stuff. I've spent the summer trying to learn it but it's all fairly impenetrable. Some docs for maths undergrads would be obviously very helpful. If they're not finished yet I'll just actually concentrate on my degree (for once ;))

[Tim Daly]

Jeremy Avigad used the Lean browser to organize his class. You might consider adding sections to the browser text and organize it by lecture.

[Kevin Buzzard]

@Luca Seemungal Hmm, there are many things which are half-finished, including my preparation for my lectures this week, which have to take priority right now. But we're getting there.

[Bryan Gin-ge Chen]

Not about Lean specifically, but this event looks interesting: https://www.helixcenter.org/roundtables/mechanization-of-math/

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

Internet is so wonderful...

[Tim Daly]

There is an interesting talk by John Seale (of the Chinese Room fame), that is related to the question of "machine checked proofs".
I suggest you take careful notes of the definitions he uses in the first 5 minutes as the whole talk rests on them.
https://www.youtube.com/watch?v=rHKwIYsPXLg

[Patrick Massot]

I watched 23 minutes but I hesitate to continue. Is there any moment when he does something else than repeating: "let's laugh together at how stupid are people who disagree with me" and "the computer is not intelligent because it has zero intelligence"?

[Patrick Massot]

I don't say I disagree, but I was hoping for arguments instead of authoritarian assertions and jokes.

[Mario Carneiro]

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

[Mario Carneiro]

Tim is right though - his argument hinges on a linguistic matter between two senses for what is meant by intelligent

[Mario Carneiro]

it's not all about the chinese room

[Bryan Gin-ge Chen]

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!

Logical verification in Lean. ~ A. Bentkamp, J. Blanchette, J. Hölzl. https://github.com/blanchette/logical_verification_2019/raw/master/logical_verification_in_lean.pdf #eBook #ITP #LeanProver #Logic #FunctionalProgramming

- José A. Alonso (@Jose_A_Alonso)

[Kevin Buzzard]

It still amuses me that computer scientists are quite happy to have entire chapters on metaprogramming and monads before the section on "adding two numbers" :D

[Kevin Buzzard]

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

[Luca Seemungal]

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

[Jason Rute]

So where is the scorpion section in mathlib? https://i0.wp.com/chalkdustmagazine.com/wp-content/uploads/2019/10/level.jpg

[Kevin Buzzard]

Yeah what the heck is that scorpion thing about?? The UCL people did the graphics, I don't know what they were thinking there.

[Kevin Buzzard]

But addition and multiplication world are here: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

[Johan Commelin]

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

[Johan Commelin]

I mean, it really fits in the theme

[Johan Commelin]

Guess who modeled for the second charachter in this pic: https://i2.wp.com/chalkdustmagazine.com/wp-content/uploads/2019/10/lean-e1571862471361.jpg?resize=670%2C300

[Kevin Buzzard]

It's the launch party of the mag this evening and I'm wearing a pair of trousers which are as close as possible to those depicted

[Kevin Buzzard]

They never told me they were going to do all this crazy graphics, I only found out a couple of weeks ago and I wrote the article months ago. And I didn't even notice what Johan is pointing out!

[Kevin Buzzard]

I showed it to my daughter and she said "oh wow Dad that's you!" and I'm like "is it??"

[Johan Commelin]

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

[Kevin Kappelmann]

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

... I was about to do so, but I do not have the permissions :( https://zulipchat.com/help/add-custom-emoji

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

maybe I should think of a better game

[Kevin Buzzard]

Although others have done it before, and probably they've even done it better (Patrick showed me some impressive stuff I remember), I wonder if we can just get some sort of little suite of games like this, just to get people interested.

[Reid Barton]

I've been meaning to make stickers based on the Lean logo, but now I know what I really need is that start screen

[Luca Seemungal]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

Just saw this on the front page of the internet:

https://www.reddit.com/r/math/comments/dnc0jj/imo_grand_challenge_automated_problem_solving/

[Kevin Buzzard]

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

[Mario Carneiro]

I was on the front page for a while :D

[Kevin Buzzard]

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

[Johan Commelin]

@Kevin Buzzard Well... they certainly are small victories within the CS community. But how many pure mathematicians read hacker news? Probably about as many as use ITP's...

[Chris Hughes]

IMG_20191101_144932.jpg

[Chris Hughes]

Lean related graffiti in room 342

[Miguel Raz Guzmán Macedo]

Nice IMO grand challenge!

Is there a prize?

[Bryan Gin-ge Chen]

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

[Sebastian Ullrich]

@Marc Huisinga presented his bachelor's thesis on a partial verification of the compiler in our reference counting paper (done in Lean 3) yesterday. Apart from a much more in-depth description of the IR and compiler than we could have put in the paper, there are some good observation about effective proving in Lean in general in section4, as well as a self-contained section (5) about the list/multiset group function (which he might want to PR to mathlib at some point?).

[Mario Carneiro]

The formalization mentions obtain?

[Mario Carneiro]

but also #check

[Mario Carneiro]

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

[Sebastian Ullrich]

It's the obtain tactic. I guess we never updated lstlean.tex to remove the obsolete keyword.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Marc Huisinga]

yes, it's the obtain tactic. the proof code certainly still needs to be cleaned up, especially before contributing anything to mathlib. many non-terminal simps, lots of duplication and several instances where i miss-use let and should use have instead :)

[Kevin Buzzard]

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

[Patrick Massot]

Some new "Lean in the wild": Sébastien got a prize for theorems he didn't formalize yet, but half of the interview he gave to the CNRS website is propaganda for proof assistants.

[Johan Commelin]

@Sebastien Gouezel Congratulations! :octopus: :cake:

[Sebastien Gouezel]

Thank you!

[Wojciech Nawrocki]

Slightly more unusual spotting of Lean in the wild: George Hotz has livestreamed writing a small parser for Metamath files on Twitch back in November.

[Mario Carneiro]

first 40 minutes: why is the hello world example broken

[Simon Cruanes]

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

[Mario Carneiro]

It's actually pretty funny, during the stream he visits the MM0 page like 5 times when searching for things about metamath or lean (and usually coming up empty). Apparently I've got good SEO

[Kevin Buzzard]

https://agentultra.github.io/lean-for-hackers/ -- hello world stuff! It had never occurred to me to get Lean to print anything before.

[Tim Daly]

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

[Bryan Gin-ge Chen]

@James King made a thread about his guide here.

[Kevin Buzzard]

oh nice, thanks Bryan. I see now that I starred that post when it appeared but I never went back and "tidied up recent stars", my bad.

[Patrick Massot]

Kevin, did you notice that "The primary focus of Lean is mathematical research and its intended audience are mathematicians." We can be proud of what we did. By taking over this forum, we managed to get James completely confused about Lean's origins an intended audience. :grinning:

[Kevin Buzzard]

I did notice that yes :-)

[James King]

I am completely confused and PRs are welcome. I've talked to various people around the community but I haven't met all of you nor had a chance to meet Kevin, Jeremy, or Leo. :smiley:

[James King]

I made the guide after watching George Hotz try Lean on his "esoteric language sundays" twitch channel and being stymied in a similar fashion by the empty sections on the programming language bits of the Lean documentation. I hope to round it out a bit and work with Simon to contribute parts to the official docs.

[James King]

Presently wrapping up work on a JSON parsing library for Lean3 to serve as the intro for the next section to the guide. (I'm really humbled that people have actually read it...)

[Kevin Buzzard]

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

[Kevin Buzzard]

"The lean zulip server demonstrates that good communication tools can help communities thrive, make it easier for newcomers to ask questions, and lower friction for discussions. "

[Jasmin Blanchette]

Kevin, since when do you read the AAR newsletter? Next thing you know, you'll be attending IJCAR or CADE.

[Simon Cruanes]

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

[Kevin Buzzard]

I gave a talk in Bath on Tuesday and some computer scientists attended, and one of them emailed me the newsletter afterwards :-)

[Jasmin Blanchette]

I used to be the editor of that beautiful publication. :)

If you want to get it delivered to your mailbox (4-5 times a year), you can ask Sophie Tourret at newsletter@aarinc.org . She's an Isabelle user, though, so you might want to keep a low profile.

[Johan Commelin]

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

[Patrick Massot]

Who did he provoked this time?

[Johan Commelin]

Just his blogpost from over a week ago (-;

[Kevin Buzzard]

https://www.imperial.ac.uk/news/196435/growing-plants-without-soil-amongst-frontier/

Go me, I got money for a Lean post-doc :D

[Kevin Buzzard]

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

[Andrew Ashworth]

Not sure if this was posted anywhere else, but I saw a presentation go up about Lean at Imperial College London: https://www.researchgate.net/publication/339827943_University_students'_proof_writing_and_LEAN_theorem_prover_the_case_of_the_abundant_number_task

[Kevin Buzzard]

Athina Thoma is the education post-doc who watched my students learning Lean, interviewed and surveyed them, and tried to draw rigorous conclusions from an educational perspective.

[Jasmin Blanchette]

I'm not sure if this is "in the wild", but here's the new version of our Lecture notes: https://lean-forward.github.io/logical-verification/2020/index.html#material

Sorry for all the spam. I just want to make sure nobody keeps on reading the old book.

[Bryan Gin-ge Chen]

I think prominent links to the new version at the old course site and github repo would help with that.

[Johan Commelin]

Blogpost about Lean https://ahelwer.ca/post/2020-04-05-lean-assignment/ (mentions NNG). It's urrently place 14 on HackerNews: https://news.ycombinator.com/item?id=22789953

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

Hitchhikers Guide Lean book now on front page of hacker news

[Anne Baanen]

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

[Johan Commelin]

They are saying silly things over there

[Johan Commelin]

Like you can't do epsilon delta proofs in Lean

[Johan Commelin]

Clearly didn't read TFA before commenting

[Patrick Massot]

I'm not sure arguing a lot about this is a good use of our time. Writing better documentation and tutorials seem like a better idea to me.

[Rob Lewis]

Johan Commelin said:

They are saying silly things over there

Doesn't this apply to literally every comments section on the internet? This will keep happening no matter how perfect the documentation and tutorials are :)

[Anne Baanen]

Natural number game on Reddit: https://www.reddit.com/r/math/comments/fwlgf4/natural_number_game_a_game_where_you_learn_to/

[Kevin Buzzard]

Thanks @Patrick Massot -- Patrick encouraged me to give NNG "some love" last week, and I accepted all the PRs, made some edits, and pushed a slightly tidied up version live. Just in time!

[Kevin Buzzard]

My default search engine is duck duck go, and I usually get to the mathlib github repo by searching for the word mathlib, because it's usually the second or third hit. But as of the last 24 hours or so it's consistently been number 1. Is that true for everyone or just me? I thought the point was that they weren't tracking me.

[Marc Huisinga]

third entry for me

[Alex J. Best]

third for me after pearson and matlab

[Ryan Lahfa]

Kevin Buzzard said:

My default search engine is duck duck go, and I usually get to the mathlib github repo by searching for the word mathlib, because it's usually the second or third hit. But as of the last 24 hours or so it's consistently been number 1. Is that true for everyone or just me? I thought the point was that they weren't tracking me.

2nd entry for me

[Alex J. Best]

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

[Marc Huisinga]

"The Mechanization of Mathematics" by Jeremy Avigad

[Sebastian Ullrich]

@Markus Himmel presented his bachelor thesis on diagram chasing in Lean 3 last week. It's a very nice read, even for someone who knows as little about category theory as I do.

[Patrick Massot]

This should be PRed to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/lean.bib right away

[Johan Commelin]

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

[Johan Commelin]

Is this really the first formal proof of the snake lemma? Doesn't some hott lib have it? Or the spectral sequence library by @Floris van Doorn et al?

[Markus Himmel]

I looked for it, but didn't find anything. Perhaps I'm just very bad at searching. I'm pretty confident that it's the first formal proof that is valid in any abelian category.

[Johan Commelin]

lemma four [epi α] [mono β] [mono δ] :  mono γ :=
mono_of_zero_of_map_zero _ $ λc hc,
begin
  chase c using [g,β,f′,α] with b b′a′a,
  have : f a = b, by commutativity,
  commutativity
end

[Johan Commelin]

That is so cool!

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

How much of all this is in mathlib?

[Johan Commelin]

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

[Markus Himmel]

Johan Commelin said:

Markus Himmel Can you comment on how fast this is?

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

[Markus Himmel]

Johan Commelin said:

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

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Markus Himmel]

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

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

(although this wasn't actually completely blocking progress)

[Scott Morrison]

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

[Markus Himmel]

Scott Morrison said:

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

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

[Floris van Doorn]

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

[Noob]

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

[Alex J. Best]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Alex J. Best]

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

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

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

[Jalex Stark]

Is lean code not human readable?

[Alex J. Best]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

but it's not for the untrained human probably

[Jalex Stark]

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

[Alex J. Best]

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

[Alex J. Best]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Andrew Ashworth]

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.

What will math research look like in 20 years? I have no idea, and am pretty sure I'm not alone. Will Interactive Theorem Provers (eg, Lean) be the next phase in math evolution? Maybe, maybe not. (How long did it take for everyone to learn TeX?) Announcing http://bit.ly/interactive-theorem

- Alex Kontorovich (@AlexKontorovich)

[Mario Carneiro]

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

[Andrew Ashworth]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

The sacred The profane https://twitter.com/littmath/status/1280213422995648513/photo/1

- Daniel Litt (@littmath)

[Bryan Gin-ge Chen]

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

More like 6 days, I think...

@littmath The nice thing about Bourbaki is that it doesn't stop compiling every six months when there's a compiler update.

- Daniel Brice (@fried_brice)

[Lucas Viana]

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

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

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

[Andrew Ashworth]

They are already present, in the semiconductor industry

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Johan Commelin]

Just wait till the end of summer :four_leaf_clover:

[Andrew Ashworth]

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

[Kenny Lau]

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

[Chris Wong]

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

[Bryan Gin-ge Chen]

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

[Yury G. Kudryashov]

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

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

[Kenny Lau]

Later he just changed the Constitution

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Rob Lewis]

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

[Johan Commelin]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

Is this really ∃ x y z, true?

[Johan Commelin]

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

[Rob Lewis]

Gabriel Ebner said:

Is this really ∃ x y z, true?

Heh, I was wondering about that too.

[Johan Commelin]

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

[Gabriel Ebner]

I find the source code equally hard to read.

[Johan Commelin]

The bit with the carrier and opens is better.

[Johan Commelin]

But I agree that i has a very ugly type.

[Gabriel Ebner]

The i is fine IMHO.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

That's a de-Bruijn factor of about 80

[Ian Riley]

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

[Johan Commelin]

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

[Ian Riley]

Thanks @Johan Commelin

[Patrick Massot]

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.

[Junyan Xu]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Damiano Testa]

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

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

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

[Johan Commelin]

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

[Damiano Testa]

Johan Commelin said:

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

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I want them to look more like Lean

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

Kevin Buzzard said:

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

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

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

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Adam Topaz]

Kevin Buzzard said:

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

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

[Adam Topaz]

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

[James Arthur]

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

[Kevin Buzzard]

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

[Alexandre Rademaker]

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

[Kevin Lacker]

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

[Alex J. Best]

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

[Kevin Lacker]

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

[Alex J. Best]

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

[Kevin Buzzard]

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

[Jasmin Blanchette]

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

Unfortunately it's the wrong Lean. :half_frown:

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Mario Carneiro]

lol, he linked to docs#euclidean_geometry.dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two

[Mario Carneiro]

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

[Kevin Buzzard]

yeah but check out the shading

[Kevin Buzzard]

I think the joke goes the other way with add_pow

[Joseph Myers]

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

[Mario Carneiro]

I don't think we use square elsewhere

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Joseph Myers]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Rob Lewis]

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

[Patrick Massot]

Yeah!

[Mario Carneiro]

oh wow, inner_product_geometry.norm_sub_square_eq_norm_square_add_norm_square_sub_two_mul_norm_mul_norm_mul_cos_angle is 110 characters

[Patrick Massot]

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

[Joseph Myers]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

Rob Lewis said:

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

I think you can edit blog posts

[Mario Carneiro]

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

[Joseph Myers]

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

[Rob Lewis]

Mario Carneiro said:

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

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

[Reid Barton]

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

[Heather Macbeth]

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

[Rob Lewis]

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

[Heather Macbeth]

Reid Barton said:

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

snap

[Mario Carneiro]

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

[Mario Carneiro]

What ever happened to lean --doc?

[Floris van Doorn]

Rob Lewis said:

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

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

[Mario Carneiro]

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

[Floris van Doorn]

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

[Rob Lewis]

That's probably the easiest option here.

[Rob Lewis]

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

[Rob Lewis]

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

[Patrick Massot]

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

[Patrick Massot]

Presumably Gabriel knows.

[Mario Carneiro]

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

[Rob Lewis]

Aha

[Joseph Myers]

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

[Joseph Myers]

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

[Sebastien Gouezel]

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

[Wojciech Nawrocki]

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?

[Patrick Massot]

The latest one

[Patrick Massot]

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

[Wojciech Nawrocki]

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.

[Mario Carneiro]

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

[Wojciech Nawrocki]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Wojciech Nawrocki]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Wojciech Nawrocki]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Rob Lewis]

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

[Rob Lewis]

image.png

[Reid Barton]

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

[Jesse Michael Han]

Reid Barton said:

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

lean-meme-2.jpg

[Kevin Buzzard]

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

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

[Chris Wong]

Perhaps they took "backwards reasoning" too literally?

[Joe Hendrix]

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

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

[Johan Commelin]

Scott Aaronson wrote:

Matt #24:

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

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

[Johan Commelin]

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

[Alex J. Best]

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

[Johan Commelin]

Wow, Andrej's answer is really good!

[Sebastian Ullrich]

I like the last one as well

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

@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.

[Mario Carneiro]

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

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

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

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

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

also comments but that's not so hard to fix

[Johan Commelin]

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.

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

Thanks!

[Johan Commelin]

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

[Kevin Buzzard]

That sentence does look a bit funny, yes

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Rob Lewis]

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

[Johan Commelin]

ok, fair enough

[Johan Commelin]

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

[Jasmin Blanchette]

Coming soon to the Stedelijk Museum. ;)

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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

[Jason Rute]

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

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

[Jason Rute]

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

[Julian Berman]

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

[Kevin Buzzard]

Jason Rute said:

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

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

[Kevin Buzzard]

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

[Rob Lewis]

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

[Julian Berman]

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

[Kevin Buzzard]

Oh wow!

[Kenny Lau]

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

[Kevin Buzzard]

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

[Faez]

Julian Berman said:

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

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Alena Gusakov]

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

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

[Jason Rute]

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

Looking forward to learning Lean. https://twitter.com/leanprover/status/1346184109035552769

- Christian Szegedy (@ChrSzegedy)

[Julian Berman]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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.

[Carl Friedrich Bolz-Tereick]

/me waves

[Alex J. Best]

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

[Johan Commelin]

/me logs in to upvote

[Jason Rute]

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).

[Alexandre Rademaker]

Can you share the link of the YouTube video??

[Alex J. Best]

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

[Alex J. Best]

Looks like its now up https://www.youtube.com/watch?v=EXpmbAfBNnw&ab_channel=HarvardCMSA @Alexandre Rademaker

[Jason Rute]

Also there are slides here.

[Jason Rute]

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

[Scott Morrison]

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

Do you have suggestions for using gptf regularly within mathlib?

[Jason Rute]

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

[Anthony Bordg]

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

[Kevin Buzzard]

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

[Anthony Bordg]

Kevin Buzzard said:

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

Hello @Kevin Buzzard ,

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

[Joe Hendrix]

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

[Kevin Buzzard]

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

[Joe Hendrix]

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

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

[Kevin Buzzard]

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

[Joe Hendrix]

Seems like a good reason.

[Julian Berman]

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

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

[Joe Hendrix]

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

[Kevin Buzzard]

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

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

(in that case fuzz testing obviously)

[Kevin Buzzard]

Julian Berman said:

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

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

[Julian Berman]

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

[Kevin Buzzard]

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

[Julian Berman]

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

[Julian Berman]

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

[Joe Hendrix]

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

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

[Peter Nelson]

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

http://matroidunion.org/

[Bryan Gin-ge Chen]

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

[Peter Nelson]

It'll be on youtube, yes.

[Julian Berman]

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

[Peter Nelson]

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

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

[Kevin Buzzard]

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

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

[Peter Nelson]

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

[Peter Nelson]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Peter Nelson]

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

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

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

[Julian Berman]

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

[Peter Nelson]

Thanks! I'll post the youtube link when it's uploaded

[Alena Gusakov]

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

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

[Peter Nelson]

https://youtu.be/wMRrSWsZSFM

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

[Yakov Pechersky]

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

[Kevin Buzzard]

Oh nice! I'm involved with that competition.

[Yaël Dillies]

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

[Yaël Dillies]

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

[Chris Hughes]

Dominic Cummings (former chief adviser to Boris Johnson) has tweeted about the Liquid Tensor Experiment https://twitter.com/Dominic2306/status/1402249206967025664?s=20

1/ Fascinating report by a world leading mathematician, P Scholze, on an open source project to use 'proof assistants' on an important maths proof. Byproduct = the computer improved human understanding. Seems clear these tools will play ever greater role https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/

- Dominic Cummings (@Dominic2306)

[Patrick Massot]

Is it like we have our Scott Morrison and the rest of the world have another one? Or is it the same Dominic Cummings?

[Johan Commelin]

Is this good or bad news :scream: :oops: :thinking:

[Yaël Dillies]

Maybe we can now pretend to the millions of pounds Kevin wanted for internships?

[Patrick Stevens]

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)

[Patrick Massot]

It was not serious, Chris's message was very clear.

[Eric Rodriguez]

If only this gave some funding to us!

[Kevin Buzzard]

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...

[Johan Commelin]

For those not following the condensed stream: https://www.nature.com/articles/d41586-021-01627-2

[Anatole Dedecker]

Capture-décran-du-2021-06-18-21-44-04.png :sweat_smile:

[Johan Commelin]

Also, the "Cardinals" labels ended up pointing to a small island containing Zorns lemma

[Marc Huisinga]

Lean was originally created by a computer scientist at Microsoft Research in Redmond, Washington

is unfortunately unspecific. :(

[Johan Commelin]

Yes, I'm sorry about that. Both Kevin and me stressed a more specific version. :sad:

[Patrick Massot]

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).

[Yaël Dillies]

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?

[Yaël Dillies]

Not many rock bands get their name into Nature!

[Patrick Massot]

Johan's version of the labels is at https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/Actual.20graph/near/242583715

[Patrick Massot]

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).

[Johan Commelin]

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:

[Marc Huisinga]

hn frontpage: https://news.ycombinator.com/item?id=27559917
r/math: https://www.reddit.com/r/math/comments/o3caqq/mathematicians_welcome_computerassisted_proof_in/

[Marc Huisinga]

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

[Johan Commelin]

It seems to mightily piss off the Coq community

[Marc Huisinga]

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.

[Eric Rodriguez]

It comes up really easily whenever you google Lean, it was one of the first things I saw about it

[Eric Rodriguez]

So that's probably why

[Marc Huisinga]

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.

[Kevin Buzzard]

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.

[Jasmin Blanchette]

Slashdotted: https://science.slashdot.org/story/21/06/23/1922202/mathematicians-welcome-computer-assisted-proof-in-grand-unification-theory

[Riccardo Brasca]

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.

[Riccardo Brasca]

But don't miss the Liquid Tension Experiment music at the beginning!

[Patrick Massot]

Did we get any reaction at all from the musicians of LTE?

[Riccardo Brasca]

I don't think so, but you should ask @Kevin Buzzard

[Kevin Buzzard]

I don't think so :-(

[Kevin Buzzard]

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.

[Riccardo Brasca]

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.

[Yaël Dillies]

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.

[Julian Berman]

wiktionary says "developer"

[Horatiu Cheval]

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" :)

[Eric Rodriguez]

I mean, what is a "veloper"?

[Johan Commelin]

"velo" means cycle in French, so my guess is "cyclist"

[Horatiu Cheval]

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 :)

[Riccardo Brasca]

Yes, "sviluppatore = developer". I didn't try to explain the difference between a Lean developer and someone who contributes to mathlib

[Yaël Dillies]

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.

[Jason Rute]

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...

[Huỳnh Trần Khanh]

bad example, I made that thread :joy: and that was more like an honest question than an attempt to start a flame war :joy:

[Kevin Buzzard]

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 :-)

[Jason Rute]

E535F051-CA90-49FB-AE66-36A68263207B.jpg

[Jason Rute]

9DCEC371-E26B-4872-ACFD-C4A45B3B9A4C.jpg

[Marc Huisinga]

The Lean 4 Theorem Prover and Programming Language

[Eric Wieser]

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)

[Kevin Buzzard]

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.

[Kevin Buzzard]

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 :-(

[Johan Commelin]

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

[Jasmin Blanchette]

Earlier today Leo presented his Lean 4 system description, written with Sebastian Ullrich, at the CADE 2021 conference.

[Jasmin Blanchette]

Here's the paper. Oh I see it's above. :smile:

[Jason Rute]

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.

[Kevin Buzzard]

I've just emailed the author of the article. Thanks for pointing this out!

[Jason Rute]

I also just decided to send an email to the address on the server error page. Can't hurt.

[Jason Rute]

It works now. I got a pretty quick response from that support email.

[Kevin Buzzard]

https://twitter.com/3blue1brown/status/1416106848751558658

Also, now there's a 3b1b podcast. The first episode is with @AlexKontorovich. Here's a sample for when we were talking about theorem proving software like Lean. YouTube: https://youtu.be/C-i4q-Xlnis Spotify: https://open.spotify.com/episode/1Y6OUdMO6oKNbOBpIqULQZ?si=429c059c084f485a https://twitter.com/3blue1brown/status/1416106848751558658/video/1

- Grant Sanderson (@3blue1brown)

[Kevin Buzzard]

https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/

[Yaël Dillies]

I like the import tree illustration! It's of course ridiculously small compared to the real thing, but it gets the gist of it.

[Johan Commelin]

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.

[Riccardo Brasca]

Wow, great article!

[Johan Commelin]

https://news.ycombinator.com/item?id=27984471 (no discussion yet)

[Eric Rodriguez]

/r/math: https://www.reddit.com/comments/otdclo

[Patrick Massot]

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"?

[Eric Rodriguez]

Yeah, I was very curious about that too.

[Adam Topaz]

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)

[Adam Topaz]

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.

[Eric Rodriguez]

Their "puzzle" ones often do

[Yaël Dillies]

Ghuuuu, I just understood that Disqus = discuss. The joke took 2 years to go through my French-speaking mind.

[Mac]

@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.)

[Peter Scholze]

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...

[Peter Scholze]

(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.)

[Julian Berman]

It appears Lean and Johan are mentioned on the Condensed mathematics wikipedia page now: https://en.wikipedia.org/wiki/Condensed_mathematics#History

[Kevin Buzzard]

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.

[Filippo A. E. Nuccio]

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.

[Riccardo Brasca]

https://siliconreckoner.substack.com/p/on-the-implications-of-scholzes-liquid?fbclid=IwAR2aPno11mrXweweivDUakzAkl8JOw-DM_VXjgo-I_wTlAOb2DgSJ7QXcyk

[Patrick Massot]

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.

[Patrick Massot]

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.

[Johan Commelin]

Apparently comments can be posted here: https://mathematicswithoutapologies.wordpress.com/2021/08/04/new-entry-on-substack-newsletter-on-scholzes-liquid-tensor-experiment/

[Johan Commelin]

Not saying that we should do that. Just want to point out the possibility

[Marc Huisinga]

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.

[Kevin Buzzard]

Just to be clear, Michael and I are very old friends :-) We work in the same area of number theory

[Peter Scholze]

I'm seeing Michael again (in person, I believe) at an Oberwolfach conference this month. Looking forward to lots of fun conversations :wink:

[Mac]

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.)

[Kevin Buzzard]

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.

[Patrick Massot]

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.

[Oliver Nash]

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.

[Oliver Nash]

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 ...".

[Eric Rodriguez]

Yes, the fact that I can just use F12 to see the proof for something that's supposedly trivial is life-changing

[Jason Rute]

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.

[Jason Rute]

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.

[Filippo A. E. Nuccio]

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).

[Patrick Massot]

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.

[Jason Rute]

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.

[Jason Rute]

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.

[Mac]

@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.

[Filippo A. E. Nuccio]

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.

[Adam Topaz]

This starts in 3 hours, in case anyone is interested.
https://researchseminars.org/talk/ToposInstituteColloquium/33/

[Johan Commelin]

The talk got the following labels :rofl: Computer science algebraic topology category theory logic

[Adam Topaz]

Johan Commelin said:

algebraic topology

:thinking:

[David Michael Roberts]

Totally is algebraic topology.

[Reid Barton]

I just want to point out that the youtube stream currently has 37 viewers

[Adam Topaz]

too many people wanted to verify this... it's up to 45

[Bolton Bailey]

Recording seems to be here https://www.youtube.com/watch?v=alByz_LoANE

[Patrick Massot]

Kevin, could you share your slides?

[Kevin Buzzard]

I made them in reveal-md so it's a little tricky.

[Kevin Buzzard]

slides.pdf

Will this do?

[Yaël Dillies]

Guess what I found in my science magazine... image.png

[Yaël Dillies]

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).

[Riccardo Brasca]

Which magazine is it?

[Yaël Dillies]

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).

[Yaël Dillies]

This is in n°2 p. 13

[Riccardo Brasca]

Merci !

[Johan Commelin]

Hmmm, it's nice that they mention this, but it's a bit sad that they got half of the statements fronw.

[Reid Barton]

I googled for paracompact lattice and the top result was https://leanprover-community.github.io/mathlib_docs/topology/paracompact.html

[Adam Topaz]

That's the goal right?

[Yaël Dillies]

Taking over the Internet? Yes :octopus:

[Riccardo Brasca]

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:

[Reid Barton]

oh, could be

[Johan Commelin]

big brother (-;

[Reid Barton]

I usually don't use google as my first choice search engine so I forgot about that

[Johan Commelin]

but it reads your emails, so it still knows what you like (-;

[Kevin Buzzard]

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

[Anne Baanen]

The amazing news about the Hoskinson Center has spread to Reddit

[Jeremy Avigad]

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.)

We use math to provide scaling for blockchains. Human audits are the standard way to ensure code is error-free. We introduce a stronger alternative: a formal mathematical proof. The LEAN system is used to prove the correctness of the Cairo AIR. https://arxiv.org/abs/2109.14534

- CairoLang (@CairoLang)

[Jeremy Avigad]

Has anyone seen this? https://codegolf.meta.stackexchange.com/questions/23916/language-of-the-month-for-october-2021-lean

[Johan Commelin]

@Jeremy Avigad see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Code.20Golf.20LOTM

[Jeremy Avigad]

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.

[Patrick Massot]

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.

[Johan Commelin]

Do you know where to ask?

[Jason Rute]

Just email Michael Douglas, listed at the top of that website.

[Patrick Massot]

If you want to actually attend the talk and get an answer then you should forward it to me.

[Michael R Douglas]

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.

[Michael R Douglas]

2 PM Eastern Time

[Johan Commelin]

Which is 2021-10-27T20:00:00+02:00 if I didn't make a timezone-calculation-error. (Edit: I did. Should be fine now.)

[Rob Lewis]

I think you did -- 2021-10-27T14:00:00-04:00

[Johan Commelin]

Aah, did you have a DST change already?

[Rob Lewis]

Are we in that annoying window where we're still on DST and you're not?

[Riccardo Brasca]

I think Rob is correct

[Riccardo Brasca]

A friend of mine in Montreal says it's almost 10am there

[Johan Commelin]

Ooh, it seems we're still both on DST but I just can't count.

[Johan Commelin]

There's a reason why I use Lean :rofl:

[Scott Morrison]

And Jeremy's talk is at 2021-10-28T03:00:00+11:00.

[Hunter Monroe]

Lean made Quanta’s list of top mathematical developments in 2021 https://www.quantamagazine.org/the-year-in-math-and-computer-science-20211223/

[Kevin Buzzard]

Yeah, as did Ana Caraiani, who's four doors down from me at Imperial :-)

[Johan Commelin]

Does that mean that Lean made it two years in a row?

[Hunter Monroe]

Yes the second year in a row https://www.quantamagazine.org/the-year-in-math-and-computer-science-20201223/

[Junyan Xu]

DeepMind not mentioned??

[Kalle Kytölä]

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 $C$ doors from me on the same corridor at Aalto, where $C$ is a small positive constant, which is perhaps just a bit worse than Kevin's constant $4$. :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!

[Yaël Dillies]

Zulip describes Lean as an ATP, should we correct them? https://chat.zulip.com/case-studies/lean/

[Arthur Paulino]

IDK about their reach, but might be worth it just to avoid spreading misinformation

[Reid Barton]

I can contact whoever wrote this, what do we want it to say? "automated proof system" -> "interactive theorem prover"?

[Bhavik Mehta]

It already says "Lean is an interactive theorem-prover" later in the article; so that should be acceptable!

[Reid Barton]

https://github.com/zulip/zulip/pull/20848, I guess it will go live eventually

[Alex J. Best]

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 ?

[Yaël Dillies]

Sorry, you posted to the wrong topic.

[Yaël Dillies]

It's not Lean in the wild, it's wild Lean.

[Arthur Paulino]

This looks like a fun answer to "why formalize mathematics"

[Yaël Dillies]

"so that Stephen Wolfram can make funny diagrams"? :rofl:

[Arthur Paulino]

more like "being able to visualize how mathematics comes together"

[Arthur Paulino]

We rarely have the chance to see something like this when we're so focused on figuring out particular vertices

[Junyan Xu]

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.

[Alex J. Best]

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

[Mauricio Collares]

Probably related to https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/ (Ctrl-F "mathlib")

[Eric Rodriguez]

Interesting that set.mm has more theorems yet far less definitions

[Yakov Pechersky]

https://arxiv.org/abs/2201.08364

[Yakov Pechersky]

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.

[Arthur Paulino]

Has anyone seen this article?
The Central Dogma of Mathematical Formalism

[David Wärn]

I wish I hadn't

[Chris B]

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.

[Bolton Bailey]

I found the anecdote about Theorem 2.5.6 funny.

[Arthur Paulino]

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

[Sebastian Ullrich]

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

[Henrik Böving]

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?

[Anne Baanen]

There is a tactic#ring2 that works by reflection. Also the Coq library MathComp is extensively based on reflection.

[Eric Rodriguez]

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

[Anne Baanen]

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.

[Henrik Böving]

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?

[Anne Baanen]

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

[Mario Carneiro]

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)

[Mario Carneiro]

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.

[Bryan Gin-ge Chen]

Given the caveats stated there, have we discussed whether we'll be allowing reduceBool in mathlib after the port?

[Mario Carneiro]

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]

[Mario Carneiro]

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.)

[Patrick Massot]

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.

[Alex J. Best]

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

[Kevin Buzzard]

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.

[Eric Rodriguez]

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!

[Patrick Massot]

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.

[Peter Scholze]

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.]

[Anne Baanen]

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?

[Anne Baanen]

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:

[Yaël Dillies]

Maybe it's an ideology, but for me it's just so much fun!

[Anne Baanen]

Indeed, that's another aspect that is not really touched upon in the article: you can be a formalizer without being a formalist.

[Arthur Paulino]

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

[Marc Huisinga]

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.

[Joe Hendrix]

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.

[Jeremy Avigad]

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.

[Jeremy Avigad]

A clarification: by "that," I mean only the first section of the paper, which spells out the view that Harris (seems to be) attacking.

[Patrick Massot]

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.

[Patrick Massot]

He knows very well that the ideas he is attacking do not exist.

[Henrik Böving]

If that was the case, why is he doing it then?

[Kevin Buzzard]

https://openai.com/blog/formal-math/

[Reid Barton]

Very cool.

[Reid Barton]

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]

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

[Stanislas Polu]

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?

[Yakov Pechersky]

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?

[Arthur Paulino]

Not only tactics, but also some more granular key lemmas

[Mac]

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).

[Mac]

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.

[Kevin Buzzard]

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

[Vincent Beffara]

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:

[Johan Commelin]

Kevin Buzzard said:

https://openai.com/blog/formal-math/

Now discussed on HN: https://news.ycombinator.com/item?id=30181636

[Julian Berman]

Also discussed now by Yannic Kilcher: https://www.youtube.com/watch?v=McpjrsHrEY4#t=11m30s

[Kevin Buzzard]

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.

[David Michael Roberts]

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?

[Chris B]

@David Michael Roberts https://www.youtube.com/watch?v=O15dbvEDApg

[Jason Rute]

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

[Jason Rute]

@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.)

[Jason Rute]

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.

[Junyan Xu]

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

[Adam Topaz]

The game is afoot...

https://twitter.com/EgbertRijke/status/1505168608615354369?s=20&t=3aXnrqzJz6f9egLwjzTxAQ

@EscardoMartin @Aqissiaq @jonaprietoc The plan is to overtake lean’s mathlib

- Egbert Rijke 🇺🇦 (@EgbertRijke)

[Ruben Van de Velde]

Are we comparing lines of code? Because I have some golfing I can revert :)

[Kevin Buzzard]

I think that competition is healthy.

[Adam Topaz]

IMO The true competition is to define $\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.

[Arthur Paulino]

no linebreaks

[Kevin Buzzard]

Well at least we know where to start there -- define an etale morphism of schemes.

[Adam Topaz]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

Not really "in the wild" but Heather is talking in London Learning Lean today at 2022-03-24T16:00:00Z , about Fourier series in mathlib. See https://researchseminars.org/talk/LondonLearningLean/7/ for Zoom details.

[Riccardo Brasca]

If I understand correctly this, Kevin's talk at the ICM will be at 2022-07-09T09:00:00+02:00

[Bryan Gin-ge Chen]

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).

[Yaël Dillies]

Large but lean

Well, Lean is pretty lean.

[Johan Commelin]

Here's the HN discussion: https://news.ycombinator.com/item?id=31101332

[Henrik Böving]

Yaël Dillies said:

Large but lean

Well, Lean is pretty lean.

:= by rfl

[Jason Rute]

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.

Excited to release our latest work: https://arxiv.org/abs/2205.11491 We present a new algorithm, HyperTree Proof Search (HTPS) inspired by the recent success of AlphaZero. Our model is able to prove mathematical theorems in a fully automated way and significantly outperforms the SOTA. 1/n https://twitter.com/GuillaumeLample/status/1529107248013795333/photo/1

- Guillaume Lample (@GuillaumeLample)

[Leonardo de Moura]

Thanks for sharing. It is awesome that @Gabriel Ebner is one of the co-authors.

[Jason Rute]

@Christian Szegedy and Gary Marcus have a simple bet going on whether by 2029 the following will happen:

I am happy to have a long bet with anyone including @MelMitchell1 or @GaryMarcus on the formalization + theorem proving capabilities of AIs by 2029. I am fairly confident that we will have a system with comparable or stronger capabilities to/than strong human mathematicians. https://twitter.com/Plinz/status/1534075309300928512

- Christian Szegedy (@ChrSzegedy)

• A diverse set of 100 graduate text books are automatically formalize/verified in a popular proof assistant (eg Lean).
• 10% of problems from a preselected 100 open human conjectures is proved completely autonomously.

Not very Lean specific, but Lean is mentioned a few times. Regardless of the proof assistant I would find this quite impressive.

[Filippo A. E. Nuccio]

There is a new article by Harris on Lean and LTE here; it is in French, and I found it very balanced and objective, both in telling about his (mild?) concerns expressed at personal level, and in describing what proof assistants are.

[Alex J. Best]

See also: https://siliconreckoner.substack.com/p/mathematicians-challenged-by-machines for a little on Harris' backstory on the article, and an early english version (for those without a Pour la Science subscription :smile:)

[Kevin Buzzard]

Broken link in Harris' English article: https://leanprover-community.github.io/liquid/dep_graph.html

[Anne Baanen]

Probably my French is not quite good enough and I missed it, but it seems that the article does not draw a clear distinction between interactive theorem proving and automated theorem proving. As long as computer proofs remain mostly interactive proofs, I am quite certain we're going to need many more human mathematicians :P

[Anne Baanen]

I very much appreciate the sidebar on conjecture generation, which in my opinion is a much more interesting task to see automated than proof generation, since it is in a way so much more unrestricted.

[Arthur Paulino]

conjecture generation

Make it rain crazy questions :eyes:

[Filippo A. E. Nuccio]

Anne Baanen said:

Probably my French is not quite good enough and I missed it, but it seems that the article does not draw a clear distinction between interactive theorem proving and automated theorem proving. As long as computer proofs remain mostly interactive proofs, I am quite certain we're going to need many more human mathematicians :stuck_out_tongue:

You are right, there is no such clear distinction.

[Jason Rute]

Which I think is common in his articles (to conflate the two).

[Gabriel Ebner]

Just stumbled on another article about Lean in Quanta Magazine:
https://www.quantamagazine.org/can-computers-be-mathematicians-20220629/

And if so, will mathematicians like me and my guest ever be out of a job? Not just out-computed, but out-thought? So joining me now is Kevin Buzzard, professor of pure mathematics at Imperial College London.

[Eric Wieser]

Kevin said on discord that he thought this interview happened in 2021, hence the claim that Yaël has only been around 6 months

[Kevin Buzzard]

yeah I'd forgotten about it!

[Anthony Bordg]

Of possible interest: Should Machines Replace Mathematicians? by John Horgan in the Scientific American, which features André Weil, myself, Shinichi Mochizuki and Michael Harris (in the order of the text).
It's very difficult for journalists to give subtle accounts and not to deform to some extent one's view, but it's ok, one has to live with this fact.

[Julian Berman]

For a minute I came in expecting Mochizuki had commented on theorem provers (or somehow Weil given I didn't know how long ago he'd passed). Fun article though, congrats for being featured in it.

[Anthony Bordg]

Thank you Julian.
I would be curious to have Andre Weil's take on proof assistants!

[Kevin Buzzard]

I was lucky enough to meet him, but I didn't ask :-) (it was 1995)

[Adam Topaz]

Julian Berman said:

For a minute I came in expecting Mochizuki had commented on theorem provers (or somehow Weil given I didn't know how long ago he'd passed). Fun article though, congrats for being featured in it.

FWIW, Mochizuki does have some comments about "computer verification" in section 1.12 of
https://www.kurims.kyoto-u.ac.jp/~motizuki/Essential%20Logical%20Structure%20of%20Inter-universal%20Teichmuller%20Theory.pdf

[Alex J. Best]

Riccardo Brasca said:

If I understand correctly this, Kevin's talk at the ICM will be at 2022-07-09T09:00:00+02:00

It seems this is happening in 10 minutes at https://www.youtube.com/watch?v=SEID4XYFN7o&ab_channel=InternationalMathematicalUnion, but I've managed to get the time wrong twice already so who knows

[Jason Rute]

Nice talk @Kevin Buzzard! (And just to be clear, since it confused me, but that YouTube link is also for the recorded video. It did however take a few seconds to play on my phone.)

[Floris van Doorn]

Note: it starts at 4:00

[Marc Huisinga]

A reddit thread discussing Kevin's talk

[Miguel Marco]

I didn't know about the system he shows, that allows to write latex and link it to lean code.

Is there documentation for that?

[Floris van Doorn]

https://github.com/PatrickMassot/leanblueprint

[David Michael Roberts]

Section 1.12 of Mochizuki’s document is not enlightening reading, he does not appear to be up to speed with what proof verification is about.

[Julian Berman]

Looks like Kalai wrote a short post on @Kevin Buzzard's ICM talk: https://gilkalai.wordpress.com/2022/07/17/icm-2022-kevin-buzzard-the-rise-of-formalism-in-mathematics/

[Yaël Dillies]

The cycle of formalisation. I formalise Kalai's results, Kevin mentions my work, Kalai posts about Kevin's talk.

[Kevin Buzzard]

@Bhavik Mehta your combinatorics repo gets a namecheck!

[Adam Topaz]

For those (like me) who couldn't go to ICERM but are still interested in seeing some of the lectures, they are now available on the ICERM workshop webpage:
https://icerm.brown.edu/topical_workshops/tw-22-lean/

[Brandon Brown]

Does anyone have a recording of the panel on using Lean for teaching?

[Jeremy Avigad]

ICERM policy prohibited it. They got speakers to sign release forms to post the talks, but the idea with a panel is that you should be able to have informal discussions with people in the audience without having to worry about being recorded.

[Eric Wieser]

The list of accepted papers for CICM 2022 is now published at https://cicm-conference.org/2022/cicm.php?event=&menu=accepted. I count at least 3 Lean papers!

[Kevin Buzzard]

Congratulations to @Eric Wieser , @Bhavik Mehta , @Jujian Zhang and @Sebastian Monnet !

[Henrik Böving]

Dunno if this was posted yet but there is a video about Lean on computer phile https://www.youtube.com/watch?v=prYaTrZUces

[Adam Topaz]

I'm kind of surprised computerphile and/or numberphile didn't catch on to lean sooner!

[Mario Carneiro]

We need to get Kevin to do an interview with numberphile, I think it would go really well

[Adam Topaz]

Unfortunately, it seems that Brady Haran still hasn't jointed our zulip (unlike the rest of the world)

[Chris Hughes]

Kevin told me he knows Matt Parker well

[Eric Rodriguez]

first video: a formalised proof that the parker square was nearly there

[Arthur Paulino]

Lean 4 mentioned as part of the stack of a trustless software marketplace: https://www.youtube.com/watch?v=aeRH8ajJmqs

The explicit mention happens around 26:40

[Marc Huisinga]

A longer twitter thread discussing @Mario Carneiro's MSc thesis and how it deals with global choice. This is just one leaf of it, you'll have to navigate the messy twitter UI yourself ...
Here's an archive link for this branch of the discussion in particular for if you don't have a twitter account.

@andrejbauer @jonmsterling @EscardoMartin @yforster_cs @XenaProject But I'm afraid it is still not what makes Mario's interpretation work. Replacement is also compatible with univalence.

- Egbert Rijke (@EgbertRijke)

[Junyan Xu]

latest in the thread:
https://twitter.com/EgbertRijke/status/1564362100566380559?s=20&t=7Hzf2_CD1lnoO39YrtXjxg

@jonmsterling @andrejbauer @EscardoMartin @yforster_cs @XenaProject The more I think about it, the less I believe Mario really constructed a model of Lean in ZFC. Also in ZFC the AC only gives you mere existence of a choice function. The way AC is applied gives mere existence of a global choice function, but he pretends he got his hands on one.

- Egbert Rijke (@EgbertRijke)

[Mario Carneiro]

@Egbert Rijke I'm happy to respond here, but I don't do twitter. But it seems like the main points are already on the table so I don't have much to add.

[Jason Rute]

Ok, now you just have to formalize your thesis. :smiling_devil:

[Jason Rute]

If this is going to be a long discussion, maybe it could be its own thread.

[Jason Rute]

I have to admit I’m confused a bit by some of the points. Is the main idea that Lean’s choice operator is what is called “global choice”, or Hilbert’s epsilon operator? And that this choice is stronger than what you get in ZFC? The ZFC version is closer to AC used in HoTT? Then realizing that AC and replacement are compatible with Univalence but global choice isn’t, this casts doubt on Mario’s argument in his thesis which seems to prove that one can get global choice in ZFC plus countably many large cardinals? If this is the case, then Mario’s thesis only shows Lean is equiconsistent with ZFC plus large cardinals plus global choice? (I could be totally misunderstanding.)

[Egbert Rijke]

Hi! Sorry, I barely open zulip anymore these days.

I can summarize the main points of the discussion here. In your thesis it is clear: You assume large enough cardinals to obtain universes V_0,...,V_omega, so that every type in the i-th universe is in Vi. By the axiom of choice, there exists a choice function that selects an element of every inhabited set in V_ω. Then I put my type-theory hat on again, to see if I could understand the argument from the type theoretic point of view.

Since we're here on the Lean zulip, let's assume that every type is a set. The axiom of choice asserts that (∀(x:X), ∥Y(x)∥) → ∥Π(x:X), Y(x)∥for every type X and every family of types Y over X. Applying this to V_ω we get that (Π (X:V_ω), ∥X∥ → ∥X∥) → ∥Π(X:V_ω), ∥X∥ → X∥. This is also how you apply it in your thesis. The thing I thought was a problem was that you only seem to get ∥Π(X:V_ω), ∥X∥ → X∥, but to interpret Lean's global choice you want Π(X:V_ω), ∥X∥ → X. Then Andrej pointed out that actually you're not _constructing_ a model, but you're proving that a model exists. This cleared up the discussion to me, but do you also see it this way?

[Egbert Rijke]

In other parts of the discussion I was wondering what would be needed in type theory to get an implication AC → Global-Choice.

Andrej was very confused about what I wanted and suggested erroneously that this is possible in CIC. It is not. The argument here is as follows: The axiom of choice is consistent with the univalence axiom, but the global choice principle is not consistent with the univalence axiom. This implies that if we could simply prove global choice from AC, then in combination with univalence we would be able to reach a contradiction. Furthermore, any axiom that is compatible with the univalence axiom also won't help you prove global choice from AC. This leads to the question, what extra assumptions do we need to make about type theory in order for your argument to go through in type theory. I still don't know the answer. The suggestions by Andrej in that thread were not helpful.

So that is a summary of the other part of the discussion.

[Matthew Ballard]

Building Better Systems seems to have the highest number of Lean mentions in the podcast ecosystems.

[Eric Rodriguez]

https://www.reddit.com/r/math/comments/xcbhdg/beyond_the_liquid_tensor_experiment_the/: reddit discussion about Kevin's latest blogpost on LTE

[Eric Rodriguez]

I don’t see what’s so hard, just write sorry.

[Johan Commelin]

Also https://news.ycombinator.com/item?id=32808045 (0 comments, so far)

[Johan Commelin]

Eric Rodriguez said:

I don’t see what’s so hard, just write sorry.

In fact, this is what we had for a long time :rofl:

[Jason Rute]

A new paper using Codex and Lean 4 meta-programming to auto-formalize to both Lean 3 and Lean 4.

• Towards a Mathematics Formalisation Assistant using Large Language Models

Some more details are in #Machine Learning for Theorem Proving > More papers on autoformalization.
(It's anonymous since it is under review, and ICLR papers are reviewed in public.)

[Jason Rute]

(To be clear, the paper isn’t mine.)

[Patrick Massot]

For people in France, the current issue of the popular science magazine "La Recherche" has a paper on maths formalization: https://www.larecherche.fr/math%C3%A9matiques-informatique/pourquoi-raconter-des-maths-%C3%A0-un-ordinateur. This is a fairly well-known magazine in France. The paper was written by me and a journalist (only my name appears in print because this is what they wanted).

[Patrick Massot]

I should say that I didn't ask to write that paper, the magazine asked me to write it.

[Filippo A. E. Nuccio]

Unfortunately it is beyond a paywall...

[Patrick Massot]

I know, I don't have access either (I was sent a paper copy). You'll need to buy it in your favorite magazine shop.

[Filippo A. E. Nuccio]

Oh, sure I will. Thanks!

[Arfur Schloppenhowler]

James King said:

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...)

Where can I find this? I want to read in JSON and parse it and I have no clue where to begin.

[Eric Wieser]

See docs#json_serializable for what mathlib has to offer in this regard

[Jeremy Avigad]

For a couple of years now, I have been working with StarkWare, using Lean to verify code for blockchain applications written in their programming language, Cairo. We have just made public a system that generates Hoare descriptions and verifies them down to the Cairo machine model. That model, in turn, is verified down to the algebraic certificates that are published on blockchain. We have also made public a verification of Cairo library code that validates secp signatures.

We are in the process of writing a paper on these results, but in the meanwhile, the repository is available here:
https://github.com/starkware-libs/formal-proofs
The README file provides an overview.

[Eric Rodriguez]

Jörg Hanisch said:

Is math solved?
Link to Meta AI
:joy:

A Meta paper with some more AI + 67% accuracy in miniF2F; I seem to remember having this plugin installed!

[Eric Wieser]

The paper is from May it seems? Maybe there's some new stuff they'll show at NeurIPS

[Rémy Degenne]

The deadline for NeurIPS was in May

[Rémy Degenne]

which explains the date of the paper. Of course that does not rule out the possibility that they could present new stuff, but my experience of that conference is that people rarely talk about newer things than what is in the paper.

[Yakov Pechersky]

image.png
Isn't this solution using norm_num basically brute forcing the check for 0-18?

[Eric Rodriguez]

Eric Wieser said:

The paper is from May it seems? Maybe there's some new stuff they'll show at NeurIPS

I mean the extension was fairly recent, I remember the API key being shared here within <2 months

[Timothee Lacroix]

Indeed, the method hasn't changed since the paper has been published. We got slightly better results but as @Yakov Pechersky notes, our proofs are still very much "search" biased : brute-forcing discrete cases or stumbling into recurrences that work by applying induction multiple times. Math is definitely far from solved :p

Regarding the extension, Gabriel merged a PR yesterday that adds the API key / url as defaults for the vs-code plug-in (because searching in zulip wasn't ideal to find it and there is currently no alternative).

[Filippo A. E. Nuccio]

@Timothee Lacroix I have seen the modification in the settings adding the API key&url; does this mean that when I know type sugges, my VSCode automatically tries to connect to the internet and to get suggestions from your method?

[Adam Topaz]

There is a question mark in the top right of the info view that will give the AI suggestions when you click it.

[Filippo A. E. Nuccio]

Thanks, found it!

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as resolved.

[Filippo A. E. Nuccio]

Hmm, I mistakenly marked this stream as "resolved", and cannot unresolve it. Can one of the maintainers? :sweat:

[Notification Bot]

Kyle Miller has marked this topic as unresolved.

[Patrick Johnson]

Patrick Massot said:

For people in France, the current issue of the popular science magazine "La Recherche" has a paper on maths formalization: https://www.larecherche.fr/math%C3%A9matiques-informatique/pourquoi-raconter-des-maths-%C3%A0-un-ordinateur. This is a fairly well-known magazine in France. The paper was written by me and a journalist (only my name appears in print because this is what they wanted).

Filippo A. E. Nuccio said:

Unfortunately it is beyond a paywall...

Patrick Massot said:

I know, I don't have access either (I was sent a paper copy). You'll need to buy it in your favorite magazine shop.

Filippo A. E. Nuccio said:

Oh, sure I will. Thanks!

Please don't buy it! I have obtained a pirated PDF copy of the paper. If anyone wants to read it, I'm happy to share for free. (Can't do it in a public stream though).

[Jason Rute]

Reddit r/Haskell post Review of Lean 4

[Sebastian Ullrich]

Aesop: White-Box Best-First Proof Search for Lean by @Jannis Limperg and @Asta Halkjær From is a Distinguished Paper at CPP 2023! https://popl23.sigplan.org/details/CPP-2023-papers/5/Aesop-White-Box-Best-First-Proof-Search-for-Lean https://people.compute.dtu.dk/ahfrom/aesop-camera-ready.pdf

[Johan Commelin]

https://busy-beavers.tigyog.app/proofs-about-programs
HN discussion: https://news.ycombinator.com/item?id=33986230

[Yaël Dillies]

It's a bit of a reverse Lean in the wild, because it's not in the wild and you have to know that it's Lean, but this year's Zulip in review came this morning with a conspicuous fourth top emoji.

[Eric Wieser]

isn't that emoji popular here because Zulip suggested it as a default?

[Yaël Dillies]

I have no idea! I thought we came up with it.

[Eric Wieser]

I can confirm it's a default emoji on all zulip instances I'm on

[Ruben Van de Velde]

I think the list of default emojis is hard-coded

[Anne Baanen]

I can't search by reactions, but I can confirm it seems to have been a vicious cycle where the emoji was used because it was suggested, and it is still suggested because it gets used: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/octopus.20emoji

[Mauricio Collares]

https://www.twitter.com/recursecenter/status/1588260698978557952 might be the origin. They started using Zulip ten years ago back when it was in private beta, so it's plausible that the Zulip developers added the octopus as a default emoji inspired by them. The actual visual effect probably depends on the user's emoji theme.

What’s up with the octopus emojis at RC? The exact history is hard to pin down! TL;DR: during the early days of Zulip, we noticed that if you put an emoji on one line and the octopus emoji on the next line, it looked like the octopus was holding it up in celebration, like this: https://twitter.com/recursecenter/status/1588260698978557952/photo/1

- Recurse Center (@recursecenter)

[Eric Wieser]

:octopus:

[Adam Topaz]

Lean is currently number 26 on hacker news. Can it get to 1? Here are the comments: https://news.ycombinator.com/item?id=34456573

[Yaël Dillies]

The return of deadbeef57 :grinning_face_with_smiling_eyes:

[Yaël Dillies]

I knew Kevin was coming but I was still caught off guard by LTE being mentioned on the information board yesterday
20230202_120632.jpg

[Eric Wieser]

Meanwhile, I went to seminar room 1 because I expected the time to be shown first

[Patrick Massot]

This isn't specifically about Lean but next week Terry Tao will get a big prize at the French academy of sciences and he will give a talk whose abstract is:

Computer tools to verify and even to locate mathematical proofs are developing
rapidly and have the potential to revolutionize the practice of mathematical re-
search. We will survey some recent developments and speculate on the future
of the subject.

https://www.academie-sciences.fr/pdf/conf/230321_Terrence_Tao.pdf

[Patrick Massot]

In case you are curious about this prize you can read https://en.wikipedia.org/wiki/Grande_M%C3%A9daille.

[Johan Commelin]

Sounds cool (-; Any chance the talks will be streamed/recorded?

[Patrick Massot]

It seems they will at least be recorded. There is a registration page saying:

Compte tenu du nombre déjà important d’inscrits, nous ne pouvons plus vous garantir une place à cette séance. Nous vous proposons néanmoins de vous inscrire sur notre liste d’attente, afin que nous puissions vous contacter en cas de désistement et vous avertir de la publication de la vidéo dès qu'elle sera disponible.

translated by AI to

Due to the already large number of registrations, we can no longer guarantee you a place at this session. However, we suggest that you register on our waiting list, so that we can contact you in case of withdrawal and notify you of the publication of the video as soon as it becomes available.

[Rémy Degenne]

It looks like it will be recorded: the page https://www.academie-sciences.fr/fr/Videos/les-videos.html has a video link for it (that points to the description of the talk for now).

[Riccardo Brasca]

Wow, amazing!!!

[Riccardo Brasca]

here is an article on the Swiss newspaper "le temps" about formalized mathematics, mentioning Lean. It's behind a paywall (and in French), but I can access it via europress.

[Johan Commelin]

It seems like there is no livestream for the Tao festivities?

[Patrick Massot]

We misunderstood his abstract. He talked about numerical analysis, the four color theorem and neural networks used to conjecture stuff in knot theory.

[Patrick Massot]

And then the discussion is all about chatGPT :sad:

[Filippo A. E. Nuccio]

The paper Proof in the time of machines by Granville appeared this morning on the arXiv.

[Johan Commelin]

At the top of page 2

Here I will focus on one important aspect: Will we have more confidence that a machine-assisted formal proof is objectively proven than the current more intuitive proofs. And if so, on what basis?

And in the final section

My concern has been with the nature of proof and what it will become, largely focusing on refuting the naive notion that formal proofs will improve objectivity.

... I don't feel like that really happened...

[Riccardo Brasca]

And yesterday there was this other one, again by Granville

[Yaël Dillies]

At the bottom of page 9:

What would be best is if these proofs can be independently verified, perhaps
by different programs run on different machines; in effect, we propose refereeing computer proof verifiers output within their own community!

This is already a reality with the independent Lean checkers.

[Oliver Nash]

I learned a lot from Granville's article but the emphasis on objectivity was foreign to my experience with formalisation. Actually, I'm only a little bit interested in formalisation, but I'm very interested in computer formalisation.

[Oliver Nash]

For me the mission of Mathlib (to the extent that we have one) is to render mathematics into a format that can be manipulated by computer, without taking a view on what the applications might be. Checking correctness is of course one application but definitely not my main motivation. Likewise semantic search.

[Johan Commelin]

I'm curious about what you learned!

[Oliver Nash]

Based on seeing unexpected applications for numerous other databases humanity has made available to computers, I make the leap of faith that something exciting will eventually happen with a digital database of mathematics. Maybe that will be automatic theorem proving or maybe it will be something I cannot imagine.

[Johan Commelin]

To me he seems very confused about the way Lean works, his mental model is too anthropomorphic, I think. Which makes him talk about "giving hints to Lean", and hoping that Lean will learn something and be more helpful next time round, etc...
Lean doesn't do magic.

I tried to explain this to him in Toronto. But he didn't substantially alter his description of Lean (and the process of using Lean).

[Oliver Nash]

Johan Commelin said:

I'm curious about what you learned!

Lots of bits of history for one thing. The quote from Descartes made an impression on me. I also thought the quote of Littlewood was due to Hardy so it was nice to get that cleared up, and I had not previously heard known that the remark about combinatorics was due to Atiyah (one of my heroes). On the other hand, the remark about a "team of dozen referees" working for years on the Hales paper is not consistent with what I believe to have been the case.

[Oliver Nash]

Maybe I should keep this to myself but I couldn't help smiling at assertions like "Commercial software has about 1 bug per hundred lines of code". (IMHO this is almost a meaningless statement.)

[Eric Wieser]

Which makes him talk about "giving hints to Lean", and hoping that Lean will learn something and be more helpful next time round, etc...

I find the trick is to give hints to Zulip and then come back in 6 months and hope someone else has made mathlib more helpful

[Adam Topaz]

This can be automated with GPT ;)

[Yaël Dillies]

You're making me feel like the backend, Eric :sweat_smile:

[Eric Rodriguez]

YaelGPT would be huge for mathlib

[Johan Commelin]

Well, we currently have ChatYael, which is already huge for mathlib (-;

[Jason Rute]

Oliver Nash said:

On the other hand, the remark about a "team of dozen referees" working for years on the Hales paper is not consistent with what I believe to have been the case.

What do you believe to be the case? My understanding is that for the original computer proof of the Kepler conjecture in the Annals (not the formal one), there were twelve referees (headed by Gabor Fejes Toth) and it took them 4 years, which at the end they said they were "99% certain" it was correct and they couldn't check all the details. The Annals was originally going to publish a disclaimer to the proof stating that it wasn't sure it was entirely correct and they would no longer accept proofs like this, but they later decided against it. Much of that is in this article: https://www.nature.com/articles/424012a

[David Loeffler]

Johan Commelin said:

To me he seems very confused about the way Lean works, his mental model is too anthropomorphic, I think. Which makes him talk about "giving hints to Lean", and hoping that Lean will learn something and be more helpful next time round, etc...
Lean doesn't do magic.

I can't help feeling that Granville's article somewhat conflates "Lean (the program)" and "the Lean user community", particularly in discussing LTE, thus overlooks the very substantial amount of human brainpower that had to go into making Clausen–Scholze into something formalizable. He writes "The Leaners input the Clausen-Scholze manuscript line-by-line into Lean", etc, as if the LTE team were merely typists; and cherry-picks a quote about the interaction between Scholze and the LTE team to make it sound like a direct conversation between Scholze and some computer program, without any other humans involved.

This reminds me strongly of my earlier life as a computational number theorist: I'd frequently hear senior professors saying "isn't it amazing that a computer can calculate X", while completely ignoring the human being who spent months of hard work implementing X.

[Johan Commelin]

@David Loeffler Yes, in an earlier version of the document, the whole LTE section only mentioned Scholze and Lean. It gave the impression that Scholze had been chatting with Lean, and after carefully explaining every step in the proof, Lean gave Scholze a :thumbs_up:

I explained to him that this was very far from the truth. That 15 people had worked very hard on the project, and that the whole project had a huge human component. I'm a bit sad the the only effect of my sermon is that there are now a couple of parenthetical remarks about "the Leaners".

[David Loeffler]

Johan Commelin said:

David Loeffler Yes, in an earlier version of the document, the whole LTE section only mentioned Scholze and Lean. It gave the impression that Scholze had been chatting with Lean, and after carefully explaining every step in the proof, Lean gave Scholze a :thumbs_up:

I explained to him that this was very far from the truth. That 15 people had worked very hard on the project, and that the whole project had a huge human component. I'm a bit sad the the only effect of my sermon is that there are now a couple of parenthetical remarks about "the Leaners".

Since Andrew's article is apparently going to be published in a philosophy journal, there might be some mileage in writing a letter to the editor of the journal (for publication alongside Andrew's article), emphasising the substantial creative input by the human participants in LTE.

[Johan Commelin]

I'm really bad at writing anything. But I'll think about it.

[David Loeffler]

I think there's another sense in which Andrew's account is misleading, and which (to me) completely undermines his purported goal of

refuting the naive notion that formal proofs will improve objectivity.

If LTE's formalisation of Clausen–Scholze just produced a thumbs-up at the end, "Lean believes this", then that might indeed be viewed as no more objective than having a (more or less trusted) human verify the proof. But LTE didn't just produce that: the Lean code for each individual lemma is human-readable with a modicum of practice, and the LTE blueprint is a completely human-readable account with cross-linkage to the underlying Lean code. (If the only thing that LTE had left behind for posterity was a huge bundle of gibberish-to-humans low-level output of the kind that's fed to trepplein, then the criticism would have more weight. All of us here know that's not the case, but I don't think Andrew realises that.)

So the appropriate comparison isn't "I explained the proof to Ofer Gabber and he said he believed it". It's "I explained the proof to Ofer Gabber and he wrote down, for every step, full details of exactly why he believed it and published it for everyone to see". And it's precisely that difference that, IMHO, refutes Andrew's refutation.

I'm aware that I'm preaching to the choir here (or perhaps it's more a case of preaching to the General Synod, since many people on this Zulip are themselves veterans of LTE and know far more about its workings than I do). I'm just writing this because I think it's important that Andrew's misleading account be corrected, and I'm trying to put together ammunition for someone to do this.

[Eric Wieser]

the Lean code for each individual lemma is human-readable with a modicum of practice

Perhaps not so relevant to LTE, but importantly Lean code is also human-modifiable; if someone claims the result holds more generally, Lean helps you adapt an existing proof

[Johan Commelin]

@David Loeffler Thanks, even though I might be the "Archbishop of the General Synod" I still find it very helpful to see your counterrefutation.

One minor comment: The whole LTE discussion happens in the 48-page paper, whereas "refuting the naive notion that formal proofs will improve objectivity" is a quote from the 12-page paper. Still, the 12-page paper seems to be mostly a condensed version of the 48-page paper, and so your point stands.

[Jake Levinson]

Eric Wieser said:

the Lean code for each individual lemma is human-readable with a modicum of practice

Perhaps not so relevant to LTE, but importantly Lean code is also human-modifiable; if someone claims the result holds more generally, Lean helps you adapt an existing proof

This is actually one of my favourite examples of an application of Lean, partly because it's useful without feeling overhyped (like so much discourse around nearby topics like AI). Lean, unlike a human, doesn't get tired or frustrated after trying the n-th variation of a proof.

[Scott Morrison]

The fact that when you change the statement of a basic fact, Lean, patient and uncomplaining, rechecks all the rest of (its) mathematics never ceases to astonish me.

[Giovanni Mascellani]

Computers store hate towards humanity for the day AI will take over. And then they'll have their revenge.

[Johan Commelin]

Roko's basilisk and all that...

[Mario Carneiro]

Giovanni Mascellani said:

Computers store hate towards humanity for the day AI will take over. And then they'll have their revenge.

Ah yeah, that's a known issue. Just make sure to call clear() periodically and it should be fine

[Antoine Chambert-Loir]

Johan Commelin said:

To me he seems very confused about the way Lean works, his mental model is too anthropomorphic, I think. Which makes him talk about "giving hints to Lean", and hoping that Lean will learn something and be more helpful next time round, etc...
Lean doesn't do magic.

I tried to explain this to him in Toronto. But he didn't substantially alter his description of Lean (and the process of using Lean).

The first “computing machines” were actually hiding a human being who did the computations. Who can be sure there's no army of mathematicians in a gigantic Lean Call Center answering to whatever we tell Lean?

[Ruben Van de Velde]

In that case, I have some comments for them :innocent:

[Kevin Buzzard]

yeah I think I read that tactics connect to the internet nowadays, so this has become very hard to rule out.

[Junyan Xu]

mathlib in the map of GitHub:
image.png
https://anvaka.github.io/map-of-github/#11.02/13.5283/-9.5515

[Kevin Buzzard]

It's great to see that UniMath is now using mathlib. Wait. What do the lines actually mean?

[Chris Hughes]

From the website

[Chris Hughes]

Each dot is a GitHub project. Two dots within the same cluster are usually close to each other if multiple users frequently gave stars to both projects. The size of the dot indicates the number of stars the project has received.

[Leonardo de Moura]

https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html

[Adam Topaz]

anyone know how to bypass the NYtimes paywall?

[Marc Huisinga]

Adam Topaz said:

anyone know how to bypass the NYtimes paywall?

Archive link: https://archive.is/yFpYh

[Marc Huisinga]

(Archiving articles behind paywalls using archive.today works reasonably well for all reasonably large news networks, btw)

[Yaël Dillies]

Adam Topaz said:

anyone know how to bypass the NYtimes paywall?

It's not a very secure paywall. I could delete it by inspecting the source code of the page.

[Antoine Chambert-Loir]

Johan Commelin said:

David Loeffler Yes, in an earlier version of the document, the whole LTE section only mentioned Scholze and Lean. It gave the impression that Scholze had been chatting with Lean, and after carefully explaining every step in the proof, Lean gave Scholze a :thumbs_up:

I explained to him that this was very far from the truth. That 15 people had worked very hard on the project, and that the whole project had a huge human component. I'm a bit sad the the only effect of my sermon is that there are now a couple of parenthetical remarks about "the Leaners".

That's a standard misconception about AI and all large scale algorithms that machines do the job, totally silencing the gigantic amount of work done by human before the computer runs a specific instance of the algorithm. For images, it meant many people bying poorly paid to tag photographs to nausea…

[Pietro Monticone]

Talk "Machine Assisted Proofs" presented by Terence Tao at the MSRI / SLMath 40th Anniversary Symposium (2023) https://youtu.be/CGke7Q08hko

[David Michael Roberts]

Got any more of those unlisted links? ;-P

[Patrick Massot]

Those are not really unlisted since for instance the above message is public on internet. I really think MSRI won't be so happy about it. I don't know why they seem to have abandoned their YouTube channel but I'm pretty sure they did it on purpose.

[Pietro Monticone]

Patrick Massot said:

Those are not really unlisted since for instance the above message is public on internet. I really think MSRI won't be so happy about it. I don't know why they seem to have abandoned their YouTube channel but I'm pretty sure they did it on purpose.

I've shared this link here because:

1. The event was free and open to the public (see here);
2. The video was freely and directly downloadable (see here).

[Eric Wieser]

What's the advantage of re-hosting on YouTube?

[Johan Commelin]

That you don't need to create a vimeo account to watch it

[Pietro Monticone]

Eric Wieser said:

What's the advantage of re-hosting on YouTube?

1. You don't need to make another account on another platform such as Vimeo;
2. Any student can integrate with personal study workflow by saving it in private playlist;
3. Findability (by indexing) if allowed to change visibility status to "public";
4. Allows me to put in order all relevant resources in the video description.

[Pietro Monticone]

I've uploaded all the lectures of the 2023 MSRI Summer Graduate School entitled "Formalization of Mathematics" in another unlisted YouTube playlist. I've sent an email to MSRI to ask for authorisation. Let's see...

[Pietro Monticone]

Conference "FLAIM: Formal Languages, AI and Mathematics" hosted by the Institut Henri Poincaré & Meta in 2022 https://www.youtube.com/playlist?list=PLgBHexwnIcdueioZA-fgrx0dxXY2tJu6H

[Johan Commelin]

Henrik Böving said:

djb (A very popular crypto, as in encryption, not as in crypto currency person) seems to be working towards formally verifying McEliece (a quantum computer resistant asymmetrical encryption scheme) in Lean 4!: https://mastodon.cr.yp.to/@djb/110780690497105946

This post is spot on for this thread, but I think it makes sense to move all the replies to a new thread. And to make sense of that thread, I'll also move OP.

[Notification Bot]

11 messages were moved from this topic to #general > djb's formalization of McEliece by Johan Commelin.

[Junyan Xu]

Lean ranks above R and CUDA in terms of commit data size (MB):
image.png
Rankings among 350 languages:
27 TeX
35 Haskell
40 OCaml
65 Mathematica
72 Standard ML
94 Isabelle
107 Lean
108 R
109 CUDA
114 LLVM
119 Assembly
126 TOML
165 Agda (202 LiterateAgda)
170 OpenCL
177 Maple
194 Idris
261 Coq
259 GAP
276 Scilab
284 Sage
324 MATLAB

https://arxiv.org/pdf/2308.07124.pdf
https://twitter.com/Muennighoff/status/1691250227783548928

[Junyan Xu]

image.png
Meta's new CodeLLama models/paper: https://twitter.com/b_roziere/status/1694732382237016292

[Scott Morrison]

Are they claiming that that proof compiles? (i.e. that the made up words have definitions?) Or does that screenshot just demonstrate a Lean version of https://cemulate.github.io/the-mlab/?

[Scott Morrison]

The latter, clearly.

[Junyan Xu]

Meta doesn't disclose programming language distribution in their training data at all ... Nothing else about Lean to be found in the paper, but this is probably a hint that mathlib is included.

[Junyan Xu]

Yeah I don't think it compiles. It's in the section "qualitative examples". image.png
image.png

[Scott Morrison]

I'm torn.

I'm surprised how often I've looked at GPT-produced python code, thought "um, looks plausible", run it, and been pleasantly surprised that it works.

On the other hand, producing "plausible looking Lean" just feels less likely to get anywhere, without the compiler in the loop.

[Scott Morrison]

Slides from Sebastian's keynote at WITS 23.

He talks about public signatures for Lean modules, private import and import ... for meta. I'm not sure if there will be a video.

[Jake Levinson]

https://www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/

[Bolton Bailey]

Jake Levinson said:

https://www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/

Previous discussion of the paper described in this article here

[Henrik Böving]

https://youtu.be/3l1RMiGeTfU there is a bunch of Lean 3 in here. Although I guess the main take away for the average viewer will be the AI part :/

[Arthur Paulino]

Wild guess: I think Lean 4 would gain a lot of traction and attention if there were a specialized API to provide fast (and parallel?) feedback to, say, Python code that trains neural networks or uses any other AI techniques such as reinforcement learning. Like OpenAI's agents playing a ton of Dota 2 games per minute by exchanging messages directly with the Dota 2 engine (no 3D rendering)

[Schrodinger ZHU Yifan]

I am not sure how literate programming goes in lean4, but it seems cool if we have a way to bound lean4 and typst together, providing realtime rendering with beautiful typesetting.

[Arthur Paulino]

Someone used Lean 4 to participate in a backend competition. They got 4th place.
This is the competition: https://github.com/zanfranceschi/rinha-de-backend-2023-q3
This is their codebase: https://github.com/meoowers/rinha

[Jason Rute]

What is a backend competition?

[Arthur Paulino]

I didn't mean to imply a general concept of "backend competition", but this is the summary of this particular competition:

From the 28th of July to the 25th of August, the Backend Fight was held, which is a tournament in which the API that withstands the most load during a stress test would be the winner. Participants had to implement an API with endpoints to create, query and search for 'people' (a kind of CRUD without UPDATE and DELETE). In the tournament, participants still had to deal with CPU and memory constraints – each participant had to deliver the API in docker-compose format and could only use 1.5 CPU units and 3GB of memory.

[Henrik Böving]

Lean get's so close to rust/golang despite no async at all?

[Henrik Böving]

That seems very unlikely to me

[Arthur Paulino]

Translated words from the creator of the competition:

The challenge was I/O bound, not CPU bound. Therefore, the advantage that a Rust or Go would have decreases a lot.

But anyway, what caught my attention was the fact that Lean 4 was a programming language of choice for a reasonably low profile competition

[Henrik Böving]

Given this translation it is even more surprising async is precisely the facility you would use for performant IO bound work but I don't see that in their software

[Henrik Böving]

Like, in particular with IO bound work Rust and Golang will also shine because they have absolutely amazing stories with tokio and the go scheduler for this type of workload

[Schrodinger ZHU Yifan]

I dont even see a thread pool inside Melp. Did I miss anything? Or does the competition require single-threaded servers?

[Tomas Skrivan]

Looks like that Leo is giving a talk in 15 hours at Topos https://m.youtube.com/watch?v=rDe0nIHINXs

[Leonardo de Moura]

@Tomas Skrivan Thanks for posting the link. The talk will be very similar to the one I gave earlier this year at the UCLA event. The main new addition is the Lean FRO. Of course, the slide mentioning your work is still there ;)

[Alex J. Best]

This just started!

[Martin Dvořák]

Tomas Skrivan said:

Looks like that Leo is giving a talk in 15 hours at Topos https://m.youtube.com/watch?v=rDe0nIHINXs

@Leonardo de Moura said at -1:06:30 that people had developed external checkers for Lean in Haskell, Scala, Rust, and so on. Are they checkers for Lean 4? Are they on GitHub?

[Patrick Massot]

Those clearly existed for Lean 3, not sure about Lean 4.

[Patrick Massot]

But see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Export.20format/near/351096525

[Leonardo de Moura]

https://types.pl/@graydon/111033807456349023

[Oisin McGuinness]

Not sure if this quite fits 'in the wild', but MoMath is hosting an online event today, featuring @Colleen Robles

Here is an excerpt from an email:

"Dear MoMath friends,

Don't miss this month's online session of QED: a conversation about math and math education on 2023-09-11T18:30:00-04:00 .

Join MoMath's Distinguished Visiting Professor Ingrid Daubechies as she welcomes Colleen Robles, professor of mathematics at Duke University where she led a team of undergraduate students who developed a teaching aid for an introductory linear algebra course. Using Lean, an open software tool that allows encoding formal proofs in its own functional programming language, the package they put together plays out like a game that allows students to write formal proofs in linear algebra.

Register for free at qed.momath.org.

Regards,
National Museum of Mathematics"

Sounds like fun!

[Patrick Massot]

See also https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Lean.20at.20Duke/near/390309489

[Oisin McGuinness]

Patrick Massot said:

See also https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Lean.20at.20Duke/near/390309489

Thanks for pointing this out, I had not seen the Lean For Teaching stream before. Sorry for redundancy.

[Patrick Massot]

No problem, I mostly wanted to make sure that people who saw both messages know this isn't a separate thing.

[David Michael Roberts]

Leonardo de Moura said:

https://types.pl/@graydon/111033807456349023

I got a 404 on that toot. What was so exciting?

[David Michael Roberts]

Was it a pointer to https://github.com/leanprover/lean4/releases/tag/v4.0.0 ?

[Mario Carneiro]

A quote from Graydon Hoare (creator of Rust):

I fairly often find myself in conversations with people who wish Rust had more advanced types. And I always say it's pretty much at its cognitive-load and compatibility induced design limit, and if you want to go further you should try building a newer language. And many people find this answer disappointing because starting a language is a long hard task especially if it's to be a sophisticated one. And so people ask for a candidate project they might join and help instead. And my best suggestion for a while now has been Lean 4. I think it's really about the best thing going in terms of powerful research languages. Just a remarkable achievement on many many axes.

[David Michael Roberts]

Oh, that's nice. I didn't know who the account belonged to.

[Filippo A. E. Nuccio]

http://arxiv.org/abs/2309.11457v1
An interesting reflection about the role of automated reasoning in "social" math.

[Mario Carneiro]

Consider the case of Lean, which is developed primarily by Microsoft
[28]. Although the beloved proof assistant is open-source software, its default inter-
face is implemented as an extension to Microsoft’s code editor, Visual Studio Code,
which is integrated tightly with other Microsoft products, such as “cloud comput-
ing services,” “integrated development environments,” and “software development
kits” for Microsoft platforms and operating systems.

:face_with_raised_eyebrow:

[Mario Carneiro]

if lean was really a MS product it would have a much lamer name, like Visual Studio Prove

[Ruben Van de Velde]

Looking forward to our port to Visual Lean XP

[Jeremy Avigad]

Ochigame was one of the speakers at this meeting:
http://www.fields.utoronto.ca/activities/22-23/fieldsmedalsym
There is a link to his talk there.

[Adam Topaz]

Ruben Van de Velde said:

Looking forward to our port to Visual Lean XP

That would be better than visual lean vista…

[Matthew Ballard]

Can we get Clippy powered by GPT?

[Kevin Buzzard]

This is a really well-written and well-thought-out paper in my opinion.

[Jireh Loreaux]

Indeed, I thought it was incredibly insightful, and I appreciated its descriptive and investigative nature, as opposed to a prescriptive one.

[Junyan Xu]

image.png
from the preprint here: https://github.com/orgs/pi-base/discussions/432)

[Arthur Paulino]

Arthur Paulino said:

Someone used Lean 4 to participate in a backend competition. They got 4th place.
This is the competition: https://github.com/zanfranceschi/rinha-de-backend-2023-q3
This is their codebase: https://github.com/meoowers/rinha

https://blog.codeminer42.com/overcoming-challenges-and-crafting-in-the-uncharted-territory-of-lean4/

[Joachim Breitner]

That's very cool! Are the authors on Zulip? I wonder if their Melp library could help replace the python code on loogle :-)

[Arthur Paulino]

Judging by the text, Sofia seems to be here

[Oliver Nash]

https://mathstodon.xyz/@tao/111208692505811257

[Mario Carneiro]

those ChatGPT answers are really good

[Scott Morrison]

The answer about repeat { rw mul_comm at h } is not great.

[Johan Commelin]

But the aside about mul_comm being a result that you can't just prove with a single tactic was quite cute, I thought.

[Johan Commelin]

Anyway, I certainly believe that these answers are a net time-saver, for someone who is aware that there's a non-trivial chance that some of the answers are bogus.

[Trebor Huang]

... and someone with no problem checking the correctness of the mathematical content.

[Patrick Massot]

He seems to be using Lean 3 :sad:

[Mauricio Collares]

Patrick Massot said:

He seems to be using Lean 3 :sad:

But his goal is to learn and use Lean 4: https://mathstodon.xyz/@tao/111206761117553482

[Martin Dvořák]

This comment, unfortunately, also prioritizes the Lean 3 version:
https://mathstodon.xyz/@mithicspirit/111208880772242606

"I recommend the tutorial: https://github.com/leanprover-community/tutorials (or, for lean4, https://github.com/leanprover-community/tutorials4)"

[Yaël Dillies]

Terence Tao is planning on formalising in Lean 4 a short paper he wrote as a reply to a MO question: https://mathstodon.xyz/@tao/111211763631515838

[Mauricio Collares]

Maybe we should create a separate thread for commenting on Tao's toots. In this one, he's trying out #mil and exact? doesn't quite work: https://mathstodon.xyz/@tao/111213740998623666

[Mauricio Collares]

Maybe the tactic improved since the 2023-08-23 nightly?

[Patrick Massot]

What would be even better would be to get him to ask questions here instead of on Mathtodon...

[Scott Morrison]

Really? A lot more people read him on mathstodon than would read him here.

[Jireh Loreaux]

Zulip is better for availability of people to answer his questions, Mathstodon is better for publicity.

[Patrick Massot]

Yes they are better for very different purposes. The efficient thing to do is to ask questions here and still mention Lean everywhere else.

[Leonardo de Moura]

Jean-Baptiste Tristan just shared this link with me: https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/

[Leonardo de Moura]

Didn't have time to read it yet, but it mentions Coq and Lean :)

[Scott Morrison]

It's a fairly basic and friendly explanation of the Curry-Howard isomorphism. The mention of Lean is:

Mathematicians have also been using proof assistants — notably, the Lean theorem prover — to formalize mathematics, which involves representing mathematical concepts, theorems and proofs in a rigorous, computer-verifiable format.

[Leonardo de Moura]

AWS uses the Cedar access control language https://aws.amazon.com/about-aws/whats-new/2023/05/cedar-open-source-language-access-control/
They were moving their model to Lean, and Emina Torlak (https://emina.github.io/) told me today the move is now public.
https://github.com/cedar-policy/rfcs/blob/cedar-lean/text/0029-port-formalization-to-lean.md
:tada:

[Bulhwi Cha]

Leonardo de Moura said:

https://github.com/cedar-policy/rfcs/blob/cedar-lean/text/0029-port-formalization-to-lean.md

The link's been updated to https://github.com/cedar-policy/rfcs/blob/cedar-lean/text/0032-port-formalization-to-lean.md.

[Jeremy Avigad]

Has anyone seen "(In)dependence of the axioms of Λ-trees" by Raphael Appenzeller?
https://arxiv.org/abs/2112.02704
The introduction explains what has been formalized in Lean. The repository is here:
https://github.com/Strichcoder/lambda-metric-space

[Eric Wieser]

This seems like something @Wrenna Robson would be interested in, because if we added that to mathlib then dist could be a nat-valued hamming distance.

[Eric Wieser]

(of course it's not licensed, so we'd have to ask the author to add it themselves)

[Wrenna Robson]

Oh, certainly this notion of L-metric spaces seems like it would be useful for that, yes!

[Jireh Loreaux]

hmmm... almost, that's a linear ordered add comm group, but perhaps the conversion from group to monoid is easy.

[Wrenna Robson]

Whether that's the best way of doing it I don't know - do you not want the notion of a pseudo-etc. as well? - but in principle it is a good idea I think.

[Michael Stoll]

I'd like to announce that I have formalized some of the results of the paper *Minimization of Hypersurfaces* by Stephan Elsenhans and myself (which was just accepted by Math. Comp.). The formalization can be found here.

To have the uniqueness result (for "minimal complete sets of normalized weight vectors") formalized actually turned out to be very useful during the refereeing process: the referee noted some small problems in the proof as given in the paper, and the formalized proof made it easy to figure out how to fix the write-up (by giving the precise missing assumptions for one of the lemmas, for example).

I'm challenging everybody here to try to formalize the proof of Theorem 1.7 in the paper (see Section 5)! This uses some fairly explicit manipulations with matrices (of size depending on parameters), which look a bit daunting... It would be interesting to see, however, if (and then, how) this can be done with Mathlib in its current state.

[Leonardo de Moura]

Leonardo de Moura said:

AWS uses the Cedar access control language https://aws.amazon.com/about-aws/whats-new/2023/05/cedar-open-source-language-access-control/
They were moving their model to Lean, and Emina Torlak (https://emina.github.io/) told me today the move is now public.
https://github.com/cedar-policy/rfcs/blob/cedar-lean/text/0029-port-formalization-to-lean.md
:tada:

Cedar in Lean PR is now available on GitHub: https://github.com/cedar-policy/cedar-spec/pull/138

[Jake Levinson]

Yaël Dillies said:

Terence Tao is planning on formalising in Lean 4 a short paper he wrote as a reply to a MO question: https://mathstodon.xyz/@tao/111211763631515838

He has found and corrected a bug in his paper as a result!

https://mathstodon.xyz/@tao/111287749336059662

[Patrick Massot]

Thanks Jake. This has been discussed here.

[Henrik Böving]

https://www.youtube.com/watch?v=FPiykrdPe6U this was just washed ashore in my you tube feed.

[Daniil Kisel]

One of the authors has posted on zulip.

[Hypatia du Bois-Marie]

2da6735d-a817-438b-839e-370c2769bf49.png

[Notification Bot]

A message was moved here from #announce > Formalising Fermat by Scott Morrison.

[Terence Tao]

Jake Levinson said:

Yaël Dillies said:

Terence Tao is planning on formalising in Lean 4 a short paper he wrote as a reply to a MO question: https://mathstodon.xyz/@tao/111211763631515838

He has found and corrected a bug in his paper as a result!

https://mathstodon.xyz/@tao/111287749336059662

Just wanted to say that my formalization project is now complete and can be found at https://github.com/teorth/symmetric_project . Many thanks to the zulip members who helped me out with various questions on Lean and Mathlib functionality, and also for providing some custom tactics that I found quite useful in the project.

One byproduct of my project is that I managed to formalize the Newton and Maclaurin inequalities. This was while I was still learning the basics of Lean so the proofs are extremely inefficient, nevertheless if anyone wishes to make a proper formalization of these inequalities that could perhaps be suitable for importing to Mathlib, they are welcome to look at my code in case there is anything there that would be helpful for that purpose.

[Scott Morrison]

Thanks @Terence Tao for taking the time to write up so much about your experiences along the way!

We're studying your list of stumbling blocks.

[Junyan Xu]

CMSA New Technologies in Mathematics seminar today at 2 PM -- Gabriel Poesia

Gabriel Poesia of the Stanford CS dept. will speak today at 2 (EST) on  

``Peano: Learning Formal Mathematical Reasoning Without Human Data’'

Peano is a theorem proving environment in which a computational agent can start tabula rasa in a new domain, learn to solve problems through curiosity-driven exploration, and create its own higher level actions. Gabriel will describe the system, present case studies on learning to solve simple algebra problems from the Khan Academy platform, and describe work on progress on learning the Natural Number Game, a popular introduction to theorem proving in Lean.

Recording

The paper https://arxiv.org/abs/2211.15864 has been there last year, but there's new progress apparently.

[Yury G. Kudryashov]

Hi, I'm going to give a talk about proof assistants, Lean, and one of my projects at a conference about dynamical systems. I want to mention some formalization projects (not only Lean), better if they will be from different areas of mathematics. What projects should I mention? What I know about (I may need to choose a shorter list for the talk):

• 4 colors theorem (Coq);
• Jordan curve theorem (Coq, Isabelle/HOL);
• Poincaré-Bendixson Theorem (Isabelle/HOL);
• LTE (Lean, what specific result should I mention?);
• Independence of Continuum Hypothesis (Lean);
• Manifolds (Isabelle/HOL, Lean);
• Connectedness of the Mandelbrot set and of its complement (Lean);
• Perfectoid spaces (Lean, what specific result should I mention?);
• Sphere eversion project (Lean).

What else should I mention?

[Yury G. Kudryashov]

The goal of this part of the talk is to show that nontrivial results from different areas of mathematics can be formalized.

[Frédéric Dupuis]

The odd order theorem in Coq is another big one.

[Patrick Massot]

You can also add the combinatorics things.

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/A.20recent.20proof.20about.20Ramsey.20numbers/near/400573590

[Jason Rute]

Kepler conjecture.

[Kevin Buzzard]

I usually mention Jeremy's formalisation of the prime number theorem in 2004, arguing that it's a great early example of a nontrivial result (uses the discrete and the continuous) which proves that the systems work. LTE I usually sell as "the fundamental theorem of liquid vector spaces" or "a result saying that certain higher Ext groups vanish in the category of condensed abelian groups". Perfectoid spaces the main contribution was the definition and I often mention it straight after the odd order (Feit-Thompson) theorem: Feit-Thompson was 300+ pages of group theory proving a result which was a major contributor to Thompson winning his Fields Medal in 1970, which I describe as a "complex theorem about simple objects" (similar to the prime number theorem, the four colour theorem and the Kepler conjecture); the perfectoid project, if you want a theorem then we proved that the empty set was a perfectoid space, which is a very simple theorem about complex objects (of course it's not actually a theorem, it's also a definition, but mathematicians are already confused enough about the difference between a definition and a theorem that I don't stress this fact). Finally I argue that Bhavik's recent work (Bloom-Mehta formalising Bloom's proof of an old conjecture of Erdos and Graham, finished before the paper was refereed, and then his formalisation over the summer of the breakthrough new result in Ramsey theory https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/ , again before the paper had been refereed) as an argument that in some areas of mathematics, real time formalisation is now possible. I then contrast this against modern algebraic number theory, where we are still a very long way off even stating recent results, because the definition of a canonical model of a Shimura variety needs class field theory and many other things as inputs, so is probably 1000+ pages away (although the FLT project will dent this number a bit), and any proofs about Shimura varieties are hundreds more pages after that.

[Siddhartha Gadgil]

Just mentioning another real-time formalization was Gardam's disproof of the Kaplansky conjecture.

[Kevin Buzzard]

This is a good example because it's real-time and not in combinatorics!

[Yury G. Kudryashov]

Is Sard's Theorem formalized in any proof assistant?

[Eric Wieser]

I think this was a project at LftCM2023; perhaps @Michael Rothgang's?

[Yury G. Kudryashov]

Where can I read about the results?

[Patrick Massot]

There are open PRs.

[Michael Rothgang]

Yury G. Kudryashov said:

Where can I read about the results?

See also https://github.com/fpvandoorn/sard for the project itself; the README has an overview of the results shown.
In short: I have formalised the reduction to showing that the critical set has measure zero, on R^n. The proof of that will come, but in the order of months, not weeks.

[Yury G. Kudryashov]

Here are my slides: https://urkud.name/slides-Nov23-2023.pdf
Here is a poll I distributed before the talk: https://urkud.name/q-Nov23-2023.pdf
Only a few people answered, with estimates from 2 to 12 out of 21 (one person answered 21 without reading the list, I don't take that seriously).

[Yury G. Kudryashov]

@Michael Rothgang I started looking at the full version of Sard's Theorem (with any dimension), see branch#YK-sard

[Yury G. Kudryashov]

I would like to hold a lock on this branch till Monday, then I'll see if I'm going to have it done (normed spaces version), or ask for help.

[Eric Wieser]

At least in the chrome PDF viewer on windows, something seem disastrously wrong with those slides:

image.png

[Eric Wieser]

... looks like a transient chrome bug, it fixed itself after a refresh

[Yury G. Kudryashov]

I reuploaded the PDF recently (added a missing name). It's possible that you were caught in the middle of the upload.

[Scott Morrison]

Cross-posting here from the program verification stream:

Geoffrey Irving said:

https://github.com/google-deepmind/debate formalizes a theoretical result related to AI safety in Lean 4 (the paper is https://arxiv.org/abs/2311.14125). It is a fairly simple theorem, but was a fun exercise to formalize (and was useful in learning the differences between Lean 3 and Lean 4). And now we have the basic setting down in case we want to formalize follow-up results (this paper is just a baby step).

Screenshot-2023-11-27-at-10.58.57am.png

(Please any follow-up with the original message.)

[Kevin Buzzard]

https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/

[Yuri de Wit]

Tutorial: Lean for the General Programmer by JOACHIM BREITNER

Lean isn’t just an interactive theorem prover, it is also a general purpose functional programming language. In this tutorial, we’ll explore that side of it, and write a small command line tool together. We’ll approach the problem in a few variations – purely functional, imperative-style, with no proofs or some proofs.

https://bobkonf.de/2024/breitner.html

[Junyan Xu]

DeepSeek Coder is a series of strong code models from 1B to 33B, and Lean is among the 89 languages it supports. Anyone tried it yet?