Zulip Chat Archive

Stream: general

Topic: Community blog

Patrick Massot (Sep 20 2021 at 21:23):

The mathlib maintainers team is proud to announce that we created a blog on the Lean community website. It will feature:

  • posts highlighting some new contributions to mathlib or papers
  • news about ongoing projects such as the Liquid tensor experiment or the sphere eversion project
  • news about exciting developments in other proofs assistants
  • announcements of conferences and talks
  • some explanations of specific topics in a less formal context than the documentations
  • speculations about future developments or somewhat philosophical discussions

There is no predefined list of authors. Everybody can submit a pull-request with a post. If you are unsure whether your post will be welcome then don't hesitate to first discuss the topic of your post on Zulip before investing too much time writing it. We wrote a couple of example posts, but we hope the community will write many more.

Kevin Buzzard (Sep 20 2021 at 21:55):

I like the idea of the "this month in mathlib" posts. I did a few of these on Twitter and they seemed to go down very well. My main problem with these was that I'd see something in #rss and want to tweet about it instantly but the PR wouldn't be in the docs yet and then I'd forget about it. Somehow the hardest thing to do is to make sure you mention all the cool stuff in the appropriate post

Patrick Massot (Oct 02 2021 at 07:49):

Don't miss the September version of this month in mathlib in the blog as well as a nice post about Radon-Nikodym that we forgot to announce here.

Kevin Buzzard (Oct 02 2021 at 08:32):

Oh nice -- I'd just commented on Twitter that I was looking forward to this :-)

Kevin Buzzard (Oct 02 2021 at 08:35):

"the class group of an integral closure is finite" is as it stands an incorrect or ambiguous statement. My memory is that what's going on is that finiteness of class group is preserved by integral closure.

Kevin Buzzard (Oct 02 2021 at 08:38):

@Anne Baanen @Filippo A. E. Nuccio have I got this straight?

Patrick Massot (Oct 02 2021 at 08:39):

You don't have to ask experts, this is all formalized!

Patrick Massot (Oct 02 2021 at 08:40):

docs#class_group.fintype_of_admissible_of_finite and docs#class_group.fintype_of_admissible_of_algebraic

Patrick Massot (Oct 02 2021 at 08:41):

you will need to read docs#absolute_value.is_admissible

Patrick Massot (Oct 02 2021 at 08:41):

But a better one sentence summary would be welcome.

Patrick Massot (Oct 02 2021 at 08:41):

Note that we will very soon have a full blog post about this.

Kevin Buzzard (Oct 02 2021 at 08:44):

My point is simply that it's not true that if A is some random ID then its integral closure in something is finite. In fact my memory is faulty because I think the integral closure of the PID C[X]\mathbb{C}[X] in the field of fractions of C[X,Y]/(Y2−X3−1)\mathbb{C}[X,Y]/(Y^2-X^3-1) is not finite

Kevin Buzzard (Oct 02 2021 at 08:47):

Oh that's right there's some weird assumption which happens to be satisfied in the global field case

Kevin Buzzard (Oct 02 2021 at 08:50):

Is "in the presence of an admissible absolute value, the class group of an integral closure is finite" too long/clunky? You can leave it if you like. But for me the current version reads very oddly because it's so obviously wrong. It would be like saying "culminating in a proof that the square of a function is continuous", the statement as it stands is so manifestly false that it's really hard to imagine what we really mean

Kevin Buzzard (Oct 02 2021 at 08:54):

Or you could just say "reduces the proof that the class group of a global field is finite to an admissibility assertion"

Patrick Massot (Oct 02 2021 at 08:56):

The second proposition came too late, I already pushed the first one

Kevin Buzzard (Oct 02 2021 at 08:56):

Or maybe just "the class group of a certain kind of integral closure is finite"

Kevin Buzzard (Oct 02 2021 at 08:57):

Ok the push is fine. Sorry for the noise.

Patrick Massot (Oct 02 2021 at 08:57):

No need to be sorry! Thanks!

Kevin Buzzard (Oct 02 2021 at 08:58):

Everything else looks great :-)

Kevin Buzzard (Oct 02 2021 at 09:01):

PS another observation is that my temporary mathematical confusion was resolved because somebody wrote docstrings for theorems rather than just for definitions. Thanks!

Patrick Massot (Nov 02 2021 at 17:07):

The blog has a new post listing ways LTE contributed to the theory of normed groups in mathlib.

Patrick Massot (Nov 04 2021 at 09:24):

Also don't miss this month in mathlib which has been published this morning but appears before the above post before it's dated from November 1st. It has been quite a productive month (see also our mathlib statistics page for raw quantitative information).

