# Zulip Chat Archive

## Stream: new members

### Topic: Intro: Elisabeth Bonnevier

#### Elisabeth Bonnevier (Jan 06 2023 at 10:04):

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 (Jan 06 2023 at 10:46):

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

Last updated: Dec 20 2023 at 11:08 UTC