Hong Kong

Stream: Geographic locality

[Moin Ahmed Qidwai]

Hi All,
Anyone else from Hong Kong here?

[Kenny Lau]

me and @Shing Tak Lam I believe

[Moin Ahmed Qidwai]

Awesome!
Have you been using Lean for long? Just playing or using it for some projects?

[Kenny Lau]

I have been using Lean for 3 years and I contribute to mathlib.

[Moin Ahmed Qidwai]

That is great. Maybe we could have a meetup in Hong Kong once the Covid situation levels off a bit.

[Kenny Lau]

for now you can join the discord server!

[Shing Tak Lam]

Kenny Lau said:

me and Shing Tak Lam I believe

I'm indeed from HK but I can't go back atm :(

[Antoine de Saint Germain]

Anyone in HK and eager to get a study group ?

[Jam Kabeer Ali Khan]

Hey! sure

[Yang Ming-Tian]

Antoine de Saint Germain said:

Anyone in HK and eager to get a study group ?

:wave:

[Shen Kaizhe]

Sure lol

[Jon Cheah]

Hello!

[Antoine de Saint Germain]

Little reminder that today at 2pm HKT we have our weekly Lean workshop in HKU. Anyone and everyone welcome ! We'll be working on formalising frieze patterns (c.f. https://github.com/Antoine-dSG/frieze_patterns)

[Antoine de Saint Germain]

Our regular meeting are happening again ! In HKU, every Wednesday from 3pm to 5pm, in Room 102 of Elliot Hall. Everyone is welcome

[Laurance Lau]

Ah, just learned about this thread. Unfortunately leaving Sunday night...