*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 28 Feb 2018 08:47:03 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <39080d46-8655-7346-d1cd-980405e86c81@in.tum.de>*References*: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com> <FDFF8848-06A0-4300-AF7B-ADBB9F30A489@exchange.uibk.ac.at> <CAAi=gevK1B1sGOyoRD4b1jSdCgkytQLV_=z2ckFHhpK+81Hg2g@mail.gmail.com> <68f6ad9b-4697-c321-b24c-61b79471c1a2@sketis.net> <CAAi=gevi-9xYm1x6ct5DNdZAzHtCV-TVn+0e4XbAO6OwjLABNQ@mail.gmail.com> <a1a747187c34ad9df3038496533835d5@cam.ac.uk> <39080d46-8655-7346-d1cd-980405e86c81@in.tum.de>

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 ∧ A*A + B*B = C*C" Nitpick found a counterexample: Skolem constants: A = 4 B = 3 C = 5 Larry > On 27 Feb 2018, at 16:19, Tobias Nipkow <nipkow at in.tum.de> 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

**References**:**[isabelle] Vector transpose***From:*Omar Jasim

**Re: [isabelle] Vector transpose***From:*Thiemann, Rene

**Re: [isabelle] Vector transpose***From:*Omar Jasim

**Re: [isabelle] Vector transpose***From:*Makarius

**Re: [isabelle] Vector transpose***From:*Omar Jasim

**[isabelle] counterexamples to Euler's conjecture with Isabelle***From:*Dr A. Koutsoukou-Argyraki

**Re: [isabelle] counterexamples to Euler's conjecture with Isabelle***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Next by Date: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Previous by Thread: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Next by Thread: Re: [isabelle] counterexamples to Euler's conjecture with Isabelle
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list