You're right (and the GP isn't). A proof of your topological theorem in any one of Coq/Isabelle/Lean is a pretty good indication that it's correct, in spite of their various foundations.

... assuming you correctly wrote your theorem in those frameworks.

I think you are exaggerating the difficulty of theorem statement compared to proof. Here is one (admittedly extreme) example in Lean, from the formal abstracts website.

theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare