3 ms·

Would it be possible to simplify the system by making default assumptions about a consensus/common-sense logic? Are topologists interested in different logical

• alimw 8y ago
  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.
  • Retra 8y ago
    ... assuming you correctly wrote your theorem in those frameworks.
    • alimw 8y ago
      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