Re: [isabelle] counterexamples to Euler's conjecture with Isabelle



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.