Kevin Buzzard (Nov 04 2021 at 15:48):

I just tweeted about the blog and it looks like this:

twitter.png

Is there a way of making it say some Lean logo (or even a mathlib logo!) instead of that "missing picture" icon?

Mario Carneiro (Nov 04 2021 at 15:55):

I think you want to follow the directions at https://developer.twitter.com/en/docs/twitter-for-websites/cards/overview/summary-card-with-large-image

Mario Carneiro (Nov 04 2021 at 15:55):

or, I guess that needs to be in the leanprover-community web site source

Rob Lewis (Nov 04 2021 at 15:56):

Yeah, on the docs pages we have in the header

    <meta name="twitter:card" content="summary">
    <meta name="twitter:title" content="algebra.algebra.basic - mathlib docs">
    <meta name="twitter:description" content="Algebras over commutative semirings. In this file we define `algebra`s over commutative (semi)rings, algebra homomorphisms `alghom`, and algebra equivalences `algequiv`. We also define the usual…">
    <meta name="twitter:image" content="https://leanprover-community.github.io/mathlib_docs/meta-twitter.png">

Rob Lewis (Nov 04 2021 at 15:56):

So idealy we'd have a blog version of https://leanprover-community.github.io/mathlib_docs/meta-twitter.png

Bryan Gin-ge Chen (Nov 04 2021 at 15:58):

There's also this open issue for the community website. If someone wants to make the images, the rest shouldn't be too hard.

Patrick Massot (Nov 22 2021 at 08:26):

On the community blog, don't miss Anne's blog post about mathlib's recent advances in number theory!

Patrick Massot (Dec 07 2021 at 08:47):

We're a bit late this month, but your wait is over: the community blog has its post on mathlib news from November!

Patrick Massot (Dec 11 2021 at 12:13):

We have a new blog post, by @Frédéric Dupuis, about the long awaited semi-linear map refactor, unlocking access to work in (bi)linear algebra over real and complex numbers in particular.

Patrick Massot (Dec 17 2021 at 08:54):

We're introducing a new category of blog post: backstage interviews with mathlib's active contributors, check out the first one!

Julian Külshammer (Dec 17 2021 at 10:00):

Great interview. Pleasure to read. Small style comment: Not all the questions are boldface.

Yaël Dillies (Dec 17 2021 at 10:02):

I think that's on purpose? The main questions should be bolded, and then came some discussion.

Yaël Dillies (Dec 17 2021 at 10:03):

Thanks again to the contributors for thinking I would be worth interviewing. That means a lot :hearts:

Yakov Pechersky (Dec 17 2021 at 13:31):

Thank you for the shoutouts!

Filippo A. E. Nuccio (Dec 17 2021 at 15:05):

Very nice, @Yaël Dillies !

Yaël Dillies (Dec 17 2021 at 16:53):

Yakov Pechersky said:

Thank you for the shoutouts!

You wholly deserve it! Wouldn't have embarked on the convexity refactor without you.

Arthur Paulino (Dec 17 2021 at 16:54):

I just read the interview and it was a great experience. Thanks for the effort put into it!

Patrick Massot (Dec 22 2021 at 14:29):

We have a new blog post, by @Scott Morrison: an Update on mathlib Lean 4 porting effort!

Mauricio Collares (Dec 22 2021 at 15:07):

This is a great post! It's perhaps too early to ask this, but will the final mathlib4 repo have the whole mathlib3 git history? This seems very tricky to get right but also a very worthwhile goal.

Mauricio Collares (Dec 22 2021 at 15:12):

I guess history preservation itself can be done after the fact (migrate to a history-less version, get the merged history to be perfect and then rewrite the repo once), but it at least ffects the choice of final repo location (/mathlib vs /mathlib4).

Johan Commelin (Dec 22 2021 at 15:59):

Please see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathport.20and.20git.20history/near/265814809 for a discussion about mathport and preserving git history from mathlib3 to mathlib4.

Arthur Paulino (Dec 22 2021 at 16:05):

Thanks again for the effort! This part was a highlight for me:

Porting missing tactics from mathlib3 to mathlib4. This is still a huge task, and will not be automated in any way. If you've contributed tactics to mathlib3, please consider trying to port them to Lean 4. If you're interested in learning some Lean 4 metaprogramming, what better way to do that than porting tactics? We'll write more about this in a future post, with some pointers about places to get started, and how to hook up new tactic implementations to the existing tactic parsers that Mario has already ported to mathlib4.

