Zulip Chat Archive

Stream: new members

Topic: Alexander Kurz

Alexander Kurz (Sep 29 2023 at 20:02):

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 (Sep 29 2023 at 20:05):

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 (Sep 29 2023 at 20:07):

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 (Sep 29 2023 at 20:56):

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.

Last updated: Dec 20 2023 at 11:08 UTC