Antoine de Saint Germain

Stream: new members

[Antoine de Saint Germain]

Hi all, Antoine here from the University of Hong Kong. I’ve just come back from a workshop in Singapore about Lean, and am interested in getting my « hands dirty » with Lean ! I
I am hoping to reach the stage where I can formalise 1) cluster algebras, 2) anything Lie-theoretic.

[Johan Commelin]

Welcome! Some of us are working on a project to Leanify the classification of fd semisimple Lie algebras: https://github.com/orgs/leanprover-community/projects/17

[Yuma Mizuno]

This is a very late message, but please allow me to send it.

I'm happy to see someone interested in cluster algebras on Zulip. I'm a very enthusiastic follower of this topic as well (Actually, I came across your name in your new arXiv paper about cluster algebras).

It might not be useful anymore, but I have a repository where I previously formalized cluster algebra in Lean 3. I only made definitions without proving anything, so please note that I didn't properly verify that the definition is "correct".

[Derek Rhodes]

@Yuma Mizuno, by the way, the link to your repository seems to be malformed :thinking:

[Yuma Mizuno]

correct url: https://github.com/yuma-mizuno/lean-cluster-algebra

[Aaron Liu]

You can just edit the original message