Weekly Lean Hacking with MathsSoc

We’ve collaborated with MathsSoc to bring you our first regular event: weekly hacking with the Lean4 theorem prover!

Lean is a dependently-typed proof assistant, with a lot of community support to make it as easy as possible to write mathematical proofs in a machine-verifiable manner. Our two hour sessions are a place to learn about proof assistants, and to get some practical experience with Lean and mathlib4.

Sessions take place every Thursday in AT5.04, from 5pm to 7pm. We’re planning to have academic talks every other week, starting from the 5th of October (next week!). Be sure to keep an eye on our Discord for announcements of these!