Madrid, Spain

Stream: Geographic locality

[Hang Lu Su]

Hola a tod@s!

@Pepa Montero Jimena, @Enrique Diaz Blanco, @Juanjo Madrigal, @Jorge Luis Mayoral Perez and myself are meeting this Wednesday at the faculty of mathematics of Universidad Complutense at 18:00 to organize Madrid Lean meetings (MadLean). If anyone is interested in helping us organize, please DM me or any of the above people to coordinate. Thanks!

PS: would it be possible to rename this topic to Madrid, Spain or Madrid, ES for clarity?

[Hang Lu Su]

Exact location and time confirmed! We have reserved aula 113 of the faculty of mathematics from 18:00-20:00.

[Hang Lu Su]

My co-organizers and I are delighted to announce MadLean, the first Lean Meetup in Madrid!

It will take place this Wednesday at 18:00-19:30 at the Faculty of Mathematics of the Universidad Complutense (room TBA but probably 113).

The rough plan is to:

• Assist with Lean installation :computer:.
• Show newcomers how to do simple proofs :check:.
• Share our Lean tooling :tools:.
• Discuss projects we are working on :light_bulb:.
• Hang out and have a good atmosphere while learning together :blush:.

Everyone is welcome to attend!

Poster by our very own @Pepa Montero Jimena

[Castedo Ellerman]

Aw man, I wish I was in Madrid more often and I could join. I notice nobody in this Spain topic is sending others a :octopus: emoji. :wink: :rolling_on_the_floor_laughing:

[Hang Lu Su]

Room 113 confirmed!

[Hang Lu Su]

The second MadLean meetup will happen next Wednesday, February 18th 18:00-19:30, at the Faculty of Mathematics of the Universidad Complutense, room 104! :tada:

Last week:

• I presented my finitely presented group project (WIP).
• @Jorge Luis Mayoral Perez gave us a tutorial on installing the leanblueprint tool by @Patrick Massot. :working_on_it:

This week:

• Some of us are going to show up earlier at 17:00 to watch @Martin Dvořák's thesis defense, and then proceed with the program as usual. :book:
• We now have a local WhatsApp community to keep up with our members, spearheaded by @Enrique Diaz Blanco! :blush:

Poster by @Pepa Montero Jimena.

[Hang Lu Su]

The third MadLean meetup will happen next Wednesday, February 11th 18:00-19:30 at the Faculty of Mathematics of the Universidad Complutense, room TBA.

Last week:

• We watched Martin's thesis defense as planned.
• @Pepa Montero Jimena gave us a presentation of her bachelors' thesis, where she formalized Urysohn's lemma! :tada:

Update:

• We have now have an official website, made by none other than @Juanjo Madrigal !!! :star_struck:

https://madlean-hub.web.app/

[Snir Broshi]

Very cool!
Question: is the thesis unrelated to Mathlib? Because Mathlib had Urysohn's lemma since 2021 (docs#exists_continuous_zero_one_of_isClosed / mathlib3#6967). Though only one side of it IIUC?

[Pepa Montero Jimena]

Hi @Snir Broshi! The thesis is not unrelated to Mathlib, I used Mathlib objects for my formalization and proof, but I was prompted by my supervisor to try to write it myself without looking at Mathlib's.

From the docs you mentioned I copied this extract: "Most paper sources prove Urysohn's lemma using a family of open sets indexed by dyadic rational numbers on [0, 1]. There are many technical difficulties with formalizing this proof (e.g., one needs to formalize the "dyadic induction", then prove that the resulting family of open sets is monotone). So, we formalize a slightly different proof."

Essentially, I did not realize there was an easier way of formalizing it, so I followed the traditional proof mentioned here and ran into the problems they describe (and overcame them!). So my proof is different from the one in Mathlib.

[Ruben Van de Velde]

Nice job!

[Pepa Montero Jimena]

Thank you! :))

[Hang Lu Su]

Just letting people know the room will be announced last minute this week.

There’s been an administrative hiccup, but @Pepa Montero Jimena and I are meeting with the vice-dean of the university this week at the beginning of the meetup in order to ask for more resources, so hopefully this shouldn’t happen again!

Meetup will start on time with @Enrique Diaz Blanco @Juanjo Madrigal present :gift_heart:.

[Hang Lu Su]

Room 113 confirmed! :face_exhaling:

[Hang Lu Su]

The fourth MadLean meetup will happen next Wednesday, February 25th 18:00-19:30 at the Faculty of Mathematics of the Universidad Complutense, room TBA.

Last week:

• @Enrique Diaz Blanco held down the event while most of us were gone :smile:.
• @Juanjo Madrigal introduced us to verso :book:.
• I spoke about my experience contributing to mathlib.

If I may permit myself an observation, it seems like while the documentation is very clear on how to PR, due to people here not having experience with the PR process (I might be the only one in Madrid, or at least at the meetup) there seems to be a psychological barrier towards action despite some of our local people having pretty advanced Lean knowledge. I want to once again thank @Kevin Buzzard for encouraging me to just put my code out there, and was very happy to be able to pass that human touch on. I think we should see more local activity on that front soon, if it hasn't happened already :wink:.

Updates:

• The meeting with the vice-dean went smoothly, and I want to shout out @Pepa Montero Jimena for her professionalism during the meeting. We have reason to expect things to be a little more stable now that the university is aware of our activities.

[Hang Lu Su]

Room 104 confirmed for this week!

A big thanks to @Enrique Diaz Blanco who's been doing most of the paperwork to book the room thus far despite being at a very critical point in his academic journey. :clap:

[Hang Lu Su]

Latest version of our poster by @Pepa Montero Jimena!

[Hang Lu Su]

We have moved to room 114 due to a technical issue with the projector.

[Hang Lu Su]

The fifth MadLean meetup will happen next Wednesday, March 3rd 18:00-19:30 at the Faculty of Mathematics of the Universidad Complutense, room TBA.

Last time:

• We tried a new format with these meme-y onboarding slides. The goal was three-fold: quickly onboard new members, foster a sense of psychological safety, and have every member participate by imposing that the first half-hour be a collaborative workshop. :sparkling_heart:.
• @Juanjo Madrigal gave a brilliant talk about elaboration, along with a nice demo file we can click through and understand at home. :mind:

Updates:

• @Pepa Montero Jimena made her first mathlib PR :tada:.
  Her poster is also now advertised on the screens at UCM!

  

• We now have a MadLean Github account where we are planning to post communal projects :peace_sign:.

• It's with great sadness that we are saying goodbye to @Juanjo Madrigal, who be moving to London for a Lean-related job. Thank you for all you've given to MadLean so far, and let's keep in touch! :smiling_face_with_tear:

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as resolved.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.