Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

Atrium > Mathematics, Physics & Philosophy: proof verification

Bottom of Page

1 to 16 of 16

  1.  
    • CommentRowNumber1.
    • CommentAuthorjim_stasheff
    • CommentTimeOct 18th 2012
    From a colleague
    Subject: [Math-visitors] remarkable achievement in proof verification
    Date: Wed, 17 Oct 2012 13:22:57 -0400
    From: Jean Gallier <jean@cis.upenn.edu>
    To: faculty@math.upenn.edu, grad@math.upenn.edu, visitors@math.upenn.edu


    Dear all,

    I learned from the "Types Forum" that a group of researchers at MSR/INRIA
    led by Georges Gonthier completed a formal verification (in Coq) of the
    "Odd order theorem," due to Feit and Thompson
    (every finite group of odd order is solvable).

    The task of proof verification in Coq took 6 years. The Coq development contains
    ~ 170 000 lines of code
    ~ 4200 definitions
    ~ 15 000 theorems.

    They did find small gaps, but all could be patched.


    For more details, see
    http://www.msr-inria.inria.fr/Projects/math-components/feit-thompson
    In particular, at the end of the page, look at the "final theory graph."

    The question remains: how do we know (and prove) that Coq is correct?
    We have to verify the verifier!

    Best,
    -- Jean
    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeOct 18th 2012

    I heard about this from the type theorists here at Princeton. An awesome achievement!!

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeOct 19th 2012

    I believe that Coq has been proved correct using a bare-bones stripped-down version of Coq, which in turn is quite small and amenable to verification by a human (unlike the proof of Feit and Thompson). But I don't know the details; probably the Types Forum knows this better. And I do know that Coq was inconsistent once, briefly, by mistake; so Jean is right to want to check!

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeOct 19th 2012

    Although, it seems very unlikely to me that Coq would ever accidentally be inconsistent in just such a way that someone trying to formalize a real mathematical proof would accidentally take advantage of to get around a flaw in the proof.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeOct 20th 2012

    Yes, for essentially the same reason that mathematics did not collapse when Russell found his paradox.

    Although it is really soundness that we want, not just consistency. Being inconsistent is only the most extreme way to be unsound.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 20th 2012

    What is especially exciting to me is the prospect of going on and verifying the classification of finite simple groups. The experts who contributed to this monumental effort are aging or passing on, and there is a danger that there aren’t enough younger people with the requisite training (in what is an extremely specialized field) to critically survey the proof. Meanwhile others use the classification theorem in their research.

    I hope I live to see such a computerized verification.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 20th 2012

    Three years ago I mentioned Sasha Borovik’s prediction that in twenty years Inna Capdeboscq will be the last non-retired mathematician in the world able to repair the proof. Of course, along with a verified proof, it would be wonderful if people could develop the field so as to make the proof simpler, i.e., the Darwin mentioned in the quote here might come along.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeOct 20th 2012

    @Toby, what does it mean to say that a formal system is “sound”? I’m used to thinking of soundness as a property of semantics, i.e. of the relationship between a formal system (syntax) and some model of it.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeOct 21st 2012

    In an absolute sense, soundness means that every theorem is true. Of course, this relies on an interpretation (to assign meaning to the sentences in the formal system), and (as you and I know even though some people prefer to pretend otherwise) there is no absolute notion of mathematical truth for the interpretation to take values in either. So really, soundness is (as you say) simply a relationship between a syntax and a model.

    But in this case, we want an informal notion of soundness anyway. The point is, if we’re using Coq to verify a proof a theorem that we want to sure is (in some informal sense) actually true, then we want to be sure that Coq verifies only proofs of true statements. Since Coq is complicated, this is hard, but if we can bootstrap this by proving, in a stripped-down simplified version, that Coq is conservative over this stripped-down version (which I’m not sure is what really has been done), then we only have to look at the simple version. Then it’s an informal question: do you trust this simple version, which you can fully comprehend? If so, we’re good!

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 21st 2012

    But how is that informal notion of “trust”/”soundness” different from consistency?

    • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 21st 2012
    • (edited Oct 21st 2012)

    Some relevant discussion on an old MO question of mine.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 21st 2012

    Try that again: Some relevant discussion. (You have to make sure the http is in there!)

    • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 21st 2012

    Ta! Using my phone and didn’t check the URL worked.

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeOct 23rd 2012

    how is that informal notion of “trust”/“soundness” different from consistency?

    In principle, it has nothing to do with consistency; although in practice, if one wants to do only consistent mathematics, then soundness requires consistency. But it's easy to be consistent and unsound!

    Here is a system of axioms for arithmetic (in classical untyped first-order logic with equality, a nullary operator 00 for zero, a unary operator SS for the successor, and binary operators ++ for addition and ⋅\cdot for multiplication):

    • ∀x,Sx≠0\forall\, x,\; S x \ne 0,
    • ∀x,∀y,Sx=Sy⇒x=y\forall\, x,\; \forall\, y,\; S x = S y \;\Rightarrow x = y,
    • ∀x,x+0=x\forall\, x,\; x + 0 = x,
    • ∀x,∀y,x+Sy=S(x+y)\forall\, x,\; \forall\, y,\; x + S y = S (x + y),
    • ∀x,x⋅0=x\forall\, x,\; x \cdot 0 = x,
    • ∀x,∀y,x⋅Sy=(x⋅y)+x\forall\, x,\; \forall\, y,\; x \cdot S y = (x \cdot y) + x.

    This system is consistent, but it is not (under the specified interpretation) sound.

    Formally, one could give an interpretation of this system in (say) Peano Arithmetic and prove that the interpretation is unsound; informally, I indicated in parentheses when I introduced the language what the interpretation (in ‘reality’) was supposed to be, and this interpretation is unsound.

    (If anybody cannot spot the error, it's in the next axiom to last.)

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeOct 24th 2012

    But you’re still invoking some “intended model”, so as before “soundness” is not a property of the system but of some particular semantics for it.

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeOct 24th 2012

    Yes, it still relies on the interpretation.

1 to 16 of 16

  1.