3 ms·
... assuming you correctly wrote your theorem in those frameworks.
by Retra 8y ago
... assuming you correctly wrote your theorem in those frameworks.
- alimw 8y agoI 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