3 ms·
As your cousin post notes, Devlin isn't ignoring "machine checked" proofs. The question of whether machines can write proofs that can be "human checked" is the
by dvanduzer 12y ago
As your cousin post notes, Devlin isn't ignoring "machine checked" proofs.
The question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician. Otherwise, they'd be software engineers (which Devlin hints at in this essay).
- bumbledraven 12y agoThe question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician. Maybe Devlin should first stop denying that humans can write proofs that can be both human- and machine- checked. Then we can talk about whether machines can write those proofs.
- dvanduzer 12y agoHumans can definitely write proofs that can be checked by humans or machines. It's arguing in bad faith to suggest that mathematicians are un-qualified to determine the validity of a machine-checked proof. There are certainly some stodgy holdouts that will never be convinced, but I don't think Devlin is one of them.
- _asummers 12y agoI wasn't suggesting that Devlin was ignoring them, I was responding to my comment's parent that mathematicians he knows are ignorant of them, which I tried to make clear by saying "those mathematicians".