In the speaker’s account, statements that seem most trivial and obvious to humans are often the hardest to verify in Lean when formalizing informal proofs.

“They want, they wanna formalize it in Lean. And what they discover is often it's the most trivial statements that are most obviously true to humans are the hardest to convince Lean are correct.”