Mathlib community meetings

Stream: general

[Kim Morrison]

As just announced, we are rebooting community meetings. (We previously ran these regularly during the porting proceess.)

[Kim Morrison]

The first meeting will be at 2024-02-10T02:00:00+11:00 at https://meet.google.com/guj-dcde-cdq, and the intention will be to continue every second month on the 2nd Friday. Note that these meetings will be alternating with the FRO month meetings, which are focussed more on language development and the work of the Lean FRO.

The meetings will be recorded, and posted online afterwards.

(Of course, if we discover there is demand for more frequent meetings, we can do that too!)

[Kim Morrison]

In planning these meetings, we would like to balance two things:

• Ensuring that community requests and concerns are heard and addressed.
• Staying on topic and avoiding long digressions --- these will be relatively large meetings so we can't waste people's time.

While we would like to keep these meetings fairly informal, these constraints mean that we will need an agenda. To the extent that a moderator is required, there'll be someone from the maintainers handling each meeting.

[Kim Morrison]

I'll post a poll shortly with suggestions of general topics for discussion. (We've already discussed this a bit amongst the maintainers.) Ideally in future we'll keep doing such a poll for each meeting, to try to make sure everyone has a say in what these meetings cover. Please feel free to use this thread to expand on topics, suggest subtopics, etc. But let's not have this thread become actual discussion of the topics! :-)

[Kim Morrison]

/poll Discussion topics for February Mathlib community meeting

[Eric Wieser]

Was a recording made of this meeting?

[Sebastian Ullrich]

No, but we can do so next time if people are in favor

[Eric Wieser]

Ah, so I guess

Scott Morrison said:

The meetings will be recorded, and posted online afterwards.

wasn't true this time

[Adam Topaz]

Indeed a recording would have been nice, as I had to miss this meeting due to teaching (and thus will probably miss the future ones during this semester).

[Michael Rothgang]

Similar here: I would have loved to watch a recording later.

[Kim Morrison]

Sorry, yes, absolutely meant to. At the last moment I discovered I couldn't open the meeting and Sebastian or Leo needed to, and then in the rush I forgot to record. Next time!

[Kim Morrison]

To get the ball rolling for future meetings, the default date would be 2024-04-13T00:00:00+10:00, after the next FRO community meeting at 2024-03-09T02:00:00+11:00.

[Kim Morrison]

I was wondering if in the meantime we might be interested in holding a "review party".

I was thinking a coordinated time, a zoom room possibly with some breakout rooms for subject areas, and participants do any combination of

• improving editorial processes (tracking slow PRs, auto-recommendation of reviewers, maybe even trying out editflow!)
• assigning PRs to potential reviewers
• closing, reviewing, and marking PRs as awaiting-author.

[Kim Morrison]

(I'll take thumbs up on that message as interest; if it's something enough people might participate in, we can move in to scheduling. Please refine the proposal below, too!)

[Eric Rodriguez]

One thing that was briefly mentioned last meeting and I think would be good to raise again next meeting is proof golfing. It's hard to say as sometimes it's stylistic changes that are only positive, and then sometimes it's huge compressions that most people would perceive as negative.

[Martin Dvořák]

My favorite example of huge proof compression:
https://github.com/leanprover-community/mathlib4/blob/a24907839ba28f0009af978642d62e1cc3076038/Mathlib/Data/List/Basic.lean#L2493

[Michael Rothgang]

Cross-linking the April edition since I at least would have looked in this thread.

[Jireh Loreaux]

oops, I didn't realize there were two threads, sorry!

[Matthew Ballard]

The next installment of the Mathlib community meetings will be 2024-08-09T10:00:00-04:00 in a little under three weeks. All are welcome!

As the agenda is being assembled, I want to encourage you to post here to highlight issues or questions of importance to you. If you prefer, you can also DM me or any maintainer of Mathlib.

[Matthew Ballard]

Much apologies for the late notice. But the next community meeting will be 2024-10-18T10:00:00-04:00 instead of today.

I want to particularly invite people involved in the #Equational project to share their perspectives on how Mathlib's current design helped or hurt their goals.

[Michael Rothgang]

This is/will be the correct link, right? https://meet.google.com/guj-dcde-cdq

