Alex Rogovskyy

Stream: new members

[Alex Rogovskyy]

Hi! I'm Alex, currently a Master's student and working with Lean at @Laurent Bartholdi 's seminar. I have previous experience with Coq, but just got into Lean recently. Currently, I'm thinking about implementing the Jordan Normal Form theorem (as it's apparently not done yet). Not quite sure yet in what generality I should do it or how difficult it's going to be; probably going to start with a quite specific version. Looking forward to hopefully making a useful contribution to mathlib.

[Kevin Buzzard]

I think @Pierre-Alexandre Bazin has been working on this.

[Alex Rogovskyy]

Ah alright, thanks for telling! I'll think about what other topic to take, or maybe I'll continue on that one just for myself as a learning experience.