Based on what I understand, here is a brief summary. Clausen and Scholze are developing "Condensed mathematics", with "condensed sets" replacing topological spaces (replacing in algebraic applications but equvialent to usual topology in geometric situations).
A foundational theorem of theirs had a delicate proof and Scholze was worried it could be wrong. Since it wan meant to be used as a blackbox, an error would mean a lot of mathematics built on it will be in doubt.
Six months ago, Scholze issued a challenge to the formalization community to formalize and computer verify a set of results, including the foundational one. Scholze announces that the result he was waorried about is now formally verified in the lean
theorem prover, with some tweaks to the proof outline along the way (and the original challenge is halfway done). This suggests that "formalization" is approaching the stage where this is (even in practice) the best way to be sure mathematics is correct.