Learning To Code In Lean 4 With A Friend: Starting Out

My friend Avi Cramer and I start learning the Lean 4 functional programming language. This time we cover the basics like installing the language, evaluating arithmetic expressions, type checking and function definitions. The plan is to build towards more advanced topics like recursion, dependent type theory and theorem proving.
Installation:
lean-lang.org/lean4/doc/quick...
The Lean book we are following:
lean-lang.org/functional_prog...
This video covers 1.1 to 1.3 in the book.
Avi's Website:
avicraimer.com/
Avi's KZbin:
• TypeScript Type Theory...

[@rhodesd]

Avi and Richard, thank you for taking the time to make this video, please keep going!

[@RichardSouthwell]

Thank you! Will do!

[@avi3681]

Super fun making the video with you!

[@RichardSouthwell]

yea, making this was 100% fun

[@jacksonstenger]

My friend just mentioned Lean to me the other day, it sounds very exciting, hope you guys continue to explore the language!

[@RichardSouthwell]

Yes it is exciting, and we shall certainly continue our exploration !

[@jamesgood7894]

Watched some of your category theory videos in the past and was surprised to find this recently posted. Not sure if it is something you’d be interested in covering after you’ve touched on everything you already have planned, but it would be great if you could also cover just using the language for some general purpose programming (potentially even showing how to pull in some Rust libraries). edit: I only read the description when I posted this, but after listening to the first five minutes, it sounds like general purpose programming is what you two intend to cover here. Nonetheless, interoperability with Rust in order to leverage existing libraries would be beneficial, so hopefully that can be touched upon in future videos if it is possible.

[@ShakilAhmed-ro4ki]

I tried lean a few days back 😊 . Would love to see more on this.

[@RichardSouthwell]

Yea, its great if this resource will help you

[@Nolrai12]

the lean 4 version of Mathlib is actually pretty well along by now, I haven't run into anything missing from it yet!

[@RichardSouthwell]

That's good news. It seems like we are learning Lean 4 at the right time

[@avi3681]

Thanks for the correction, I realized after we recorded this that my info on the MathLib upgrade was out of date.

[@RichardSouthwell]

@@avi3681 Its good timing for us to do this as Mathlib is becoming available

[@friedporkrice]

I really enjoyed following along on my own in VSCode with lean4, thank you, and what a great idea. I wonder if this "pair learning" format would work well for your other topics too.

[@RichardSouthwell]

Yes. It's a good idea. Actually I've got something like that in the pipeline

[@davidchristiansen8582]

This is a great video - thank you for making it!

[@RichardSouthwell]

And thank you for writing the book we are following 😀

[@davidchristiansen8582]

And thank you for reading it so carefully 🙂 That's the greatest joy for a writer.

[@hebozhe]

I developed and plan to rebuild a Fitch solver, so of course I'd run into Lean. Good to know it's not terribly esoteric.

[@user-ed3bs1vq8b]

8:30

[@pmosh1]

The News today brought me here