Lean Together

If you have been curious about Lean -- the programming language to teach math to a computer -- but did not know how to get started, come Lean with us! The Math AI Lab (ai.math.uw.edu) is organizing this event to bring Lean beginners together, including level 0, to quote Panda Po. This is also a good way to engage with the UW Math AI Lab in order to participate in future research projects.

 

I will give a small demo that you will follow on your laptop right in the browser. We will probably start with the Natural Number Game and proceed to Glimpse of Lean.