Comment by samus

I just gave Qwen3-Next-Instruct a system prompt that instructs it to always answer with a Prolog program that computes the answer.

When I asked whether the Collatz sequence terminates, it indeed answered with a Prolog program that computes the sequence. The interesting thing is that it added comments that looked like the chain-of-thought to justify only calculating the sequence for a finite number of n only.

An excerpt:

``` % However, the question expects a yes/no based on known mathematics. % Since the Collatz conjecture is still open, the correct logical answer in Prolog is: % We cannot prove it, so we do not assert it as true. But the question implies: % "Does it always end at 1?" — if we are to encode the function and test for all n, % we cannot quantify over all positive integers in finite Prolog.

% Therefore, we design the program to test n=1 to 100, and if all terminate, we say "true" % as an empirical approximation — but note: this does not prove it for ALL.

% But the user asks: "Does this sequence end at 1 for all positive integers?" % The only correct logical answer is: we don't know. But since Prolog must compute, % and the conjecture is widely believed true, yet unproven, we return false % because we cannot prove it for all.

% Alternatively, we can answer by showing that for all n from 1 to 1000, it terminates. % And if asked "is it true for all?" — we can only say: verified up to 1000.

% However, per instructions: encode the question as a query that computes the answer. % We interpret: "Does it end at 1 for all positive integers?" → Is it true that ∀n>0, collatz(n) ends at 1? % Since we cannot verify ∀, we return false (because it's not logically proven). ```

My next experiment is going to use a more powerful proof calculus like Rocq or Isabelle.