Paris area, France

Stream: Geographic locality

[Samuel Lelièvre]

I'm in Orsay, Paris area, France.

[Patrick Massot]

I'm also there, we should be able to meet after the lock-down!

[Patrick Massot]

(Samuel is working in my math department).

[Etienne.bfx]

Hi, I am a first year PhD student in Ergodic Theory and Hyperbolic geometry. I am at Ecole polytechnique, a school near Paris.

[Kunhao Zheng]

Hi! I didn't find the stream before! I'm also from EP and I'm doing my 3A internship right now. Enchanté!

[Floris van Doorn]

I'm starting to work with @Patrick Massot this week at the University of Paris-Saclay.

[Filippo A. E. Nuccio]

Welcome to France, @Floris van Doorn !

[Frederic Peschanski]

Bonjour, I'm an associate professor at Sorbonne University (campus Jussieu) in theoretical computer science and combinatorics.

[Kyle Miller]

I recently started working with @Patrick Massot at Université Paris-Saclay, sharing an office with @Floris van Doorn

[Rish Vaishnav]

I have recently joined the LMF at Université Paris-Saclay! I will be working on designing and implementing a translator between Lean and Dedukti (and on proof system interoperability more generally).

[Patrick Massot]

Nice! We have a very informal seminar where people interested in formalized maths try to meet once every two weeks in Orsay. I wrote "try" because sometimes we don't manage to meet (especially in those days when a stubborn government insist on a very unpopular pension system reform, resulting in many days where protests make it very difficult to move in the Paris area). Do you want to receive information about it? Ideally you could even give a talk so that we get to know you. It doesn't matter whether you formalized great stuff or not, you could simply tell us what you are interested in.

[Rish Vaishnav]

Yes, I would love to attend and introduce myself! Feel free to add me to any relevant mailing list.

[Sam van G]

Me too, please, @Patrick Massot. Thank you!

[Sam van G]

I think I never introduced myself here: I am an associate professor ("maître de conférences") at IRIF, Université Paris Cité.

[Yvon Fredrich]

Hi, I'm a maths student at the ENS paris saclay and curious about mathlib, lean and all the interfaces aroud lean. I'm still very new though. I'm also interested in the informal seminar in Orsay @Patrick Massot, could I receive information about it ?

[Riccardo Brasca]

For those around, I will give a talk next Monday, at 2023-03-20T14:00:00+01:00 or 2023-03-20T15:00:00+01:00 (still to be confirmed) about the flt-regular project. The talk will be at Université Paris Cité (aka Paris 7, aka Paris Diderot, aka Université de Paris...), here

It will be quite similar to my last year talk at Orsay.

[Nicolas Rolland]

Bonjour, I am interested in using Lean as a programming language and DSL host, relying on category theoretical constructs (mostly distributors from Jean Bénabou)

[Riccardo Brasca]

Welcome! Where are you based? In Paris area there are mostly mathematicians interested in Lean, but we are happy to get new people involved!

[Nicolas Rolland]

In Paris indeed ! The ability to express both (categorical) math and real programs in the same language is very enticing and will hopefully be fruitful

[Nicolas Rolland]

btw, I (used to) organize a functional programming meetup group in Paris and plan to reboot it, if only to talk about Lean . It is a perfect ground for making presentations talks to a forgiving audience, (mostly) amateur in formal methods, haskell/ml/scala practionners . It can be useful to evangelize Lean (hence my desire to reboot it), to polish and practice presentations before going to your peers for hard scrutiny, or to showcase "programming pearls" you find useful. It is more "program" inclined than mathy, but they were happy to hear about monoidal string diagrams and monads

[Shreyas Srinivas]

If it is online, I would love to join. I am 2-3 hours from Paris, but it costs 100 Euros to get there

[Riccardo Brasca]

For those around Paris this should be interesting (I think it is more for students than experts, but still)

[Vincent KUBICKI]

Hi, I am completely new to proof assistant. I am an amateur who wants to understand the jump from functional language (Haskell) to theorem proving. I live and work in Lille in ML / IA (mostly in C++).