I will definitely try it when I feel more ready

Arthur Paulino (Dec 24 2021 at 04:01):

In the context of metaprogramming tactics, I'm finding these videos super helpful!

Patrick Massot (Dec 31 2021 at 21:20):

The last blog post for 2021 is an update about the Liquid Tensor Experiment!

Kevin Buzzard (Jan 01 2022 at 02:48):

@Johan Commelin You're not tempted to say far more explicitly "look we simplified the argument because we formalised it and it made us abstract the properties we needed"? People like de Jong proved great theorems in maths because they thought about what people were actually using when they were relying on resolution of singularities and then made a weaker construction which sufficed -- this was his big breakthrough. To say that a computer is helping us to do this is something which I think should be emphasized

Johan Commelin (Jan 01 2022 at 06:57):

@Kevin Buzzard You are right. But it's been a subtle interplay between me abstracting the properties we needed, and Scholze immediately recognizing that all the pieces fit together. Without his input, I don't think I would have connected the dots.
Lean forced me to do the abstraction, but it didn't help us with connecting the existing puzzle pieces when it comes to this Breen-Deligne lemma.

Johan Commelin (Jan 01 2022 at 06:59):

Where I see genuine help from Lean is in untangling the rest of the proof. That was one complicated tangle, and with Lean we managed to find a precise path through the maze. I wasn't able to find that path without Lean.

Johan Commelin (Jan 01 2022 at 06:59):

At some point in time, we should write down these findings in a careful way. Probably when we write a paper about the whole journey.

Patrick Massot (Jan 04 2022 at 21:58):

The traditional monthly recap is now available for December 2021!

Filippo A. E. Nuccio (Jan 05 2022 at 12:40):

Thanks, Patrick! I was not aware of @Anne Baanen 's work on #9888 and I find it really cool.

Johan Commelin (Jan 08 2022 at 19:40):

A summary/overview of what happened last year in the Lean community: 2021 - The Bottom Line

Yaël Dillies (Jan 08 2022 at 21:01):

Thanks for the shoutout!

Johan Commelin (Jan 31 2022 at 14:13):

The next backstage interview with Yakov Pechersky.

Yakov Pechersky (Jan 31 2022 at 14:18):

Thank you to the blog organizers for reaching out. It was such a fun experience to have a chat about mathlib. And in general, to reiterate what I said in the chat, huge thanks to the community in general.

Eric Taucher (Jan 31 2022 at 17:14):

From Yakov interview

In DNA, you know, DNA is replicated, and there's a 5' strand and a 3' strand. And DNA can really only get replicated in one direction by the replicating enzyme. So one of the strands, and it just goes through the enzyme and goes and goes and goes. And then the other one strand, it has to go forward, go back a little bit, go forward, go back a little bit. And so it has these fragments -- they are called Okazaki fragments. It's really cool that it does that.

If a picture is worth a thousand words a video is worth a million, enjoy. Mechanism of DNA Replication (Basic)

Patrick Massot (Feb 07 2022 at 07:10):

The traditional monthly recap is now available for January 2022!

Patrick Massot (Feb 12 2022 at 14:58):

Don't miss the wonderful story of mathlib's PR #10000 by Yury on the blog!

Filippo A. E. Nuccio (Feb 12 2022 at 17:00):

Great story, @Yury G. Kudryashov !

Jireh Loreaux (Feb 12 2022 at 20:16):

@Yury G. Kudryashov fascinating story, thanks for making Gelfand's formula possible!

Patrick Massot (Mar 07 2022 at 16:52):

The traditional monthly recap is now available for February 2022!

Moritz Doll (Apr 08 2022 at 12:22):

Will there be no recap for March?

Yaël Dillies (Apr 08 2022 at 12:23):

There is one in preparation! https://github.com/leanprover-community/blog/tree/month-mar-2022

Moritz Doll (Apr 08 2022 at 12:23):

ah, thanks. I just looked at the PRs. Stupid me.

Scott Morrison (Apr 08 2022 at 12:42):

I think everyone is feeling pretty busy. If anyone would like to suggest some sentences to go in between the selected PRs, at https://github.com/leanprover-community/blog/blob/month-mar-2022/posts/month-in-mathlib-mar-2022.md, please go ahead!!

Jireh Loreaux (Apr 09 2022 at 05:50):

I have some things I could add. Should I just push to the month-mar-2022 branch? Or do I need write access? Or should I fork and PR?

Johan Commelin (Apr 09 2022 at 06:26):

@Jireh Loreaux I think that for the blog repo a fork an PR method is the best for now

