Intro: Elisabeth Bonnevier

Stream: new members

[Elisabeth Bonnevier]

Hi!
My name is Elisabeth Bonnevier and I am a PhD student at the University of Bergen, Norway. My research is in Homotopy Type Theory and I spend much of my time formalising in Agda. This semester I want to have a couple of hands-on 'introduction to computer formalisation' sessions for the mathematics students at the university. I want to make it as useful and as simple as possible, without having to teach them much type theory. Thus I thought that tactics based formalisation in Lean would be the best alternative. So I have jumped on here because I frequently have questions as I am trying to learn it :smiling_face:

[Patrick Massot]

If you target maths then you should probably stick to Lean 3. The maths library of Lean 4 isn't ready yet.