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.
[ Parent
| on HN ]
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.