Yuri Sulyma

Stream: new members

[Yuri Sulyma]

Hi, I'm Yuri. I'm a mathematician working in homotopy theory (adjacent to a little bit of the condensed stuff). I'm also the developer of Liqvid, a tool for making interactive videos for teaching math/coding; I'm hoping this could be used for interactive Lean tutorials. I played around with Lean at a HoTT workshop several years ago, but haven't kept up with it.

[Ruben Van de Velde]

I have no idea what any of those words mean, but welcome!

[metakuntyyy]

Well, I always get an existential dread when I read category theory, so you're not alone. Welcome @Yuri Sulyma

[Kevin Buzzard]

Can you make a short video explaining a roadmap to formalising prismatic cohomology in lean? Maybe start by discussing the definition here and the community can say what we already have

[Yuri Sulyma]

@Kevin Buzzard to clarify, I'm not trying to formalize prismatic cohomology in Lean (at this time). I'm interested in extending my animation software to record interactive Lean videos (about much more elementary topics).

[Niels Voss]

You might want to consider getting in touch with @David Thrane Christiansen, who is writing the reference manual and verso, which is sort of like a supercharged version of markdown or mdbook designed for Lean. Not sure if there's any overlap, but it might be worth checking.