[Matthew Ballard]

Reminder that the community meeting will be in 1 hour 2024-10-18T10:00:00-04:00 . The general theme is building on top of mathlib. We have a lot of interesting projects that have recently completed or are on going. I encourage anyone involved in one of them to join and share their perspectives.

[Damiano Testa]

Will the meeting be recorded? I won't be able to attend, but would be curious to hear about what is going on!

[Matthew Ballard]

Michael Rothgang said:

This is/will be the correct link, right? https://meet.google.com/guj-dcde-cdq

Tentatively. If not, I will post a different link 10 minutes before the start.

[Matthew Ballard]

It will be at https://sc-edu.zoom.us/j/89485684468 (~ 10 minutes)

[Eric Wieser]

The claim I made in the meeting was wrong, priority really does win:

import Mathlib

notation "x" => 1
notation (priority := default+1) "x" => "1"

#eval (x : Nat) -- doesn't work, even though the low-priority one would work

[Shreyas Srinivas]

I want to add that channeling contributions at the task proposal stage has the benefit that contributors haven't already sunk formalisation effort before duplicates have been spotted.

[Matthew Ballard]

Thanks to everyone who came! I learned a good deal. The next one will come in December with more information appearing closer to the date.

[Kevin Buzzard]

Apologies -- I couldn't make this one (I was interviewing) but I had not realised that people involved in interesting projects were specifically being asked things (indeed I didn't read the message above about this because I was interviewing :-) ). Let me know if there's any questions which you just want me to hit R and say something about re FLT.

[Matthew Ballard]

Reminder that the next Mathlib community meeting will be 2024-12-13T10:00:00-05:00 at https://meet.google.com/guj-dcde-cdq All are welcome!

[Matthew Ballard]

Reminder that this will start in a little less than 50 minutes. Hope to see you there.

[Kim Morrison]

How did the meeting go? What was discussed?

[Kevin Buzzard]

And is the recording available?

[Michael Rothgang]

There was the plan of turning a transcript of the meeting into a community blog post, right? (I still think that would be great.)

[Ashley Blacquiere]

Kevin Buzzard said:

And is the recording available?

Yes! I just uploaded it to the Lean FRO channel on YouTube (HD is still processing as I write this, but SD should be available to view).

Kim Morrison said:

How did the meeting go? What was discussed?

Main topics were big wins from 2024 and hopes for Mathlib in 2025.

Michael Rothgang said:

There was the plan of turning a transcript of the meeting into a community blog post, right? (I still think that would be great.)

I have the transcript and can share if anyone would like to use it to create a blog post. Given the meeting topic, it'd be a great source for a 2024 wrap-up post.

[Matthew Ballard]

Summaries of the two main topics at #general > Highlights of 2024? and #general > Predictions for 2025? Please contribute!

[Matthew Ballard]

Our next community meeting will be tomorrow 2025-02-14T10:00:00-05:00 Please join us!

[Matthew Ballard]

Please join! Happening now!

[Matthew Ballard]

https://meet.google.com/guj-dcde-cdq

[Kim Morrison]

Anyone want to give a brief summary or recap?

[Ashley Blacquiere]

I have the recording and transcript! Haven't posted it yet, but coming soon.

[Ashley Blacquiere]

Today's Mathlib Community Meeting recording is live on YouTube.

[Kim Morrison]

