Workgroup on formalizing mathematics in Mathlib 4

Aabhas Gulati and Ion Nechita are organising a work group to learn the proof assistant Lean 4. We meet every Friday at 2 p.m.

For more details, please look at the website LeaninToulouse where we will post details of the meetings, and proofs covered in the workgroup.