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



Dear Angeliki,

The original conjecture looks difficult to refute with our tools, unless you are very lucky. The second one, where just A is left, is easy:

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

That way quickcheck will try 1000 random values up to 100. Of course you need to have some idea in what range to search and in general you have to be lucky ("random").

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 6600
https://io9.gizmodo.com/how-two-sentences-overturned-200-years-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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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