News for hackers. Stuff that matters.
Re:How close are computers to automating mathematical reason... by wisnesky on Saturday August 29, 2020 @02:05PM (#24318115)
You are right that computer generated proofs are often tough to understand, and that understanding is often the intended goal of writing a proof. But proofs can be useful for reasons besides human understanding, especially so in engineering. For example, when a browser establishes a secure session with an encryption protocol, the reason it is secure has to do with the difficulty of finding a proof that eg certain numbers factor, but no human cares about this proof. As another example, a compiler can use a proof that a program is type correct to optimize it, but humans would not find such proofs interesting at all.
Re:How close are computers to automating mathematical reason... by sukilot on Saturday August 29, 2020 @02:25PM (#24318280)
That's great, but not relevant to mathematicians doing their jobs.
Re:How close are computers to automating mathematical reason... by whatshisface on Saturday August 29, 2020 @04:31PM (#24319219)
Knowing which conjectures were true would probably help mathematicians work more efficiently. At the very least nobody would spend time searching for counterexamples to true conjectures.