A working group for learning Lean and using it in numerical linear algebra research.
Regular meeting: Every other Tuesday 9:30-11am (Eastern Time).
Location: Zoom. To join the mailing list and receive the Zoom link, email me.
October 27, 2026 — Meeting 1
Haim Avron presented an overview of Lean, his personal experiences/workflow using Lean in conjunction with AI for research, and a proposal for formalization standards in the NLA community. [slides]
November 10, 2026 — Meeting 2
Kunal Marwaha will give a talk on Lean and Prove2Me.