*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 27 Feb 2018 17:19:55 +0100*In-reply-to*: <a1a747187c34ad9df3038496533835d5@cam.ac.uk>*References*: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com> <FDFF8848-06A0-4300-AF7B-ADBB9F30A489@exchange.uibk.ac.at> <CAAi=gevK1B1sGOyoRD4b1jSdCgkytQLV_=z2ckFHhpK+81Hg2g@mail.gmail.com> <68f6ad9b-4697-c321-b24c-61b79471c1a2@sketis.net> <CAAi=gevi-9xYm1x6ct5DNdZAzHtCV-TVn+0e4XbAO6OwjLABNQ@mail.gmail.com> <a1a747187c34ad9df3038496533835d5@cam.ac.uk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

Dear Angeliki,

quickcheck[random,size=100,iterations=1000]

Tobias On 27/02/2018 16:49, Dr A. Koutsoukou-Argyraki wrote:

Dear Isabelle users, motivated by the following mini-paper from the 1960's where a counterexample to Euler's conjecture was found by a direct search using the supercomputer CDC 6600https://io9.gizmodo.com/how-two-sentences-overturned-200-years-of-mathematical-1697483698I tested if Isabelle can do something similar using nitpick/quickcheck.It turns out that for the specific case for n=5 (for which we already do knowthat there exists a counterexample with 4 summands) after I use nitpick/quickcheck forlemma euler5 : shows"∄ (A ::int) (B ::int) (C ::int) (D ::int) (E ::int). ( (A>0) ∧ (B>0) ∧ (C>0) ∧( D>0) ∧ (E>0) ∧ ( A^5 + B^5+ C^5 +D^5 = E^5)) "I immediately get the answer: "nitpick/quickcheck found no counterexamples". (Note that without setting : (A>0) ∧ (B>0) ∧ (C>0) ∧ ( D>0) ∧ (E>0) nitpick gives me the counterexample (-1, -1, 1, 1, 0) while quickcheck gives the counteraxample (0,0,0,0,0) but of course Euler's conjecture is for positive integers only.) Actually, even for the following, nitpick and quickcheck give up without finding the counterexample (which should be A=27) lemma euler5 : shows "∄ (A ::int). ( (A >26) ∧(A<28) ∧( A^5 + 84^5+ 110^5 +133^5 = 144^5)) ". I also tried nitpick quickcheck and sledgehammer after doing the following, without getting the desired counterexample A=27 (value correctly gives "true"): value"( (27::int)^5 + 84^5+ 110^5 +133^5 = 144^5) " lemma euler5 : shows "∄ (A ::int). ( (A >26) ∧(A<28) ∧( A^5 + 84^5+ 110^5 +133^5 = 144^5)) "Any ideas? Could it be somehow possible to make Isabelle's automation find suchcounterexamples?Thank you, Best, Angeliki Koutsoukou-Argyraki So for but perhaps this should not be surprising as it looks like the reason is the fact that Isabelle is not really built for numerical computations- note that sledgehammer times out without finding a proof of : shows "( 27^5 + 84^5+ 110^5 +133^5 = 144^5) " sledgehammer Best, Angeliki On 2018-02-26 19:29, Dr A. Koutsoukou-Argyraki wrote: well I don't think they do badly because as I wrote below nitpick and quickcheck do find trivial counterexamples when one removes the condition (A>0) ∧ (B>0) ∧ (C>0) ∧ ( D>0) ∧ (E>0). Also it looks like it was a very powerful supercomputer that found the counterexample for n=5 so it must be very tough. Now what I want to check is to what extend I can help nitpick /quickcheck by setting some of A, B, C etc as in the known counterexample and see if the automation can discover the rest to complete the counterexample. And/Or set an interval of integers for the search. I 'll do some experimenting and will update you, I'm very curious Best, Angeliki On 2018-02-26 19:11, Lawrence Paulson wrote: I'm genuinely surprised that they gave up, and so quickly. I think that they would run forever. Quickcheck cannot even find a Pythagorean triple! lemma "∄ (A ::int) (B ::int) (C ::int). ( (A>0) ∧ (B>0) ∧ (C>0) ∧ ( A*A + B*B = C*C)) " nitpick On the other hand, the paper you cited looks pretty specialised to me. I do wonder how quickcheck works, that it can't solve such an easy problem. Larry On 26 Feb 2018, at 18:23, Dr A. Koutsoukou-Argyraki <ak2110 at cam.ac.uk> wrote: Dear Larry, dear Wenda,for the specific case for n=5 (for which we already do know that there exists acounterexamplewith 4 summands) after I do nitpick /quickcheck, I immediately get the answer: "nitpick/quickcheck found no counterexamples". (Note that without setting : (A>0) ∧ (B>0) ∧ (C>0) ∧ ( D>0) ∧ (E>0) nitpick gives me the counterexample (-1, -1, 1, 1, 0) while quickcheck gives the counteraxample (0,0,0,0,0) but of course Euler's conjecture is for positive integers only.) lemma euler5 : shows"∄ (A ::int) (B ::int) (C ::int) (D ::int) (E ::int). ( (A>0) ∧ (B>0) ∧ (C>0) ∧( D>0) ∧ (E>0) ∧ ( A^5 + B^5+ C^5 +D^5 = E^5)) "In this paper from 1988 (see link below) Elkies finds infinitely manycounterexamplesfor the case n=4. http://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/home.html Would it be perhaps a good idea to try implementing his counterexample generator so as to reinforce Isabelle's automation ? Thank you, Best, Angeliki

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] counterexamples to Euler's conjecture with Isabelle***From:*Dr A. Koutsoukou-Argyraki

**Re: [isabelle] counterexamples to Euler's conjecture with Isabelle***From:*Lawrence Paulson

**References**:**[isabelle] Vector transpose***From:*Omar Jasim

**Re: [isabelle] Vector transpose***From:*Thiemann, Rene

**Re: [isabelle] Vector transpose***From:*Omar Jasim

**Re: [isabelle] Vector transpose***From:*Makarius

**Re: [isabelle] Vector transpose***From:*Omar Jasim

**[isabelle] counterexamples to Euler's conjecture with Isabelle***From:*Dr A. Koutsoukou-Argyraki

- Previous by Date: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Next by Date: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Previous by Thread: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Next by Thread: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list