[Tainnor]

For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/124731...