*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle*From*: Dominique Unruh <unruh at ut.ee>*Date*: Wed, 28 Feb 2018 10:51:57 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <2e1f4f2f-0d3a-14bf-8b80-e06498c99cd9@in.tum.de>*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> <2e1f4f2f-0d3a-14bf-8b80-e06498c99cd9@in.tum.de>

On 28 February 2018 at 09:08, Tobias Nipkow <nipkow at in.tum.de> wrote: > Just for fun I tried to find the counterexample by an explicit search: > > [...] > > If you try the target values 1^5, 2^5, ... it takes 4 hours until 144^5 is > found. > > I wonder how long it took them on their CDC 6600. Probably not terribly long, as this tweet reply would indicate: https://twitter.com/BruceHoult/status/585427224846675969 Best wishes, Dominique. 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 6600 > https://io9.gizmodo.com/how-two-sentences-overturned-200-yea > rs-of-mathematical-1697483698 > > I 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 > know that there exists a counterexample with 4 summands) after I use > nitpick /quickcheck for > > 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)) " > > 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 > such counterexamples? > > > 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 a counterexample > with 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 many > counterexamples > for 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 > >

**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

**Re: [isabelle] counterexamples to Euler's conjecture with Isabelle***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Previous by Thread: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Next by Thread: Re: [isabelle] Vector transpose
- 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