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 verifier

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/ 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-confirms-peter-scholze-proof-20210728/ 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.