Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: coq proof of fermat's last theorem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: coq proof of fermat's last theorem


chronological Thread 
  • From: Chris Casinghino <chris.casinghino AT gmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Re: coq proof of fermat's last theorem
  • Date: Thu, 2 Apr 2009 08:36:13 -0400
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; b=FRh1F29nZ1BKSVEtE8aoT3ishRHeMv0+/6DArRzu9HjD3zIMO9uBWLDNA/NtDgflW8 wm1Ot/zeBDQlJHAPnBHNF1H//9v5yHGg1g99et7xBn2ZGQTdGQ3/LD41QGKuG6qRnYOi 88Am+HzDORzHC9UorOqTNy+w+RWw3UCenG6r8=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
I know it is partially documented [1], but are the coq developers
aware that this "feature" can be exploited in this way?  All joking
aside, it seems deceptive that this file compiles.

--Chris

[1] 
http://coq.inria.fr/V8.2/doc/html/refman/Reference-Manual003.html#@default3



On Wed, Apr 1, 2009 at 11:33 AM, Chris Casinghino
<chris.casinghino AT gmail.com>
 wrote:
> Hi Coq Club,
>
> Brian Aydemir and I are pleased to announce a completed coq proof
> of Fermat's last theorem.  Attached, you'll find the .v file.
>
> It's known to compile with both coq 8.1 and 8.2 using coqc on the
> command line.  Note that you won't be able to step through it in proof
> general or coqide, though, because it depends on a feature they don't
> implement.
>
> --Chris Casinghino
>



Archive powered by MhonArc 2.6.16.

Top of Page