[isotypic]

What exactly do you mean by non-trivial/modern standards? While certainly the largest and most complicated theorems are currently out of reach of proof verifiers, there isn't a shortage of usage of them to prove important/modern theorems (of course certain fields are much more developed/more amenable to verification than others).

* https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/ discusses a few recent usages in recent papers and the author's grant to formalize Fermat's last theorem.

* The liquid tensor experiment (https://www.quantamagazine.org/lean-computer-program-confirm...)

* Feit-Thompson was formalized in 2012.

I do largely agree that formal correctness within mathematics is not as important as it may seem, though this doesn't mean formal verification of a proof is completely orthogonal to understanding it - you can't formally verify something without really understanding the proof in the first place.