Many interesting discussions (I'm just part way through).

[Kim Morrison]

The desire to have a good auto-formatter is of course reasonable! It's also very hard because of Lean's extensibility. We really want to get there but it doesn't seem likely to happen immediately!

In the meantime, can we just start linting for all the most common errors? (Spaces around colons and parentheses, for example.)

[Kim Morrison]

It's really important that reviewers don't have to do this.

[Damiano Testa]

I can look into toning down the ppRoundtrip linter, so that it can reliably check something.

[Damiano Testa]

It is already not too bad, but it flags way too much and not everything is good.

[Damiano Testa]

I can probably start by making it look at binders.

[Michael Rothgang]

I could probably whip up a text-based linter for e.g. the spacing issues. It would be less reliable than the pretty-printer based logic, but could also be useful.

[Damiano Testa]

There was already an experiment with linting whitespace: #14379.

[Damiano Testa]

While trying to get a reasonable number of exceptions with the linter, #22006 contains a few easy whitespace cleanups.

[Arthur Paulino]

As a data point reference, cargo fmt doesn't attempt to format everything. In particular, it usually skips macro syntax.

Though I'm not sure it would be very satisfying for Mathlib in particular because the vast majority of lines are within the tactic DSL. So in a sense it's what cargo fmt would skip, if we apply the analogy.

Tossing an idea in case it helps: syntax authors could provide an optional API to format the syntax they create, which would be ultimately called by lake fmt. Otherwise, output the same original string of text.

[Eric Wieser]

In theory, syntax already has such an API, in the form of instructions to the pretty printer

[Damiano Testa]

In fact, the pretty-printed syntax is what the ppRoundtrip linter uses.

[Damiano Testa]

Here is a source of many discrepancy between the pretty-printed syntax and actual mathlib code: is it

theorem logMap_apply_of_norm_one (hx : mixedEmbedding.norm x = 1)
    (w : { w : InfinitePlace K // w ≠ w₀ }) :

or

theorem logMap_apply_of_norm_one (hx : mixedEmbedding.norm x = 1)
    (w : {w : InfinitePlace K // w ≠ w₀}) :

(note the spaces around the brackets).

[Damiano Testa]

The pretty-printer makes a choice. However, for situations such as the one above, I am not so sure that enforcing either convention is clearly the way to go.

[Damiano Testa]

And special-casing all situation such as the one above is a lot of work! :smile:

[Damiano Testa]

Not to mention, the situations where the pretty-printed syntax is either invalid or valid but not defeq to the original!

[Arthur Paulino]

I didn't know that pretty-printed syntax could possibly not be defeq to the original source. That's pretty scary.

Regarding convention, the convention is usually whatever the auto-formatter picks. It's automatic anyway

[Damiano Testa]

A common source of non-defeq comes from casts/type ascriptions.

[Eric Wieser]

@Damiano Testa, I think you're confusing delaboration (Expr -> Syntax) with pretty printing (Syntax -> Std.Format)

[Eric Wieser]

Syntax -> String can also be ambiguous, but I think you need something more pernicious than coercions to trigger it

[Damiano Testa]

Eric, yes, I did confuse delaboration with pretty-printing!

[Damiano Testa]

#22051 removes more whitespace inconsistencies (and some missing . and typos).

[Damiano Testa]

The bulk of the changes are to make sure that doc-strings start with /-- and end with -/ -- emphasis on the spaces!

[Matthew Ballard]

Our next Mathlib community meeting will at be at 2025-04-11T10:00:00-04:00. Please join us on Google Meet https://meet.google.com/guj-dcde-cdq !

[Matthew Ballard]

Reminder: this is happening in 5!

[Matthew Ballard]

Due to the Big Proof workshop at INI this week, we are moving the date for this month’s community meeting from 2025-06-13T10:00:00-04:00 to 2025-06-27T10:00:00-04:00.

[Matthew Ballard]

Reminder that in under two hours we will start the next community meeting at https://meet.google.com/guj-dcde-cdq Please join us.

[Matthew Ballard]

Starting now! Please join us if you are interested.

[Matthew Ballard]

Thanks to everyone who joined. Some items from the meeting:

• We don't have a Contributing.md Should we? What should we include?
• Related, should we update our PR template to include links to information like this and affirmative check boxes?
• An important thing to keep in mind is the division between building on top of mathlib and contributing directly to mathlib. For someone new coming in from the outside, these are going to require different levels of engagement with the tooling around mathlib.
• It would be nice to regularly automatically highlight contributors, particularly first time contributers. https://github.com/all-contributors/cli might help
• Developing the tactic-authoring and meta-programming pool of knowledge would be great. Some ideas towards this were to hold a workshop focused on it to help grow peoples' skills, to pair up experienced mentors with less experienced by eager developers to work on projects.
• For projects, we have a master list at #10361 which could use some triaging to assess difficulty as projects. Finding a way to gauge community need would also help prioritize potential projects.

[Matthew Ballard]

A reminder that the next community meeting will be 2025-08-08T10:00:00-04:00 at https://meet.google.com/guj-dcde-cdq. Topics that have been mentioned:

• What is grind and how should I use it?
• Can we streamline Mathlib's morphism hierarchy?
• What is the Mathlib Initiative?

Hopefully people will show up who can answer these questions! (Not it!).

[Matthew Ballard]

From #mathlib4 > Mathlib Announcements we've seen grw and Riemannian manifolds land since the last meeting. Also rich topics!

[Ching-Tsun Chou]

Will the meeting be recorded? The time (7am) is a bit too early for my time zone.

[Kim Morrison]

(Unfortunately I won't be able to make it, hopefully someone else who has been using grind will come!)

[Matthew Ballard]

Reminder: 1 hour.

[Michael Rothgang]

I won't make it either (on a crowded train in Germany), but would love to listen to a recording.

[Matthew Ballard]

Bonus to anyone who brings a problem for GPT 5 Pro to chew on while we chat.

[Bryan Gin-ge Chen]

If GPT5 can figure out what's going on in #mathlib4 > Failing CI @ 💬 (and fix it), I'll be very happy.

[Yaël Dillies]

Matthew Ballard said:

Bonus to anyone who brings a problem for GPT 5 Pro to chew on while we chat.

Natural or formal language?

[Matthew Ballard]

Let's say the output has to be Lean code. The input can be either.

[Yaël Dillies]

Too late, I've got formal statement :grinning:

[Yaël Dillies]

Here it is:

import Mathlib

/-- Proved in the literature. -/
lemma vc_lt_four_of_convex_r2 {C : Set (Fin 2 → ℝ)} (hC : Convex ℝ C)
    {x : Fin 4 → Fin 2 → ℝ} {y : Set (Fin 4) → Fin 2 → ℝ}
    (hxy : ∀ i s, x i + y s ∈ C ↔ i ∈ s) : False := sorry

/-- Open as far as I'm aware. -/
lemma vc2_lt_two_of_convex_r3 {C : Set (Fin 3 → ℝ)} (hC : Convex ℝ C)
    {x y : Fin 2 → Fin 3 → ℝ} {z : Set (Fin 2 × Fin 2) → Fin 3 → ℝ}
    (hxy : ∀ i j s, x i + y j + z s ∈ C ↔ (i, j) ∈ s) : False := sorry

[Matthew Ballard]

import Mathlib

/-- Proved in the literature. -/
lemma vc_lt_four_of_convex_r2 {C : Set (Fin 2 → ℝ)} (hC : Convex ℝ C)
    {x : Fin 4 → Fin 2 → ℝ} {y : Set (Fin 4) → Fin 2 → ℝ}
    (hxy : ∀ i s, x i + y s ∈ C ↔ i ∈ s) : False := by
  classical
  -- Diagonal set: membership is defined as *not* being in C after the shift by `y s`.
  let s : Set (Fin 4) := {i | x i + y s ∉ C}
  -- For this `s`, the given equivalence becomes `p ↔ ¬p`.
  have h : x (0 : Fin 4) + y s ∈ C ↔ x (0 : Fin 4) + y s ∉ C := by
    simpa [s] using hxy (0 : Fin 4) s
  -- `p ↔ ¬p` is impossible.
  by_cases hp : x (0 : Fin 4) + y s ∈ C
  · exact (h.mp hp) hp
  · exact hp (h.mpr hp)

/-- Open as far as I'm aware. -/
lemma vc2_lt_two_of_convex_r3 {C : Set (Fin 3 → ℝ)} (hC : Convex ℝ C)
    {x y : Fin 2 → Fin 3 → ℝ} {z : Set (Fin 2 × Fin 2) → Fin 3 → ℝ}
    (hxy : ∀ i j s, x i + y j + z s ∈ C ↔ (i, j) ∈ s) : False := by
  classical
  -- Same diagonal trick in the 2-parameter index.
  let s : Set (Fin 2 × Fin 2) := {p | x p.1 + y p.2 + z s ∉ C}
  have h :
      x (0 : Fin 2) + y (0 : Fin 2) + z s ∈ C ↔
      x (0 : Fin 2) + y (0 : Fin 2) + z s ∉ C := by
    simpa [s] using hxy (0 : Fin 2) (0 : Fin 2) s
  by_cases hp : x (0 : Fin 2) + y (0 : Fin 2) + z s ∈ C
  · exact (h.mp hp) hp
  · exact hp (h.mpr hp)

[Yaël Dillies]

Egregious! It thinks I am doing set theory!

[Matthew Ballard]

After what I've seen it do, I am just happy it doesn't get near my student's PhD problem.

[Matthew Ballard]

I am not sure how long that will be the case though...

[Yaël Dillies]

I wonder how much better its answer would have been had I written an informal description of the problem

[Matthew Ballard]

We should probably continue in #Machine Learning for Theorem Proving. I still trying to push 5 Pro on the same thing with little success but I suspect there are more people with access around.

[Eric Wieser]

Want to add this to formal-conjectures?

[Yaël Dillies]

Sure, why not!

[Eric Wieser]

Will the recording / transcript / Gemini notes be shared for the meeting yesterday?

[Matthew Ballard]

The recording is up on Youtube now. (Link suppressed due to mobile.) Thanks @Ashley Blacquiere ! The other two we can share also but I haven’t sanity checked the Gemini output.

[Yaël Dillies]

@Eric Wieser said:

Want to add this to formal-conjectures?

Here's the full file I've written since the meeting. How much of it do you want in formal-conjectures? In order, I have:

• a currently non-leanable proof of vc_lt_four_of_convex_r2
• leanable proofs of exists_convex_r3_vc_eq_infty and exists_convex_rn_add_two_vc_n_eq_infty (the former is a special case of the latter, really)
• hopefully soon a non-leanable proof of vc2_lt_two_of_convex_r3
• no proof idea on exists_vcn_le_of_convex_rn_add_one whatsoever

[Paul Lezeau]

Yaël Dillies said:

Here's the full file I've written since the meeting. How much of it do you want in formal-conjectures? In order, I have:

• a currently non-leanable proof of vc_lt_four_of_convex_r2
• leanable proofs of exists_convex_r3_vc_eq_infty and exists_convex_rn_add_two_vc_n_eq_infty (the former is a special case of the latter, really)
• hopefully soon a non-leanable proof of vc2_lt_two_of_convex_r3
• no proof idea on exists_vcn_le_of_convex_rn_add_one whatsoever

I think everything in the file looks reasonable to add - feel free to open a PR and ping me for a review!

[Notification Bot]

A message was moved here from #mathlib4 > Instances on terms by Damiano Testa.

[Yaël Dillies]

@Paul Lezeau said:

I think everything in the file looks reasonable to add - feel free to open a PR and ping me for a review!

:ping_pong: google-deepmind/formal-conjectures#553 :slight_smile:

[Matthew Ballard]

Apologies for the late notice but let’s push the community meeting until next Friday (localized time when I get to a computer).

[David Renshaw]

ah, that explains why there are so few people in the meeting right now!

[David Renshaw]

in the future, can you please update the "Lean Community Meetings" Google calendar when things get rescheduled like this?

[David Renshaw]

(There were about 6 people other than me who showed up today. I told them the meeting is happening next week.)

[Matthew Ballard]

Apologies again. Travel constraints ultimately made it impossible. I should have just rescheduled earlier rather than holding out hope.

[Matthew Ballard]

Reminder: this is now coming up in a little under 24 hours 2025-10-17T10:00:00-04:00 Hope to see you there!

[Michael Rothgang]

Same meeting link as before, i.e. https://meet.google.com/guj-dcde-cdq?

[Matthew Ballard]

Reminder: ~30 minutes from now.

[Riccardo Brasca]

Will it be recorded?

[Kim Morrison]

Could someone post a link to the recording if available?

[Rida Hamadani]

Kim Morrison said:

Could someone post a link to the recording if available?

https://youtu.be/SWpK9RWZwVI

[Matthew Ballard]

Reminder that our next meeting is in a little under 24 hours 2025-12-12T10:00:00-05:00

Everyone is welcome. Please bring with you some of your favorite things in Lean and Mathlib over the past year and your new year's resolutions!

[Matthew Ballard]

Heading over to https://meet.google.com/guj-dcde-cdq now. See you there!