Slashdot Mirror

← Back to Stories (view on slashdot.org)

Software Is Starting To Aid Mathematical Proofs

Posted by kdawson on from the sequencing-the-mathematical-genome dept.

An anonymous reader writes "Mathematical proofs are supposed to establish absolute certainty, since each statement is a pure deduction from fundamental axioms. But the reality is that mathematicians make mistakes. Proof-validation software can do what mathematicians never do: spell out every last step, making sure everything is right. Such software has been around for 20 years, but mathematicians and computer scientists now say they are nearing the point where every mathematician will routinely use the software before submitting a new result to a journal, producing a fully correct, formal, axiomatized mathematics."

2 of 90 comments (clear)

  1. Re:Awesome by Tablizer · · Score: 4, Funny

    I would love to see in fully correct, formal, axiomatized mathematics, why my wife is such a bitch!

    Simple:

    A. You are a nerd
    B. Your wife wants a life
    C. If a woman gets no life, she becomes a bitch
    D. Nerds have no life

    A + B + C + D -> Your wife is a bitch

    Next!

    --
    Table-ized A.I.
  2. one proof engine by emeraldemon · · Score: 4, Informative

    For what it's worth, I've had good experiences with coq: http://coq.inria.fr/ Although I've never used it for anything large, it has the nice ability to make proofs about code, and export the code to haskell, scheme, or ML. I had a fun time proving that the min function always returns the lesser of the two values.