[Patrick Massot]

Welcome! Isn't it risky to publicly write that Lille is in the Paris area?

[Vincent KUBICKI]

1 hour of TGV, come on :).

[Ruben Van de Velde]

Lille? That's nearly Belgium!

[Vincent KUBICKI]

There is a beautiful part of Flanders on this side of the border also.

[Patrick Massot]

I'm leaving. I don't want to be around when someone from Lille comes here and start killing everyone without trying to figure out who said Lille is in the Paris area and who said it is in Belgium.

[Filippo A. E. Nuccio]

Oh, I thought it was in Canada... :angel: :flag_canada:

[Paul Schwahn]

Bonjour, I am a first year postdoc at Paris-Saclay! I wonder, does this informal seminar still exist?

[Patrick Massot]

Not in Orsay. Three people left this year. I will come back next year and maybe we will resume.

[Paul Schwahn]

Ah that's unfortunate, since I am only there until the summer.

[Joël Riou]

I am in office 3P17 (not right now though).

[Antoine Chambert-Loir]

@Riccardo Brasca and I had envisioned to pursue it in Paris this year but we didn't manage to make it. In a few weeks, after LFTCM2024, we may find time for a few meetings.

[Joachim Breitner]

I’m tentatively traveling to Paris in a week, on Monday, Sep 23 and wouldn’t mind getting to know the faces of some of the local Lean and Mathlib community there. Anyone up for lunch?

[Patrick Massot]

This is very tempting. Where will you be exactly?

[Riccardo Brasca]

It depends on my teaching, but I am also interested!

[Joachim Breitner]

Nice! (The emotion, not the City)
Haven't booked my train yet, visiting a friend in Jussieu. But no schedule yet. I'm arriving at gare de lest, probably around 11:30, and happily hop on Metro to come anywhere.

[Patrick Massot]

We could try to find some lunch place around the Cité U metro station. This is at the intersection of the train line from Orsay to Paris and the tram line going through Riccardo’s university.

[Patrick Massot]

Note that I am in Paris is a rather weak sense, I have an half an hour train ride to Paris.

[Joachim Breitner]

Sounds like a good plan to me!

[Joachim Breitner]

But I stand corrected: My train (just booked) arrives at 12:33. Hope it can still work.

[Johan Commelin]

This is France... they have their meals 2 hours later than in Germany :grinning:

[Riccardo Brasca]

On Monday I have to teach at 2:45 PM, so around 1pm at Cité universitaire should work me

[Patrick Massot]

Riccardo, do you know any nice place we could use?

[Joachim Breitner]

Johan Commelin said:

This is France... they have their meals 2 hours later than in Germany :grinning:

… and longer

[Riccardo Brasca]

Patrick Massot said:

Riccardo, do you know any nice place we could use?

Not close to Cité U. But if you take the B we can maybe go somewhere close to Luxembourg

[Riccardo Brasca]

(not talking about the country)

[Patrick Massot]

Sure, this is almost the same to me. I was trying to find something more convenient for you.

[Joël Riou]

On Monday, I teach in the early morning in Orsay, but I can go to anywhere on RER B for lunch.

[Luigi Massacci]

From experience I can recommend this place:

Pomozza
+33 1 44 98 21 78
https://goo.gl/maps/ScakZF6V95EcywNp9

which is about 30min from Orsay and maybe 35(?) from Sophie-Germain (changing from C to B at cité U, I assume it should take about that) and about as many from gare de l’est (that’s on the B line too anyway)

[Tomaz Mascarenhas]

Hi, I would love to go too (though I am from Brazil, so not sure if I count as part of the local Lean community). Next monday at lunch works for me.

[Riccardo Brasca]

@Antoine Chambert-Loir are you around next Monday?

[Patrick Massot]

In the mean time I realized that I need to be at ENS Paris at 3pm so I’m definitely in favor of having lunch in quartier latin.

[Rish Vaishnav]

