Missed this when it came out, but apparently Lean was used to formally verify an uncertain section of a proof in some cutting edge work in the first half of 2021:
And it all happened much faster than anyone had imagined. Scholze laid out his challenge to proof-assistant experts in December 2020, and it was taken up by a group of volunteers led by Johan Commelin, a mathematician at the University of Freiburg in Germany. On 5 June — less than six months later — Scholze posted on Buzzard’s blog that the main part of the experiment had succeeded. “I find it absolutely insane that interactive proof assistants are now at the level that, within a very reasonable time span, they can formally verify difficult original research,” Scholze wrote.
Missed this when it came out, but apparently Lean was used to formally verify an uncertain section of a proof in some cutting edge work in the first half of 2021:
https://www.nature.com/articles/d41586-021-01627-2