José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Learning Lean (part 3). ~ Rado Kirov. rkirov.github.io/posts/lean3

Learning Lean: Part 3

I am continuing to learn Lean (see part 1 and part 2). I lost some steam around March-April, but in the last two months I picked it up again. In a way it was a nice spaced repetition for relearning some of the basics. This summary was supposed to be my notes from finishing the rest of Mathematics in Lean and finishing chapters 2 and 3 of exercises from Terence Tao’s Analysis textbook, but also I couldn’t help also comment on the challenges and opportunties I see in doing formal mathematics with Lean.

rkirov.github.io · Rado's Radical Reflections

0
0
0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/Jose_A_Alonso/statuses/116068539356339198 on your instance and quote it. (Note that quoting is not supported in Mastodon.)