Johan Commelin (Apr 12 2022 at 13:04):

Finally the blogpost for March is out: https://leanprover-community.github.io/blog/posts/month-in-mathlib-mar-2022/
Congrats to everyone who helped with the record number of PRs!

Yaël Dillies (Apr 12 2022 at 13:07):

Oh sorry! I meant to make the graph theory section a bit more readable.

Yaël Dillies (Apr 12 2022 at 14:08):

blog#39

Kevin Buzzard (Apr 12 2022 at 14:14):

I wish we had stats for how many people are looking at these blog posts. I've already tweeted about it; I think that it's really fascinating that four years ago we were saying "we proved the complex numbers are a ring!" (which would have been of no interest to me as a researcher) but now we're saying early graduate level/"Part III" stuff and it's far more eye-catching

Yaël Dillies (Apr 12 2022 at 14:22):

Absolutely. And there's more of this sort of combinatorics coming your way!

Alex J. Best (Apr 12 2022 at 14:23):

It wouldn't be too hard to add some privacy friendly analytics to the blog, such as https://counter.dev/ or https://www.goatcounter.com/ if we wanted to.

Yury G. Kudryashov (Apr 12 2022 at 14:42):

The link lean pr 696 points to a wrong url

Johan Commelin (Apr 12 2022 at 14:44):

Whoops, good catch. Will fix

Jireh Loreaux (Apr 12 2022 at 15:16):

That's my bad, sorry.

Jireh Loreaux (Apr 12 2022 at 15:20):

@Johan Commelin in the graph theory section there's also a stray display style ε, as in $$\varepsilon$$, which should be just $\varepsilon$.

Yaël Dillies (Apr 12 2022 at 15:20):

Argh, that's my bad.

Bryan Gin-ge Chen (Apr 12 2022 at 15:41):

Jireh Loreaux said:

Johan Commelin in the graph theory section there's also a stray display style ε, as in $$\varepsilon$$, which should be just $\varepsilon$.

Fixed, thanks!

Patrick Massot (Jun 17 2022 at 21:08):

Don't miss Riccardo's post on the ring of integers of a cyclotomic field on the community blog! And while you're there, make sure you didn't miss the latest monthly recap.

Kevin Buzzard (Jun 17 2022 at 22:56):

" In particular we need to know that Q[ζp]] is a Dedekind domain." -- that should be Z not Q I think (sorry, on mobile)

Riccardo Brasca (Jun 17 2022 at 23:38):

You're right, thanks.

Patrick Massot (Jul 15 2022 at 17:27):

Today on the community blog, don't miss the official announcement of LTE completion!

Junyan Xu (Jul 15 2022 at 17:35):

Doesn't the linter complain it's not a theorem but a def?

Patrick Massot (Jul 15 2022 at 17:36):

It probably complains

Adam Topaz (Jul 15 2022 at 17:37):

I think keeping it as theorem is good (for the sake of publicity :rofl: )

Adam Topaz (Jul 15 2022 at 17:38):

I guess we could change the statement to is_zero ...

Adam Topaz (Jul 15 2022 at 17:38):

but that doesn't look as nice

Eric Wieser (Jul 15 2022 at 17:55):

Did we intentionally give credit to leanprover-community-bot?

Johan Commelin (Jul 15 2022 at 18:02):

Yes :wink:

Kevin Buzzard (Jul 15 2022 at 20:11):

They made a substantial number of contributions to the repo.

Heather Macbeth (Jul 29 2022 at 20:25):

Your weekend reading: @David Chanin on the new mathlib changelog, now live on the community blog.
https://leanprover-community.github.io/blog/posts/mathlib-changelog/
Thanks David!

Rob Lewis (Aug 04 2022 at 15:07):

I just came across https://utteranc.es/ , should we try to enable this on the community blog?

Eric Wieser (Aug 04 2022 at 15:09):

Or the very similar https://giscus.app/

Eric Wieser (Aug 04 2022 at 15:11):

Of course, the most on-brand thing to do would be to host the discussion on Zulip!

Rob Lewis (Aug 04 2022 at 15:13):

Eric Wieser said:

Of course, the most on-brand thing to do would be to host the discussion on Zulip!

Embedding a Zulip topic at the bottom of each blog post would be very cool, but I think that'd definitely be a custom project! Hah

Eric Wieser (Aug 04 2022 at 15:17):

The nice thing about using giscus over utterances is we can put it in the same repo as the blog, and not have discussions mixed with actual technical issues with the blog infrastructure

Rob Lewis (Aug 04 2022 at 15:29):

blog#50

