4 ms·

While that proof is amusing I was hoping for... an actual proof that I can give to a verifier. Ah well. A hundred or so lines of comments is probably right. St

While that proof is amusing I was hoping for... an actual proof that I can give to a verifier. Ah well. A hundred or so lines of comments is probably right. Still this looks to be some impressive work and I did enjoy this post.

pizlonator 10y ago
I'm a mathematician. Proofs are one of the means of communication between me and other mathematicians. I don't give a crap if a computer can read my proof.
- corndoge 10y ago
  Well, us programmers do since computers are the ones we're communicating with.
  - pizlonator 10y ago
    I like to write programs when I program and proofs when I mathematize. The program is for the computer and the proof is for a human. I think you're getting it all mixed up!
    - corndoge 10y ago
      I think you're wrong!
- nickpsecurity 10y ago
  Quite a few people held that view in this article: https://www.quantamagazine.org/20130222-in-computers-we-trust/ https://www.quantamagazine.org/20130222-in-computers-we-trus... It and others I've read on machine-checked proof showed the computer-centric one could catch quite a few problems with higher assurance of correctness. The peer review problem in science also makes me think it's important given I can't be sure the huge proofs will be adequately checked. Far as reliability on computer end, I've read on verified processors, proof assistants, compilers, and so on. Much of the risk can be knocked out but the black box that is human brains is another story.
nickpsecurity 10y ago
Maybe he means proof like lawyers use it instead of mathematicians. Im sure his proofs are quicker that way. ;)
- AnimalMuppet 10y ago
  Lawyers are faster than mathematicians? In fact, that's probably right, but I'm experiencing cognitive dissonance right now...
  - moomin 10y ago
    Depends how much you overclock your mathematician.
  - nickpsecurity 10y ago
    They sure prove, err argue, faster.
    - ooqr 10y ago
      The justice system has more overhead.
      - nickpsecurity 10y ago
        Just means it's ripe for disruption by a YC startup.

pizlonator 10y ago

I'm a mathematician. Proofs are one of the means of communication between me and other mathematicians. I don't give a crap if a computer can read my proof.

corndoge 10y ago
Well, us programmers do since computers are the ones we're communicating with.
- pizlonator 10y ago
  I like to write programs when I program and proofs when I mathematize. The program is for the computer and the proof is for a human. I think you're getting it all mixed up!
  - corndoge 10y ago
    I think you're wrong!
nickpsecurity 10y ago
Quite a few people held that view in this article: https://www.quantamagazine.org/20130222-in-computers-we-trust/ https://www.quantamagazine.org/20130222-in-computers-we-trus... It and others I've read on machine-checked proof showed the computer-centric one could catch quite a few problems with higher assurance of correctness. The peer review problem in science also makes me think it's important given I can't be sure the huge proofs will be adequately checked. Far as reliability on computer end, I've read on verified processors, proof assistants, compilers, and so on. Much of the risk can be knocked out but the black box that is human brains is another story.

nickpsecurity 10y ago

Maybe he means proof like lawyers use it instead of mathematicians. Im sure his proofs are quicker that way. ;)

AnimalMuppet 10y ago
Lawyers are faster than mathematicians? In fact, that's probably right, but I'm experiencing cognitive dissonance right now...
- moomin 10y ago
  Depends how much you overclock your mathematician.
- nickpsecurity 10y ago
  They sure prove, err argue, faster.
  - ooqr 10y ago
    The justice system has more overhead.
    - nickpsecurity 10y ago
      Just means it's ripe for disruption by a YC startup.