Zulip Chat Archive

Stream: new members

Topic: Heather Macbeth (introduction)

Heather Macbeth (May 07 2020 at 16:22):

Hi, I am a differential geometer (Kähler and conformal geometry in particular). I have been experimenting with Coq for a while -- actually I assigned some optional Coq exercises to my undergraduate real analysis students last semester, and learned a lot myself in the process. I am excited to try Lean! At the moment I am doing Patrick Massot's tutorials (with an eye to adapting them for my own teaching), and learning my way around mathlib.

Johan Commelin (May 07 2020 at 16:48):

Cool! Some point far in the future, I would love to have Hodge theory in mathlib... we are currently in the process of getting complex analytic manifolds (and many other kinds of manifolds). So it's still far in the future. But it's a dream!

Patrick Massot (May 07 2020 at 17:00):

Welcome! I'd be very curious to see your Coq exercises. If you ever to contribute to mathlib, there is a lot to do in differential geometry, only the very first definitions are there.

Last updated: Dec 20 2023 at 11:08 UTC