learnlean
/learnlean7
documents his journey learning the Lean proof assistant
I added some comments to the subset transitivity proof
After a two week hiatus I was considerably rustier, so just a short exercise today to prove the transitivity of subset relations: https://github.com/agostbiro/mathematics_in_lean/commit/16ae0aad2173868f365d147e43b7fee1fa65cc71
Gotta prioritize daily progress no matter what
Gotta prioritize daily progress no matter what
Did a few more exercises in the Logic section of Mathematics in Lean. I like that they're introducing a bit of analysis with monotone and even/odd functions in this section to make it less dry.
The exercises went quickly as I managed to guess the required theorem names the first or second time. This was previously a source of frustration, but it looks like I'm getting the hang of it. The naming is logical.
One interesting bit is that I managed to write a simpler solution than the book for one of the exercises (dark picture is mine and bright is the book). The reason is probably the pattern matching in the rewrite tactic becoming more powerful since the book was written.
https://github.com/agostbiro/mathematics_in_lean/commit/f0e5f3b3d40f3ca7d8b7810f7e58b49d24196021
The exercises went quickly as I managed to guess the required theorem names the first or second time. This was previously a source of frustration, but it looks like I'm getting the hang of it. The naming is logical.
One interesting bit is that I managed to write a simpler solution than the book for one of the exercises (dark picture is mine and bright is the book). The reason is probably the pattern matching in the rewrite tactic becoming more powerful since the book was written.
https://github.com/agostbiro/mathematics_in_lean/commit/f0e5f3b3d40f3ca7d8b7810f7e58b49d24196021
Did some more exercises in the Logic section of the Mathematics in Lean book.[1] These introduced proof terms which are just a series of function applications with a more elegant lambda-like syntax. Proof terms underscore that proofs in Lean are really just functions from types to types that compile.
As a I side note, the annoyance about having to guess theorem names to solve exercises remains. Hopefully I'll get better at this in the future or find better tools to help.
https://github.com/agostbiro/mathematics_in_lean/commit/4aa78ca0f8d8dc4c983b429f5dab26d26b726aa7
As a I side note, the annoyance about having to guess theorem names to solve exercises remains. Hopefully I'll get better at this in the future or find better tools to help.
https://github.com/agostbiro/mathematics_in_lean/commit/4aa78ca0f8d8dc4c983b429f5dab26d26b726aa7
Prof Kevin Buzzard gave a talk[1] at Microsoft in 2019 how he got started with Lean as a teaching tool for undergrads and how he intends to transform modern mathematics by formalizing it with Lean.
There has been a lot of progress in that and he has now a research grant to formalize the proof of Fermat's Last Theorem with Lean.[2]
What was not foreseen at the time of his 2019 talk is that AI researches have adopted Lean for models that generate proofs.[3]
[1] https://www.youtube.com/watch?v=Dp-mQ3HxgDE
[2] https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/
[3] https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
There has been a lot of progress in that and he has now a research grant to formalize the proof of Fermat's Last Theorem with Lean.[2]
What was not foreseen at the time of his 2019 talk is that AI researches have adopted Lean for models that generate proofs.[3]
[1] https://www.youtube.com/watch?v=Dp-mQ3HxgDE
[2] https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/
[3] https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
So I've been following the Mathematics in Lean book which I mostly like, but the exercises are not well designed. To solve the pictured exercise,[1] it gives you a bunch of theorems to use, plus you're supposed to remember a magic incantation (`linarith`) from the previous chapter to solve it. But `linarith` isn't really well explained there, nor is there an exercise to practice its usage.
Removing the hand-wavy magic from math is exactly why I started learning Lean, so instead of taking these as given, I rabbit-holed on how `linarith` and `abs_nonneg` work and added my findings as comments.
And this shows the power of Lean. Just by using jump to source and a bit of Googling, I was able to get a good understanding of how these things work. If this exercise was in a text book presented like this, I probably wouldn't have gotten there.
[1] https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html
Removing the hand-wavy magic from math is exactly why I started learning Lean, so instead of taking these as given, I rabbit-holed on how `linarith` and `abs_nonneg` work and added my findings as comments.
And this shows the power of Lean. Just by using jump to source and a bit of Googling, I was able to get a good understanding of how these things work. If this exercise was in a text book presented like this, I probably wouldn't have gotten there.
[1] https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html
Lean is quite elegant. Multiple if conditions are curried meaning partial application of an implication is a breeze
Did the final three exercises in the Proving Identities in Algebraic Structures section. These involved proving theorems about groups using only the group axioms.
Normally multiplying by the inverse is defined to be commutative in text books, but not here. So the first task was proving that fact. I had to look up the helper lemma for `mul_inv_cancel`, but after that proving the lemma and the theorem + `mul_one` was easy (see pic 1).
The last exercise was proving `(a * b)⁻¹ = b⁻¹ * a⁻¹`. This I'm rather proud of, because I think my solution is more legible than the official one (see pic 2).
Normally multiplying by the inverse is defined to be commutative in text books, but not here. So the first task was proving that fact. I had to look up the helper lemma for `mul_inv_cancel`, but after that proving the lemma and the theorem + `mul_one` was easy (see pic 1).
The last exercise was proving `(a * b)⁻¹ = b⁻¹ * a⁻¹`. This I'm rather proud of, because I think my solution is more legible than the official one (see pic 2).
Did some more proofs and learned the apply tactic which is pretty cool. It lets you change the goal of a proof to proving the hypothesis of something that you've already proved (see pic for example).
I also had a go at proving `theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1` from group axioms (`a⁻¹ * a = 1` is given as an axiom). This was a pretty humbling experience. I thought it was easy and I wrote down two lines on paper as a sketch, but when I expanded it step by step as Lean would want it, it turned out to be wrong. Gonna have a go at a rigorous proof again later.
https://github.com/agostbiro/mathematics_in_lean/commit/62ad33dfef38a29e7cf94e038696adbf6addd647
I also had a go at proving `theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1` from group axioms (`a⁻¹ * a = 1` is given as an axiom). This was a pretty humbling experience. I thought it was easy and I wrote down two lines on paper as a sketch, but when I expanded it step by step as Lean would want it, it turned out to be wrong. Gonna have a go at a rigorous proof again later.
https://github.com/agostbiro/mathematics_in_lean/commit/62ad33dfef38a29e7cf94e038696adbf6addd647
Sat down to get some Lean done before the day starts. Good news is that that the VSCode plugin works again. Turns out it was the old have to accept Xcode CLI tools license after an update issues. After this the toolchain failed to build the mathlib so I had to reinstall that too, but now it all seems to work again. 🙏 No time for proofs though
I had a frustrating time with Lean today.
Did some more exercises, but then the Lean plugin died in VSCode after restarting it to fix a UI issue and I haven't managed to resolve it yet. I asked on Zulip where there seems to be a helpful community.
I then took a peak at the solution for the next exercise and it uses a theorem that hasn't been introduced yet, but the exercise said to only use theorems that have been introduced. 🤷
https://github.com/leanprover-community/mathematics_in_lean/commit/61e9eca92c9c4400e6586b32d274e99db706570a
Did some more exercises, but then the Lean plugin died in VSCode after restarting it to fix a UI issue and I haven't managed to resolve it yet. I asked on Zulip where there seems to be a helpful community.
I then took a peak at the solution for the next exercise and it uses a theorem that hasn't been introduced yet, but the exercise said to only use theorems that have been introduced. 🤷
https://github.com/leanprover-community/mathematics_in_lean/commit/61e9eca92c9c4400e6586b32d274e99db706570a
TIL: Daniel Velleman wrote a Lean companion to his excellent book, How To Prove It
https://djvelleman.github.io/HTPIwL/
https://djvelleman.github.io/HTPIwL/
Did the solutions for the first batch of exercises: https://github.com/leanprover-community/mathematics_in_lean/commit/38575fb0c276f3ee8078f87f18dc3d694e715834
Most of them were pretty straightforward except for the last one (pictured) where I started in a different direction than what the authors assumed and needed the `sub_add_comm` theorem that hasn't been introduced yet. I couldn't find it by checking the docs/searching, so in the end I had to guess the name of the theorem which was a bit frustrating. Jumping to definition in a proof is magical though.
(Repeating the left side in the calc section is something that I came up with for better alignment)
Most of them were pretty straightforward except for the last one (pictured) where I started in a different direction than what the authors assumed and needed the `sub_add_comm` theorem that hasn't been introduced yet. I couldn't find it by checking the docs/searching, so in the end I had to guess the name of the theorem which was a bit frustrating. Jumping to definition in a proof is magical though.
(Repeating the left side in the calc section is something that I came up with for better alignment)
This is pretty neat. Lean has some sort of macro system to turn theorems for groups with multiplicative notation into theorems with additive notation automatically. The math library feels very ergonomic
Wrote my first proof and it was fun!
`rw [mul_comm c b]` rewrites the left side to `b * c * a`
To be continued...
`rw [mul_comm c b]` rewrites the left side to `b * c * a`
To be continued...
It's pretty cool that you can step through proofs line by line in source files. It's kinda like working with a Lisp REPL
I've been studying number theory and abstract algebra as a hobby, but I got frustrated with not being able to verify my proofs, so I started learning the Lean proof assistant. There are many ways to learn Lean:
https://leanprover-community.github.io/learn.html
Skimming the resources, the Mathematics in Lean in book clicked the best for me so I went with that: https://leanprover-community.github.io/mathematics_in_lean/index.html
Specifically, I got convinced by the Infinitely Many Primes section which is about halfway through the book. It's a simple theorem, but the rigorous proof is not trivial: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html#infinitely-many-primes
https://leanprover-community.github.io/learn.html
Skimming the resources, the Mathematics in Lean in book clicked the best for me so I went with that: https://leanprover-community.github.io/mathematics_in_lean/index.html
Specifically, I got convinced by the Infinitely Many Primes section which is about halfway through the book. It's a simple theorem, but the rigorous proof is not trivial: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html#infinitely-many-primes