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 KZread:
• TypeScript Type Theory...
Пікірлер: 20
Avi and Richard, thank you for taking the time to make this video, please keep going!
@RichardSouthwell
7 ай бұрын
Thank you! Will do!
Super fun making the video with you!
@RichardSouthwell
7 ай бұрын
yea, making this was 100% fun
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.
My friend just mentioned Lean to me the other day, it sounds very exciting, hope you guys continue to explore the language!
@RichardSouthwell
7 ай бұрын
Yes it is exciting, and we shall certainly continue our exploration !
I tried lean a few days back 😊 . Would love to see more on this.
@RichardSouthwell
7 ай бұрын
Yea, its great if this resource will help you
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.
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
7 ай бұрын
Yes. It's a good idea. Actually I've got something like that in the pipeline
the lean 4 version of Mathlib is actually pretty well along by now, I haven't run into anything missing from it yet!
@RichardSouthwell
7 ай бұрын
That's good news. It seems like we are learning Lean 4 at the right time
@avi3681
7 ай бұрын
Thanks for the correction, I realized after we recorded this that my info on the MathLib upgrade was out of date.
@RichardSouthwell
7 ай бұрын
@@avi3681 Its good timing for us to do this as Mathlib is becoming available
This is a great video - thank you for making it!
@RichardSouthwell
6 ай бұрын
And thank you for writing the book we are following 😀
@davidchristiansen8582
6 ай бұрын
And thank you for reading it so carefully 🙂 That's the greatest joy for a writer.
8:30