Let's code math | Lean4 | Theorem prover

[@splience]

Feel free to explore our code and a LaTeX document on GitHub: github.com/Splines/lean-continuous

[@Filup]

I plan to watch this in the morning, but heck, I LOVE Lean. I am so looking forward to this. I have wanted to learn lean for years!

[@Miguel_Noether]

It's already the morning

[@kingarth0r]

I LOVE LEAN

[@netherlandsjesse]

I really like this level of detail for explaining how to do proofs in Lean

[@98danielray]

your lean proofs are really clean. the way you use tactics to translate natural language into lean statements is intuitive in a way I had not seen before when playing around with it

[@null_s3t]

Your videos are so high quality, I can’t help myself! Subscribed

[@splience]

Thank you ;) It's great to hear that the efforts taken to ensure quality are recognized. On the flipside, (Quality > Quantity) is why I also take so long to produce new videos...

[@fburton8]

A small point: “irregardless” is considered an incorrect portmanteau of “irrespective” and “regardless”. Irregardless, I really enjoyed the video!

[@splience]

Ups, thanks for pointing that one out, didn't know that! (Me not being a native English speaker, there's probably more such errors that I make, feel free to highlight these in future videos as well 😅)

[@fburton8]

@@splience No worries! 😀It's a common 'error' made by native English speakers, but one that doesn't hamper understanding.

[@cheukchan2968]

even since I learned some type theory, I have long been interested of using computer to check a mathematical proof. And this is a nice intro to Lean

[@timurpryadilin8830]

we need more videos about lean !!! maybe you can do some interesting number theory or group theory next ?

[@splience]

Hey, thanks ;) I'm not particularly interested in number theory, so you will probably not see a video from me on that. Also not sure, if I will make more Lean videos, but let's see ;) Next videos will probably be something in algebraic topology and I have ideas for some other topics as well, stay tuned.

[@holery9215]

Another great video i found in this morning 🌅

[@ai_serf]

awesome... i hope to one day use lean4 to help me in demonstrate my real analysis proofs in code.

[@tsepten7930]

top tier explanations

[@korigamik]

I loved the video. Can you tell what all tools did you use to create, edit manage these animations? Maybe you can share the source code for the video itself as well ❤

[@splience]

Thanks ;) I used PowerPoint to animate everything, OBS to screen-record it and DavinciResolve to edit it and record the audio. Other great tools include Blender and GeoGebra.

[@korigamik]

@@splience how do you include latex in power point? Also how do you sync the videos to your voice and change slides at the same time? Appreciate the quick response btw

[@splience]

@@korigamik I use the great IguanaTex plugin by Jonathan-LeRoux for LaTeX in PowerPoint. With regards to synchronisation: For this video I've recorded the audio while clicking around in the presentation (and recording it), then edited the video and audio (in DavinciResolve). Later, I rerecorded parts (just the screen) where I missed clicks or where they were not well-aligned with my speech. It's a back and forth and there are many ways to do it.

[@vlynn5695]

This was an incredible Video!!!

[@Filup]

This is excellent! I really want to get back into learning Lean now that Lean 4 has been released! Are there any good tutorials or tutorial series you would recommend? I might retry my hand at it over xmas. Thanks for your videos. They are very high quality! Also, I don't suppose you have a discord server or anything for this channel?

[@splience]

Thanks ;) The Lean Community provides a website with links for resources to learn Lean4 here: leanprover-community.github.io/learn.html E.g. the natural number game is a great place to start and learn the basics: adam.math.hhu.de/#/g/leanprover-community/NNG4 With regards to the discord server: no, I don't have anything like that since I currently work on KZbin videos just for fun in my spare time. Maybe something to keep at the back of my head for the future.

[@Filup]

@@splience Thanks! I actually do remember the NNG, but I'm not sure if I ever did it. I'll have to give it a go. No issues about not having a discord or anything. It can be a pain to moderate, but being able to talk math with people of similar interests is fun.

[@aremathukr]

The topic and explanations are great, but man, I am so fascinated by the animations and the design of the video. Can you tell what software did you use? Thanks!

[@splience]

Thank you ;) For the tools I've used, see the video description. The animations themselves are all done in PowerPoint.

[@aremathukr]

​@@splience Thanks! )

[@xxnotmuchxx]

Is there a wall of all theorems in Lean? Would be interesting to see if I can learn some math and Lean at the same time from reading proofs.

[@splience]

I mean you could browse through the Mathlib4 code ( github.com/leanprover-community/mathlib4/tree/master/Mathlib ). Just be aware that this code is sometimes very dense and advanced users of Lean4 write it. But still a good idea to just give it a try and see if it actually eases understanding proofs. But it's maybe easier to understand if one has already seen the proof laid out in a "hand-written" form. If you browse through the code, you'll probably want to do so in VSCode using the Lean4 extension such that you can see the goal to solve at every step.

[@xxnotmuchxx]

@@splience Oh, would be nice if it started from the axioms.

[@maelstrom254]

Subscribed. What is your approach to learn Lean from ground up?

[@splience]

I'd suggest to first get acquainted with the basic syntax and see how simple proofs could look like. A good place to start could be the natural number game: adam.math.hhu.de/#/g/leanprover-community/NNG4 or even this video ;) Beyond that, the Lean Community provides a website with links for resources to learn Lean4 here: leanprover-community.github.io/learn.html Doing your own projects is also a good idea as that's probably where you learn most. "What I cannot create, I do not understand" - Richard Feynman.

[@maelstrom254]

@@splience thank you! 🙏

[@attiladren6990]

Thank you, Thank you, .... (1000x). This is a wonderful explanation and amazing visualization. May I ask what programs you used to create the video?

[@attiladren6990]

Sorry. In the comments, I see that you have already provided the answer to this question before.

[@splience]

​@@attiladren6990 Thank you. I've just added the tools I used in the video description since others might ask as well ;) Also see my video "Your tools are good enough": kzbin.info/www/bejne/qZKqinymrNODd6M

[@YuruCampSupermacy]

Lessssgo

[@robfielding8566]

Claude is much better with Lean4 than ChatGPT, which is confused by Lean3.