Defining structures

We briefly discussed people’s progress on their projects. We then spent the remainder of the time “live coding” an approach to proving a general version of the Brouwer fixed point theorem. This involved a lot of trial-and-error as we practiced considering the details of how to actually formalize something.

More details, including the end result of the session, are in the lean_lec_mar16.lean file.

---

Date published: Monday, March 16, 2026