This page provides links and information about some small formalization projects using Lean 4. All programs are provided as open source under the GNU GPL license (version 3). No guarantee of any kind is given.