Machine-Checkable Proofs

Scott Aaronson asks why mathematicians haven’t switched to machine-checkable proofs, and answers his own question by exhibiting the basically-human-unreadable proof of the irrationality of the square root of two using the HOL Light theorem prover. Scott provides a few interesting links:

There is also the Flyspeck Project, a project to formalize Thomas Hales’ computer proof of the Kepler conjecture, which we mentioned once before.

levitra buy levitra buy levitra online generic levitra order levitra levitra online levitra viagra levitra prescription buy generic levitra cheap levitra levitra on line order levitra online purchase levitra purchase levitra online levitra side effects viagra levitra levitra sale levitra pill levitra vs viagra levitra com discount levitra levitra sample levitra woman free levitra levitra medication levitra viagra vs dysfunction erectile levitra levitra tablet buy levitra viagra levitra medicine levitra actress bayer levitra levitra dosage levitra versus viagra buy cheap levitra levitra story levitra price levitra pen free levitra trial birth control levitra pill comparison levitra viagra levitra vardenafil levitra commercial levitra commercial actress levitra 10mg levitra review levitra free sample viagra vs levitra levitra canada levitra information compare levitra viagra drug levitra levitra lowest price compare levitra levitra testimonials cost levitra levitra online pharmacy levitra result levitra info levitra prescription america low cost levitra levitra cheapest brochure levitra levitra news drug impotence levitra buy levitra line levitra bayer levitra cheap levitra ad buy levitra viagra online buy levitra on line buy levitra cheap online online levitra cheap levitra online levitra prescription online levitra generic non prescription levitra levitra line best levitra price levitra low price low price levitra lowest price for levitra levitra discount vardenafil levitra hcl levitra vardenafil com levitra levitra sale uk compared levitra viagra cheapest levitra levitra drug levitra cost dosage levitra canada levitra canada in levitra 20mg levitra ad levitra free levitra sample info levitra commercial levitra 10mg levitra dosing levitra efficacy levitra levitra for woman woman levitra clinical data levitra kit levitra slide levitra alternative levitra

5 thoughts on “Machine-Checkable Proofs

  1. HOL (the logic) and HOL Light (the proof assistant) were designed and optimized for software verification, not for presenting machine-checkable mathematical proofs. In software verification the interest is in the fact that a theorem has been proven to be true, while mathematicians would also like to read the proof to find out *why* it is true.
    Other proof assistants are able to provide much more readable presentations of machine-checkable proofs.

  2. While wishing to know the “why” is certainly a desire, that knowledge to me seems to come from the breadth of a result to other things, thus the deeper “why” is almost certainly going to come later anyway. I feel I could accomplished quite a lot with an oracle providing handholds in the rock face, so to speak. i.e. it still seems worth it since you could still get somewhere.

  3. We haven’t even solved the problem of representing mathematics on a computer, let alone proving it. Despite the power of computers to render images of stunning beauty we still don’t have an efficient means of expressing ourselves on a computer. Mathematical notation was designed and refined over centuries going back to numerals imported from India via the Arab world. But with the advent of computers, Instead of things like the lovely curvy symbol introduced by Fourier, I now have to type crap like \int_{x_i}^{x_{i+1}} dx. When I look at most proof-checking systems they make me want to run a mile. When formally checked proofs actually look like recognisable mathematics, and can be entered in a friendly way, then some of the resistance to them might go away.

  4. >I now have to type crap like \int_{x_i}^{x_{i+1}} dx

    Only if you choose to use a plain text editor to write your tex files. With better authoring tools (like LYX) you can choose the lovely curvy symbol from a menu and see it immediately on the screen.

    >When formally checked proofs actually look like recognisable mathematics

    Proofs witten in Isabelle’s Isar do look like recognizable mathematics. Those based on ZF logic can be read like standard mathematical proofs, no need for learning special syntax. The only valid complain is that they are more detailed that some readers are used to.

    >can be entered in a friendly way,

    Yes, that’s a totally different story. The tools for writing formalized mathematics are bad.

  5. From Friedmans paper ( about proof-assistants ):

    1. The user orchestrates the refining of goals and
    hypotheses according to a natural deduction framework. This
    is in accordance with the general logical organization of
    actual mathematical proofs.

    2. The user cites definitions and theorems from
    ‘libraries’. The proper construction of libraries is
    absolutely crucial in practice. Supports strong
    reusability.

    3. It is also crucial that the proof assistant be able to
    make relatively trivial inferences on its own. Experience
    shows that otherwise the process is just too time
    consuming.

    Is there actually a mathematician that works ( or has worked ) in the manner proposed by this scheme of rationality? It appears to me this scheme could be valuable if proofs have customers just like industrial software and there were a bulk of employed test enigneers used to perform this kind of work and enhance libraries. I wonder how the agile variant of this practise would look like?

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>