recurse day 5
I ran in late because my bus line mysteriously ended about 20 minutes before Google Maps said it would.
Theorem provers 101!
Pius ran a morning study group for theorem provers and helped us learn the basics of Lean while we went through this interactive tutorial. We proved associativity ((a + b) + c = a + (b + c)) and commutativity (a + b = b + a) of addition for natural numbers!!
Doing math in a theorem prover was extremely different from writing it out by hand, and extremely confusing at first because I had no idea what inputs the transformations seemed to be taking. Once we proved associativity, my mind exploded and the mapping from math to theorem prover started to make a little sense.
Even though I used to be a math nerd, I have never done this before because I thought it was silly to prove properties that seemed to me to be intrinsically defined on the operator and group (and no, I never took real analysis either), but in the context of computational theorem proving I finally understand why that level of rigor is interesting and useful! Wowe.
Decompressing
Great conversation with V and others about the dreaded “where are you from from” question that visible racial minorities are often subjected to.