Heather Macbeth (introduction)

Stream: new members

[Heather Macbeth]

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]

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]

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.