In this first meeting, we will briefly discuss what formal verification is, how it works, why mathematicians find formal verification increasingly interesting, why Lean4 has become popular with mathematicians, and some resources for learning more. We will also use this meeting to make sure people are setup to use Lean on their own computer and brainstorm ideas for future meetings and for formalization projects we can work on to practice.

Slides: https://ghseeli.github.io/lean/UMich_Lean_Study_Group_Welcome.pdf Outcomes from this meeting:

1. Getting everyone setup with VSCode and Lean.
2. Starting the (https://adam.math.hhu.de/#/g/leanprover-community/nng4)[Natural Numbers Game].
3. Starting to formalize and prove that the sum of 1, 2, …, n is n(n+1)/2 without appealing directly to (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Intervals.html#Finset.sum_range_id)[Finset.sum_range_id].

---

Date published: Monday, February 2, 2026