São Carlos, Brazil

Stream: Geographic locality

[Lua Viana Reis]

By lack of proof witness I feel I'm the only one tinkering with lean here at ICMC, so if you are around and we don't know each other let's have a coffee and say hi!

[Oliver Butterley]

@Daniel Smania is also tinkering with lean and is more or less in the region (I’m not sure of the precise arrangement of ICMC, USP and Uni Campinas).

[Lua Viana Reis]

oh hi @Daniel Smania. I plan to watch your course next semester, so we may have a lot of hi s

[Lua Viana Reis]

Oliver Butterley said:

I’m not sure of the precise arrangement of ICMC, USP and Uni Campinas

$\textsf{Lua} \in \textsf{ICMC} \subseteq \textsf{USP campus} \subseteq \textsf{São Carlos}$

but

$\textsf{Unicamp} \cap \textsf{São Carlos} = \varnothing$

[Daniel Smania]

Hi @Lua Viana Reis @Oliver Butterley Yep, I'm working on some Lean4 code related to my research on Besov spaces, Haar wavelets, and transfer operators. I find it interesting because the ideas are somewhat elementary, which I believe makes them more amenable to formalization in Lean4. Still, it’s been quite challenging. So far, what I’ve managed to formalize (and uploaded to GitHub) is a very basic result about laminar families—a concept from combinatorics that I need in order to define Haar wavelets on measure spaces.

[Oliver Butterley]

Lua Viana Reis said:

Oliver Butterley said:

I’m not sure of the precise arrangement of ICMC, USP and Uni Campinas

$\textsf{Lua} \in \textsf{ICMC} \subseteq \textsf{USP campus} \subseteq \textsf{São Carlos}$

but

$\textsf{Unicamp} \cap \textsf{São Carlos} = \varnothing$

That's a beautiful explanation!!!! But am I correct in things that Unicamp lies geographically between Sao Carlos and Sao Paulo?

[Paul Schwahn]

Hi all! I'm not in São Carlos, but in Campinas; we have a small group at Unicamp who is working on Lie algebras in Lean. I'd be happy to meet when there is an opportunity!