Alexander Kurz

Stream: new members

[Alexander Kurz]

I am new to Lean and interested in two related topics. 1) Is Lean suitable to teach an introduction to logic for software engineers? Any experience with this? 2) Do large language models (such as GPT-4=) help to learn using a proof assistant? Again, i'd be interested if somebody used LLMs for teaching Lean, in particular to computer science undergrads.

[Johan Commelin]

Welcome! (I moved your post to a new thread.) You might be interested in the #Lean for teaching stream, although it has a bit of a focus on teaching maths. But various courses have been taught about "Lean for CS" and a logic course for CS students would certainly be in scope.

[Johan Commelin]

Concerning (2), I don't think people have experimented in the direction of using LLMs for teaching Lean. My gut feeling is that it is too early for that. But I'm far from an LLM expert.

[Alexander Kurz]

Thanks, Johan. Over the last few weeks, I learned that AIs are a powerful tool to teach and learn a new programming language. I taught myself several languages I did have zero experience in. So in principle proof assistants should be in scope. Currently I am experimenting with Isabelle, Lean and Idris. And I was wondering whether somebody here has some experience with this approach to teaching and learning.