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].

In this session, we spent time going through the lean_lec_feb9.lean file in the lean_lectures folder of the Github repository. In particular, we reviewed tactics found in the Natural Numbers Game, stepped through a proof that the sum of the first n odd natural numbers is equal to n^2, and live coded a proof of FiniteField.prod_univ_units_id_eq_neg_one, including demonstrating the refine tactic.