I can probably make it too! (Along with Tomaz, we're both at ENS Paris Saclay)

[Antoine Chambert-Loir]

Riccardo Brasca said:

Antoine Chambert-Loir are you around next Monday?

I can be there, yes.

[Patrick Massot]

Do you know a restaurant that would be convenient? It seems our group will be a bit large to improvise.

[Antoine Chambert-Loir]

How many people would be there? There are nice vietnamese or tibetan restaurants on rue Saint Jacques, and a decent pizza place facing the Institut océanographique.

[Patrick Massot]

I count 8 people so far, but I guess we could easily have a couple more when more people read this.

[Riccardo Brasca]

The standard tibetan place next to the IHP or the pizza place are good for me (the pizza place is rather big IIRC)

[Patrick Massot]

I don’t understand what happens to our world. You are the second person in this thread to claim to be Italian but still recommends having a pizza in France. What’s going on?? What will be next? Pastas in France?

[Riccardo Brasca]

well, that place is really not bad (and 100% italian of course)

[Filippo A. E. Nuccio]

Riccardo Brasca said:

The standard tibetan place next to the IHP or the pizza place are good for me (the pizza place is rather big IIRC)

I won't be there, but I am humbled to acknowledge @Riccardo Brasca 's tolerance for Italian restaurants in Paris :flag_italy:

[Anatole Dedecker]

I would love to join (hi everyone btw) ! I’m following a course at Sophie Germain until 1pm technically, but let’s say I can leave 30 minutes early if it’s not possible to delay the meeting time.

[Patrick Massot]

We can order for you if you are a bit late but manage to access Zulip from the metro.

[Patrick Massot]

I think we need to count people a bit more precisely now. Please answer the following poll.

[Patrick Massot]

/poll I want to participate in the Lean lunch on September 23rd near rue Saint Jacques
Yes

[Patrick Massot]

@Joachim Breitner @Riccardo Brasca @Joël Riou @Luigi Massacci @Tomaz Gomes @Rish Vaishnav @Antoine Chambert-Loir @Anatole Dedecker

[Patrick Massot]

I added a no option to make sure all the persons I pinged actually answer, but of course there is no need for all 10.000 other zulip users to answer they won’t come…

[Patrick Massot]

And of course people who would like to come but were not pinged because they didn’t participate in this discussion yet (or because I missed their participation) are very welcome!

[Patrick Massot]

Ok, the pizza place wasn’t available at 1pm so I booked the tibetan one, the Kokonor, 206 Rue Saint-Jacques.

[Riccardo Brasca]

Thanks!

[Patrick Massot]

I just noticed that someone answered the poll after I wrote that I booked the restaurant. I would have been smart to ping me then. I hope the restaurant will be able to fit that extra person.

[Antoine Chambert-Loir]

It was me, when I noticed I hadn't answered the poll, because I hadn't seen it… Don't worry, let's meet some other time.

[Joachim Breitner]

I am optimistic that maybe someone will be late or, or else we can squeeze together

[Riccardo Brasca]

We can surely squeeze!

[Patrick Massot]

Yes, you should definitely come anyway.

[Patrick Massot]

I should have checked more carefully before booking.

[Antoine Chambert-Loir]

(The technical point is just that the ping was below the poll, and not within, and Zulip on my phone didn't show it…)

[Patrick Massot]

As far as I know Zulip doesn’t allow anything in the same message as a poll.

[Antoine Chambert-Loir]

You may be right. So the only lesson is to include a link to the thing in the message where people are pinged.

[Antoine Chambert-Loir]

(I saw the ping, but I just understood I needed to be aware, and I answered messages…)

[Joachim Breitner]

My train is slightly delayed, so I may run 10-15mins late.

[Joachim Breitner]

I think it was @Antoine Chambert-Loir who mentioned a polyrith-produced proof that was then too large for lean to handle. Is that still somewhere to look at, or easily reproducible?

[Antoine Chambert-Loir]

I mentioned that, indeed, and I was thinking of the proof of associativity of the group law on elliptic curves, when done using the “trivial” way of writing down the relevant polynomials and checking equality monomial by monomial.

[Antoine Chambert-Loir]

I suppose @Kevin Buzzard and @Heather Macbeth have more specific details to share.

[Riccardo Brasca]

if this was the case @David Ang surely knows

[David Ang]

I haven't touched this in a while, but from my old messages with Kevin, I think the relevant equality is this:

example {x₁ x₂ x₃ y₁ y₂ y₃ a₁ a₂ a₃ a₄ a₆ : ℚ}
    (h₁ : y₁^2+a₁*x₁*y₁+a₃*y₁=x₁^3+a₂*x₁^2+a₄*x₁+a₆)
    (h₂ : y₂^2+a₁*x₂*y₂+a₃*y₂=x₂^3+a₂*x₂^2+a₄*x₂+a₆)
    (h₃ : y₃^2+a₁*x₃*y₃+a₃*y₃=x₃^3+a₂*x₃^2+a₄*x₃+a₆):
    (((a₁*x₁+a₁*x₂-y₁+a₁*a₂-a₃)*(x₁-x₂)^3+(2*x₁+x₂-a₁^2+a₂)*(x₁-x₂)^2*(y₁-y₂)-2*a₁*(x₁-x₂)*(y₁-y₂)^2-(y₁-y₂)^3-y₃*(x₁-x₂)^3)^2+a₁*((a₁*x₁+a₁*x₂-y₁+a₁*a₂-a₃)*(x₁-x₂)^3+(2*x₁+x₂-a₁^2+a₂)*(x₁-x₂)^2*(y₁-y₂)-2*a₁*(x₁-x₂)*(y₁-y₂)^2-(y₁-y₂)^3-y₃*(x₁-x₂)^3)*((-x₁-x₂-a₂)*(x₁-x₂)^2+a₁*(x₁-x₂)*(y₁-y₂)+(y₁-y₂)^2-x₃*(x₁-x₂)^2)*(x₁-x₂)-(a₂*(x₁-x₂)^2+((-x₁-x₂-a₂)*(x₁-x₂)^2+a₁*(x₁-x₂)*(y₁-y₂)+(y₁-y₂)^2)+x₃*(x₁-x₂)^2)*((-x₁-x₂-a₂)*(x₁-x₂)^2+a₁*(x₁-x₂)*(y₁-y₂)+(y₁-y₂)^2-x₃*(x₁-x₂)^2)^2)*(x₁*(x₂-x₃)^2-((-x₂-x₃-a₂)*(x₂-x₃)^2+a₁*(x₂-x₃)*(y₂-y₃)+(y₂-y₃)^2))^2*(x₂-x₃)^2 = ((y₁*(x₂-x₃)^3-((a₁*x₂+a₁*x₃-y₂+a₁*a₂-a₃)*(x₂-x₃)^3+(2*x₂+x₃-a₁^2+a₂)*(x₂-x₃)^2*(y₂-y₃)-2*a₁*(x₂-x₃)*(y₂-y₃)^2-(y₂-y₃)^3))^2+a₁*(y₁*(x₂-x₃)^3-((a₁*x₂+a₁*x₃-y₂+a₁*a₂-a₃)*(x₂-x₃)^3+(2*x₂+x₃-a₁^2+a₂)*(x₂-x₃)^2*(y₂-y₃)-2*a₁*(x₂-x₃)*(y₂-y₃)^2-(y₂-y₃)^3))*(x₁*(x₂-x₃)^2-((-x₂-x₃-a₂)*(x₂-x₃)^2+a₁*(x₂-x₃)*(y₂-y₃)+(y₂-y₃)^2))*(x₂-x₃)-(a₂*(x₂-x₃)^2+x₁*(x₂-x₃)^2+((-x₂-x₃-a₂)*(x₂-x₃)^2+a₁*(x₂-x₃)*(y₂-y₃)+(y₂-y₃)^2))*(x₁*(x₂-x₃)^2-((-x₂-x₃-a₂)*(x₂-x₃)^2+a₁*(x₂-x₃)*(y₂-y₃)+(y₂-y₃)^2))^2)*((-x₁-x₂-a₂)*(x₁-x₂)^2+a₁*(x₁-x₂)*(y₁-y₂)+(y₁-y₂)^2-x₃*(x₁-x₂)^2)^2*(x₁-x₂)^2 := by
  polyrith -- should work

[David Ang]

This is only the "generic" case where no two points in {P, Q, R, P + Q, Q + R} share the same x-coordinate.

[David Ang]

Sage agrees with me:

P.<x1, x2, x3, y1, y2, y3, a1, a2, a3, a4, a6> = QQ[]
h1 = y1^2+a1*x1*y1+a3*y1-(x1^3+a2*x1^2+a4*x1+a6)
h2 = y2^2+a1*x2*y2+a3*y2-(x2^3+a2*x2^2+a4*x2+a6)
h3 = y3^2+a1*x3*y3+a3*y3-(x3^3+a2*x3^2+a4*x3+a6)
h = (((a1*x1+a1*x2-y1+a1*a2-a3)*(x1-x2)^3+(2*x1+x2-a1^2+a2)*(x1-x2)^2*(y1-y2)-2*a1*(x1-x2)*(y1-y2)^2-(y1-y2)^3-y3*(x1-x2)^3)^2+a1*((a1*x1+a1*x2-y1+a1*a2-a3)*(x1-x2)^3+(2*x1+x2-a1^2+a2)*(x1-x2)^2*(y1-y2)-2*a1*(x1-x2)*(y1-y2)^2-(y1-y2)^3-y3*(x1-x2)^3)*((-x1-x2-a2)*(x1-x2)^2+a1*(x1-x2)*(y1-y2)+(y1-y2)^2-x3*(x1-x2)^2)*(x1-x2)-(a2*(x1-x2)^2+((-x1-x2-a2)*(x1-x2)^2+a1*(x1-x2)*(y1-y2)+(y1-y2)^2)+x3*(x1-x2)^2)*((-x1-x2-a2)*(x1-x2)^2+a1*(x1-x2)*(y1-y2)+(y1-y2)^2-x3*(x1-x2)^2)^2)*(x1*(x2-x3)^2-((-x2-x3-a2)*(x2-x3)^2+a1*(x2-x3)*(y2-y3)+(y2-y3)^2))^2*(x2-x3)^2 - (((y1*(x2-x3)^3-((a1*x2+a1*x3-y2+a1*a2-a3)*(x2-x3)^3+(2*x2+x3-a1^2+a2)*(x2-x3)^2*(y2-y3)-2*a1*(x2-x3)*(y2-y3)^2-(y2-y3)^3))^2+a1*(y1*(x2-x3)^3-((a1*x2+a1*x3-y2+a1*a2-a3)*(x2-x3)^3+(2*x2+x3-a1^2+a2)*(x2-x3)^2*(y2-y3)-2*a1*(x2-x3)*(y2-y3)^2-(y2-y3)^3))*(x1*(x2-x3)^2-((-x2-x3-a2)*(x2-x3)^2+a1*(x2-x3)*(y2-y3)+(y2-y3)^2))*(x2-x3)-(a2*(x2-x3)^2+x1*(x2-x3)^2+((-x2-x3-a2)*(x2-x3)^2+a1*(x2-x3)*(y2-y3)+(y2-y3)^2))*(x1*(x2-x3)^2-((-x2-x3-a2)*(x2-x3)^2+a1*(x2-x3)*(y2-y3)+(y2-y3)^2))^2)*((-x1-x2-a2)*(x1-x2)^2+a1*(x1-x2)*(y1-y2)+(y1-y2)^2-x3*(x1-x2)^2)^2*(x1-x2)^2)
h in ideal(h1, h2, h3) -- True

[Riccardo Brasca]

what are the coefficients of linear_combination?

[David Ang]

They're massive but you can get them by h.lift(ideal(h1, h2, h3)) in Sage

[Riccardo Brasca]

Thanks

[Riccardo Brasca]

OK, they're bigger than I though :open_mouth:

[David Ang]

The polynomials in each side have 25404 terms, and I think the linear combination coefficients each have over 10000 terms.

[David Ang]

If you'd like, you can first polyrith the baby case where a1=a2=a3=a4=0 and maybe a6=1

[Kevin Buzzard]

Riccardo Brasca said:

OK, they're bigger than I thought :open_mouth:

Yes this is exactly the problem

[Riccardo Brasca]

David Ang said:

If you'd like, you can first polyrith the baby case where a1=a2=a3=a4=0 and maybe a6=1

I get an error (the same) even in this case.

[Riccardo Brasca]

Let me see what sage thinks

[Riccardo Brasca]

OK

import Mathlib

example {x1 x2 x3 y1 y2 y3 : ℚ}
    (h₁ : y1 ^ 2 = x1 ^ 3)
    (h₂ : y2 ^ 2 = x2 ^ 3)
    (h₃ : y3 ^ 2 = x3 ^ 3):
    ((-(y1*(x1-x2)^3)+(2*x1+x2)*(x1-x2)^2*(y1-y2)-(y1-y2)^3-y3*(x1-x2)^3)^2-((-x1-x2)*(x1-x2)^2+(y1-y2)^2+x3*(x1-x2)^2)*((-x1-x2)*(x1-x2)^2+(y1-y2)^2-x3*(x1-x2)^2)^2)*(x1*(x2-x3)^2-((-x2-x3)*(x2-x3)^2+(y2-y3)^2))^2*(x2-x3)^2=((y1*(x2-x3)^3-(-(y2*(x2-x3)^3)+(2*x2+x3)*(x2-x3)^2*(y2-y3)-(y2-y3)^3))^2-(x1*(x2-x3)^2+((-x2-x3)*(x2-x3)^2+(y2-y3)^2))*(x1*(x2-x3)^2-((-x2-x3)*(x2-x3)^2+(y2-y3)^2))^2)*((-x1-x2)*(x1-x2)^2+(y1-y2)^2-x3*(x1-x2)^2)^2*(x1-x2)^2 := by
  sorry
  --polyrith -- should work

gives the same error, but the term have a reasonable size, at least in sage

[Nicolas Rolland]

Patrick Massot said:

I don’t understand what happens to our world. You are the second person in this thread to claim to be Italian but still recommends having a pizza in France. What’s going on?? What will be next? Pastas in France?

The very real, sensitive and important issue of mediocre pizzas in Paris requires me to issue the following recommendations :

• Pizza Chic (https://www.pizzachic.fr -- 13 rue de Mezieres, Paris, FR 75006)
• Restaurant Marzo (https://www.marzo-paris.com) (5, Rue Paul-Louis Courier, 75007 Paris -- 84 rue Lauriston, 75116 Paris -- 1 rue du Champ-de-Mars, 75007 Paris)

I am sorry to see that I missed this meetup.. Hope there will be other occasion like that !

[Patrick Massot]

I am sure there will be other opportunities. And we know we missed some people. The organization was not perfect but we tried to be reactive to Joachim's message.

[Filippo A. E. Nuccio]

I cannot resist to also add this to the list, by far my favorite one so far in Paris: Pizzeria Gemma, 63 rue Traversière, 75012.

[Joachim Breitner]

gives the same error, but the term have a reasonable size, at least in sage

Ok, had a look. The resulting call to linear_combination has a size of 23MB. I’m not sure if I call that reasonable :-)

When you say “at least in sage”, are the terms there smaller? In other words, does it explode already before we emit the linear_combination syntax, or is that size unavoidable?

To scale this up to larger proofs one probably has to do something similar to how the sat-integration in bv_decide works, where you can store the certificate in a separate file that then read back in a tactic (replacing linear_combination) and a fair amount of engineering that this file can be parsed and checked efficiently.

With the current design I don’t think there is an easy fix to scale it to such large terms.

[Riccardo Brasca]

Putting some the variables equal to 1 (I don't remember how many, maybe 2) I got the point where the coefficients where, say, 200 terms each, so I can really copy/paste them in Lean.

[Riccardo Brasca]

But writing let A := ... gave a deep recursion error.

[Joachim Breitner]

Not doubting that smaller examples produce just-about-manageable proof terms. Just worried that the overall approach here is unlikely to scale well.

[Patrick Massot]

Our very informal and sporadic formal math seminar will have a session next Monday, March 3rd at 1:30pm in room 1A14 of building 307 in Orsay. We’ll listen to Florent Hivert talking about Coq-combi.

[Philippe Duchon]

Patrick Massot said:

Our very informal and sporadic formal math seminar will have a session next Monday, March 3rd at 1:30pm in room 1A14 of building 307 in Orsay. We’ll listen to Florent Hivert talking about Coq-combi.

Is this purely "in person", or are there plans for an online access?

[Patrick Massot]

In person, sorry.

[Luigi Massacci]

Besides, given the state of the wifi lately, the latency of a train journey would have been lower than that of the video…

[Philippe Duchon]

That might depend on the starting point of the train journey. In my case (Bordeaux), this would have become a full-day trip - not to mention, a bit expensive.

(Of course it would still be shorter than from many other locations across the world)

[Patrick Massot]

We should try to organize a next talk in Orsay. We know we need to listen to Anatole about https://arxiv.org/abs/2501.15639. He cannot talk before March 31st, so it would be nice to do something in the mean time. One possible topic is to continue the meta-programming series that we started a while ago (we did only one meeting about this, so it will be rather easy to catch up for people who didn’t get the first talk). I think it’s good to keep the early Monday afternoon slot which works for many people. I created a poll at https://evento.renater.fr/survey/lean-talks-in-orsay-2d8lamsl to see which Mondays are good in the near future. Don’t hesitate to participate if you would come to Orsay on those dates. You can also post messages here saying you could give a talk, or simply request topics you would find interesting.

[Filippo A. E. Nuccio]

I guess you won't be able to be there on April 21st, given you're supposed to be in :flag_india:

[Patrick Massot]

I know, but people are allowed to meet in Orsay even when I’m not there.

[Antoine Chambert-Loir]

I plan to attend Thierry Coquand's lectures at Collège de France that will take place Mondays, 10-12 am, starting next week. So I won't be able to go back to Orsay.

[Ayhon]

Same

[Michael Rothgang]

In case you'd like to think about the medium term: I will be in Orsay from mid-June until mid-July, and I'm happy to speak about e.g. formalisation of bordism theory, or perhaps Riemannian metrics/whatever Patrick and I will be working on.

[Patrick Massot]

Yes, we will definitely use you in June.

[Patrick Massot]

Antoine Chambert-Loir said:

I plan to attend Thierry Coquand's lectures at Collège de France that will take place Mondays, 10-12 am, starting next week. So I won't be able to go back to Orsay.

This can be a good reason to change the schedule a bit. Would it be better to use the end of the afternoon in Orsay?

[Antoine Chambert-Loir]

Actually, I wouldn't be available neither, and I have an awful load of teaching, so maybe you'll better do without me.

[Patrick Massot]

For everybody near Paris: https://www.college-de-france.fr/en/agenda/opening-lecture/type-theory-from-russell-to-demonstration-assistants/type-theory-from-russell-to-demonstration-assistants is today.

[Damien Carré]

Hello. I found there is a team at Saclay there: https://leanprover-community.github.io/meet.html . It is very near from my home. I am wondering if I could meet them in real life during a lean real life event. How could I contact them please? I am starting lean.

[Yaël Dillies]

Hey! I would suggest posting in #Geographic locality > Paris area, France :smile:

[Notification Bot]

2 messages were moved here from #Geographic locality > irl team at Saclay by Mario Carneiro.

[Damien Carré]

thanks

[Damien Carré]

Hello. I found there is a team at Saclay there: https://leanprover-community.github.io/meet.html . It is very near from my home. I am wondering if I could meet them in real life during a lean real life event. How could I contact them please? I am starting lean.

[Kevin Buzzard]

Is there a Paris meeting coming up?

[Patrick Massot]

Good question. The poll at https://evento.renater.fr/survey/lean-talks-in-orsay-2d8lamsl was not very successful. For instance @Joël Riou and @Damien Thomine did not answer.

[Patrick Massot]

I think we will have a talk on March 31st by Anatole.

[Patrick Massot]

@gogo gogo, the first step if you are serious about wanting to meet real people is to use your real name and tell us a bit more about you.

[Damien Carré]

Yes sorry. Could we create a private place to fill my real identity please? :)

[Julian Berman]

(FYI posting that link has now shared both your name and email publicly, and even editing it in Zulip will not redact that -- which hopefully you don't feel bad about, but maybe now that's impetus enough to at least now update your zulip name to be your real one :)!

[Damien Carré]

what??? I never consented to!

[Damien Carré]

where is the place to got at monday 24 please?

[Johan Commelin]

@gogo gogo I have deleted your message, because you clearly did not intend to post something that discloses your identity.

[Johan Commelin]

Nevertheless, this community encourages the use of real names.

[Patrick Massot]

There will be no talk in Orsay next Monday because at 2:30pm several people will remotely attend @Emilie Uthaiwat masters thesis defense about Lean’s type theory. This is a great opportunity to get explanations about Mario’s paper.

[Emilie Uthaiwat]

Thank you for your interest in my presentation! I will focus on the second section "The axioms" and adopt a bottom-up approach to present some notions in type theory (starting from the untyped lambda calculus or directly from system T). I will also try to expand on some differences with Rocq (quotient types vs setoids, "propositional lifting", etc).

[Ching-Tsun Chou]

Will this presentation be recorded and made available online?

[Emilie Uthaiwat]

I'm not planning to record it or to make it available online. I'm sorry about this.

[Damien Carré]

Great idea! Can i get the link

[Damien Carré]

no problem. Any link for the next conf?

[Patrick Massot]

No.

[Patrick Massot]

Reminder: we will have at talk tomorrow by Anatole Dedecker about the continuous functional calculus in Lean. This will be 2025-03-31T13:30:00+02:00 in the usual room.

[Patrick Massot]

(beware we just switched to summer time in France)

[Damien Carré]

Can i have the address please ;) ?

[Joël Riou]

https://www.imo.universite-paris-saclay.fr/fr/acces/
This will be in room 1A14.

[Damien Carré]

13h30 demain à l ups?

[Damien Carré]

Hello people. [TRUNCATED MESSAGE BY the author to seem less rude]

[Damien Carré]

I am wondering if i could have a clear answer @Joël Riou please ?

[Johan Commelin]

Sorry, I find your message very hard to parse. But people have indeed repeatedly encouraged you to use your full name.

[Patrick Massot]

We clarified the situation in private. But I think it’s good to make something explicit for the benefit of other readers. This Zulip chat instance is a public website. We strongly encourage people to use their real names, but this is not enforced. The situation at a university is different. Our building and our activities are not open to people who have nothing to do with the university (not working or studying there), and are not invited by university employees. The laboratory director is legally responsible for people who are in the building. He doesn’t want members of the department to allow everybody entering the building. As the organizer of this seminar I cannot simply say this is a fully public event without declaring it as such (with different rules applying).

Also, this informal seminar is still a professional mathematics seminar. The talk today was not mathematically accessible to people who do not have at least four years of pure math university courses.

[Damien Carré]

Hello @Patrick Massot and thank you for the great previous meeting!

As mentinned in private, the issue has been solved. I did not realized that people used to be afraid of anynymous users. I decided to put my name public in this chat as that as mentionned in private, contrary to ingeeneering people, it is not commonly agreed by researcher communities to allow anonymous users.

Then I decided to put my name public. My personal disconfort must not impact the community ambiance.

Once again, sorry for the big inconvenience. And once again thank a lot of to @Patrick Massot for his patience. I will do my best to be more vigilant next time.

Best regards.

[Filippo A. E. Nuccio]

Is there anything in sight on 2025-04-07T13:30:00+02:00 ?

[Patrick Massot]

No, there isn’t.