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

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


> On 27 Feb 2018, at 16:19, Tobias Nipkow <nipkow at> 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

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