I've spent another couple of hours playing with Lean, following @XenaProject's Formalising Mathematics course (https://github.com/ImperialCollegeLondon/formalising-mathematics)
I think the hardest part for me is remembering what each notation really represents, like ¬ P is really (P → false)
@christianp A nice introduction to Lean is Kevin's natural numbers game: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/
Although you may have advanced past that already.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!