Vietnam

Stream: Geographic locality

[Huỳnh Trần Khanh]

Hmm... Are there Lean users in Vietnam? Just wondering.

[Huỳnh Trần Khanh]

Except me of course :rolling_on_the_floor_laughing::joy:

[Huỳnh Trần Khanh]

Maybe I should be more lenient and count people of Vietnamese descent too.

[Johan Commelin]

@Mario Carneiro you know some people, right?

[Johan Commelin]

Wasn't there some workshop by Hales in Hanoi at some point?

[Mario Carneiro]

Yes. I mostly worked with folks at the Thang Long university in Hanoi. I recall Hoang Le Truong and Nga Ngo, and Nga Ngo has actually come to several of our CMU/Pitt lean meetings once they went virtual

[Mario Carneiro]

Thales has a lot of connections in Vietnam, since he visits regularly, so he might know more about who is working on lean these days

[Trần Duy Thanh]

I'm a developer and working on LEAN4 as an efficient way to dig deep into proofs in Algebra right now. Does any one know how to keep track the list of on-going proof (that needs to be formalize) that I can contribute?

[Serhii Khoma (srghma)]

rn im in Hanoi

[Scott Buckley]

I am based in Sydney now but I am in Saigon every year to visit family. I'll be there for most of Feb 2026 if anybody wants to meet up.