Zulip Chat Archive

Stream: new members

Topic: Alex Rogovskyy

Alex Rogovskyy (Jun 28 2022 at 13:13):

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 (Jun 28 2022 at 13:13):

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

Alex Rogovskyy (Jun 28 2022 at 13:15):

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.

Last updated: Dec 20 2023 at 11:08 UTC