If G is a finite group and H ⊆ G is a subgroup, then the order of H divides the order of G.
Abstract term rewriting (Gregory Baimetov):
The confluence and the Church-Rosser property are equivalent (see Wikepidia).
Formalize the principle of well-founded induction (see Wikepidia).
Simplicial homology / tactics (Zachary Banken):
Formalize simplicial homology including definitions of simplicial complexes, faces, and the chain group as well that the square of the boundary operator is zero.
Functional programming and writing simple tactics in Lean.
Linear algebra (Dianna E.):
If V is a vector space and S, T: V → V are linear transformations such that the range of S is contained in the nullspace of T, then (ST)² = 0.
Compactness (Luca Li):
If X is a compact space, then every closed subset is also compact.
If (X,d) is a metric space and every infinite subset of X has a cluster point, then X is sequentially compact.
Banach Fixed Point Theorem (Lawrence Lin):
If (X,d) is a non-empty complete metric space and T: X → X is a contraction mapping, then T has a unique fixed point.
Euclidean Geometry (Rico Qi and Edward Yu):
Formalize Euclidean Geometry based on Hilbert's Axioms by defining points, lines, angles, and the notion of distance.