Rob Lewis (Aug 07 2022 at 09:27):

Today on the blog, @Heather Macbeth and I write about classifying isocrysals! https://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/

Patrick Massot (Aug 11 2022 at 14:34):

We are quite late but the blog now has monthly recaps for June and July: https://leanprover-community.github.io/blog/

Patrick Massot (Sep 11 2022 at 20:11):

The monthly recap blog post for August is available at https://leanprover-community.github.io/blog/posts/month-in-mathlib-aug-2022/!

Eric Rodriguez (Sep 11 2022 at 20:51):

there's a typo in the rep theory section!

Riccardo Brasca (Sep 11 2022 at 21:46):

I am watching the us open final, so I am too busy to fix it, but you can always open a PR in the blog repository!

Eric Rodriguez (Sep 11 2022 at 22:12):

that's very ruud... ;b

Yaël Dillies (Sep 11 2022 at 22:15):

Oh, we could have #16033 and #16257 next to the Heyting algebra PR.

Eric Rodriguez (Sep 11 2022 at 22:17):

blog#57 and blog#56 for a separate issue

Patrick Massot (Oct 10 2022 at 20:02):

The monthly recap for September is available at https://leanprover-community.github.io/blog/posts/month-in-mathlib-sep-2022/!

Junyan Xu (Oct 11 2022 at 00:18):

Algebraic topology
PR #16403 proves the category of sheaves on a site with values is an abelian category is abelian. It also proves that sheafification is an additive functor.

This should be algebraic geometry right?

Johan Commelin (Oct 11 2022 at 00:45):

I guess maybe it should be just "category theory"? It's sort of all 3 of them, maybe?

Mike Shulman (Oct 11 2022 at 15:40):

I would describe that fact as category theory that has its best-known applications in algebraic geometry.

Adam Topaz (Oct 11 2022 at 15:50):

Yeah I would label this under category theory. Although "algebraic topology" == "category theory" nowadays, so who knows!?

Mike Shulman (Oct 11 2022 at 16:01):

I think there is still a difference. I might be more convinced by "homotopy theory" == "higher category theory".

Adam Topaz (Oct 11 2022 at 16:01):

(I wasn't being too serious here ;))

Mike Shulman (Oct 11 2022 at 16:03):

Ok. Sometimes it's hard to tell on the Internet. (-:

Patrick Massot (Oct 15 2022 at 12:02):

Don't miss https://leanprover-community.github.io/blog/posts/lte-examples/ and its very interesting discussion of how to make sure we formalize what we intend to formalize in case of very sophisticated theories.

Anatole Dedecker (Oct 15 2022 at 13:02):

There is a small typo in the first paragraph of "Definitions and Examples in Lean": defEnition should be defInition

Andrew Yang (Oct 15 2022 at 13:14):

There is a small typo in the "Pseudo-normed groups" section: CHFPNG₁_tto_CHFPNGₑₗ should be CHFPNG₁_to_CHFPNGₑₗ.

Adam Topaz (Oct 15 2022 at 14:17):

Thanks for pointing these out! I'm sure there are other typos as well, so I'll wait a little while then fix everything found in one batch.

Yaël Dillies (Oct 16 2022 at 02:19):

I'm glad to see #3292 being put to good use!

Kevin Buzzard (Oct 16 2022 at 09:11):

Yeah, the proof that we're using the real reals

Patrick Massot (Jun 12 2023 at 17:07):

The blog has been inactive because almost everybody having Lean time is busy with the port, but Kevin wrote a recap of the Banff cohomology workshop, don't miss it!

Jireh Loreaux (Jun 12 2023 at 17:09):

@Patrick Massot that link is bad, it takes you to port status fine.

Patrick Massot (Jun 12 2023 at 17:09):

Thanks

Kevin Buzzard (Jun 12 2023 at 17:17):

Looking forward to the MSRI post ;-)

Rob Lewis (Aug 26 2023 at 16:09):

The blog has still been pretty quiet, but I'm happy to announce a new post. @Jana Göken has written a nice summary of her experience at the Machine-Checked Mathematics workshop in Leiden last month. Check it out!

Rob Lewis (Aug 26 2023 at 16:10):

We've also recently merged a new feature to the blog: you can react to and comment on posts. This is powered by a strangely named app called Giscus using GitHub's resources, so you'll need to log in with GitHub to interact.

Rob Lewis (Aug 26 2023 at 16:26):

We're always looking for new blog contributions. Please get in touch if there's anything you're interested in writing up :smile:

Last updated: Dec 20 2023 at 11:08 UTC