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:
A = 4
B = 3
C = 5
> 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:
> 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").
This archive was generated by a fusion of
Pipermail (Mailman edition) and