5 ms·

While computer proofs are better than no proofs at all, they aren't as exciting as "classic" proofs, which typically build new theory and inspire new questions

• Ericson2314 6y ago
  The 4 color theorem was a boring case analysis, but that doesn't mean that all computer proofs are boring and tedious. We have proof assistants using many beautiful type theoretic languages, and tools which can (attempt) to write proofs in this languages. In fact, this is one of the best usages of ML because we hardly care whatever impenetrable bullshit goes into the proof search when the proof must be self-justifying, and, just like a ML go game log, potentially lead to new techniques for human mathematicians.