Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Aug 22 2022 at 16:40):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
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


Last updated: Mar 28 2024 at 20:16 UTC