Email Gateway (Aug 22 2022 at 16:40): 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: Nov 21 2024 at 12:39 UTC