1067
Agost Biro
@agostbiro #1067
OSS + Rust. I have one goal in life: the ability to stop thinking at will
2018 Follower 616 Following
Petition for the next commission to get eu/acc on their agenda: https://www.eu-inc.org/
Is anybody headed to Eurorust in Vienna? Hit me up if you do! I’ll be at the async workshop tomorrow
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
Apple open sourced a break through model for monocular (single image) depth estimation. This is a huge unlock for many things from robotics to computer graphics.
https://venturebeat.com/ai/apple-releases-depth-pro-an-ai-model-that-rewrites-the-rules-of-3d-vision/
https://venturebeat.com/ai/apple-releases-depth-pro-an-ai-model-that-rewrites-the-rules-of-3d-vision/
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/
To be clear, this is not a light show, it's a military display
https://x.com/MarioNawfal/status/1840466077785923952
https://x.com/MarioNawfal/status/1840466077785923952
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
Awesome to see that developer momentum has been maintained since FarCon irrespective of markets
Nothing like the present 🙏
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 did some UI coding tonight which I’m not very good at so I tried out Cursor for it, and for the most part it wasn’t really better than a Copilot-style extension, but once I just highlighted some components that were misaligned and told it to make it nicer and it nailed it. That was magical
This is why I'll never use a closed source browser or terminal app from a startup
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/
It’s a lot easier to correct bad policy within the framework of a liberal democracy than to reverse democratic backsliding.
If Trump wins, the US starts down an unprecedented authoritarian path. As a I learned it the hard way in my native Hungary, one must vote for the winningest opposing candidate in a situation like this, no matter how misguided their policy, just to preserve the rules of the game.
If Trump wins, the US starts down an unprecedented authoritarian path. As a I learned it the hard way in my native Hungary, one must vote for the winningest opposing candidate in a situation like this, no matter how misguided their policy, just to preserve the rules of the game.
Q: How do you evaluate a technology that is a lot more advanced than what you can understand?
A: Study the person behind the tech. If they're consistently right on related topics that you can understand, then the more advanced idea is probably right as well.
A: Study the person behind the tech. If they're consistently right on related topics that you can understand, then the more advanced idea is probably right as well.
The Finite Simple Group (of Order Two) by The Klein Four a capella group
https://www.youtube.com/watch?v=BipvGD-LCjU
https://www.youtube.com/watch?v=BipvGD-LCjU
The Science of Can and Can't is the most interesting book I've read this year. It's a pop-sci exposition of the quest to expand the domain of physics to the domain of counterfactuals (things that could be). The author developed constructor theory together with David Deutsch which is a formalization of these ideas.
If you're gonna buy this, it's also worth grabbing The Book of Why by Judea Pearl which is the AI counterpart to this book.
If you're gonna buy this, it's also worth grabbing The Book of Why by Judea Pearl which is the AI counterpart to this book.
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...