None of these proofs listed in the Wikipedia page are formalized in Lean at the moment, although a few are formalized in other theorem provers (Four Color Theor

None of these proofs listed in the Wikipedia page are formalized in Lean at the moment, although a few are formalized in other theorem provers (Four Color Theorem in Coq, Kepler Conjecture in Isabelle). The "Formalization papers using Lean" section of https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/papers.html lists some theorems whose proofs have been verified in Lean, but (despite being written in Isabelle) I think the Kepler Conjecture formalization is the best example of what you have in mind. The main difference between most of the examples you list via the Wikipedia page and the examples listed in the URL I cited above is how the computer is being used: in many cases, "computer-assisted" means an ad-hoc program was used to check a bunch of cases which would be too tedious for a human to check. But what happens if there is a bug in the used ad-hoc program (or, e.g., in a linear programming solver)? To increase confidence in the verification result, ideally both the validity of the case-checking and the logic for deducing the main theorem from the checked cases would be verified by a small and general "kernel"/proof checker. This is what theorem provers such as Lean, Coq and Isabelle allow.