Beijing, China

Stream: Geographic locality

[ZHAO Jinxiang]

Hi All,
Anyone else from Beijing here?

[Qian Hong (wechat: fracting)]

Hi Jinxiang! I am a Chinese in Sydney, there's a Wechat group for formal verification, please join me :)

[Qian Hong]

update:

my WeChat ID is fracting, anyone who wants to join the WeChat group please connect me on WeChat and I'll invite you to the group. Feel free to read https://docs.qq.com/doc/DVUhUdFFQWlJYelBH for some samples of group chat history.

Cheers!

[Yao Liu]

Hi, anyone in Beijing who wants to learn Lean, let's form a study group.

[Junyan Xu]

I'll attend an informal Lean workshop at PKU from Feb 12 to 16 and I'm arriving on Feb 11. I'm told that people are working on dimension theory there, but hopefully I might also have an opportunity to lead projects on group schemes and/or covering spaces.
cc @Jz Pan since your GitHub profile says you're in the city :)

[Jz Pan]

Junyan Xu said:

I'll attend an informal Lean workshop at PKU from Feb 12 to 16 and I'm arriving on Feb 11. I'm told that people are working on dimension theory there, but hopefully I might also have an opportunity to lead projects on group schemes and/or covering spaces.
cc Jz Pan since your GitHub profile says you're in the city :)

No, In fact now I'm working at Shanghai :man_facepalming: Let me see if I can go Beijing at that time, but nothing can be guaranteed...

[Jz Pan]

As far as I know, at least there are people at Peking University, Renmin University, and AMSS, CAS working on Lean.

[Jz Pan]

(no Tsinghua University now)

[Junyan Xu]

I was told by the abaka.AI people that Tsinghua students have been helping them ...

[Y Yan]

@Junyan Xu Hi, I am a student at Tsinghua and am interested in Lean (not really working on Lean). I wonder whether there is a chance for me to attend the workshop you mentioned.

[Junyan Xu]

cc organizer: Jiang Jiedong

[Jiang Jiedong]

Hi @Y Yan ,
You are welcomed to the Lean workshop at PKU. However, the topic of this workshop is about meta-programming and collaborative work on projects on commutative algebra, which may not be the most suitable for beginners. Nevertheless, we warmly welcome your participation if you're interested.

[Y Yan]

@Jiang Jiedong Thank you! I am interested in joining. Where should I find the information about this workshop (location and schedule)?

[Jiang Jiedong]

Hi @Y Yan ,
There is no official website for this workshop. I'll send the information to you in DM.

[Ping J]

Hi! Are there groups in Beijing (or within 3 hours of flight really) working on Lean4 projects that I can join offline this summer?

I'm interested in Lean itself, but would also gladly work on any math I understand.

or just go our for a coffee and chat?

as a brief self-intro, my long-ish time ambitions are

1. to make lean-proof as easy as paper proof; user only provide key steps (milestone statements) and everything else is automated away
2. develop an AI system that base entirely on structural learning (no LLM involved) and see where that goes