Formalizing mathematics in the eXperimental Lean Lab

The eXperimental Lean Lab will showcase using Lean to formalize real mathematics. We have five groups formalizing 1) generating functions, 2) central limit theorem, 3) topology for algebraic geometry, 4) examples in commutative algebra, and 5) metaprogramming in Lean.

If you have been curious about using computers for proof assistance and verification, this talk is for you!