Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] counterexamples to Euler's conjecture with Isa...

Email Gateway (Aug 22 2022 at 16:41):

From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s

Email Gateway (Aug 22 2022 at 16:41):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Tobias,

Thanks a lot for your answer. This does work and by increasing the size
value
nitpick is indeed successful in finding the rest of the integers
individually as well.
But I suppose there is no way to perform a search like
this for more than 1 integer simultaneously ?

Thank you again,
Best,
Angeliki

Email Gateway (Aug 22 2022 at 16:41):

From: Tobias Nipkow <nipkow@in.tum.de>
Just for fun I tried to find the counterexample by an explicit search:

function find where
"find p (n::int) (t::int) (i::int) =
(let ip = i^p in
if ip > t then None else
if ip = t then if n = 0 then Some [i] else None
else if n = 0 then find p n t (i+1)
else case find p (n-1) (t-ip) 1 of
Some is ⇒ Some(i#is) |
None ⇒ find p n t (i+1))"
by pat_completeness auto
termination sorry (* couldn't be bothered *)

"find p n t i" searches for (n+1) pth powers that sum up to t (starting with i).

If you know the target value 144^5 the decomposition is found in 2 minutes:

value "find 5 3 ((144::int)^5) 1"

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.

Tobias
smime.p7s

Email Gateway (Aug 22 2022 at 16:41):

From: Tobias Nipkow <nipkow@in.tum.de>
On 27/02/2018 18:38, Dr A. Koutsoukou-Argyraki wrote:

Dear Tobias,

Thanks a lot for your answer. This does work and by increasing the size value
nitpick is indeed successful in finding the rest of the integers individually as
well.
But I suppose there is no way to perform a search like
this for more than 1 integer simultaneously ?

In principle it does not matter. For this example it still worked fine for 2
integers but the search space became too large when leaving 3 integers open.

Tobias

Thank you again,
Best,
Angeliki

On 2018-02-27 16:19, Tobias Nipkow wrote:

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

smime.p7s

Email Gateway (Aug 22 2022 at 16:42):

From: Lawrence Paulson <lp15@cam.ac.uk>
I was also puzzled by this and decided to try a much simpler example: Pythagorean triples. It doesn't take much search to find one of those, but quickcheck (with its default parameters) doesn't manage to find one. Amazingly, nitpick does, although as I gather it doesn't use arithmetic at all but reduces the conjecture to a SAT problem.

lemma "∄A B C::int. 0 < A ∧ 0 < B ∧ 0 < C ∧ AA + BB = C*C"

Nitpick found a counterexample:

Skolem constants:
A = 4
B = 3
C = 5

Larry

Last updated: Nov 21 2024 at 12:39 UTC