Claims

../

2024_07_21_seamans: With k=2 every integer n at least 0 is 2(n+2) minus (2+(n+2)), so the question as stated has the answer yes; credited by the site's curator.

2025_12_27_alexeev: A Lean proof that k=2 works, generated by Aristotle and by ChatGPT and posted by Boris Alexeev on the site's thread on 27 December 2025; its file also names Seed-Prover 1.5 and Zheng Yuan; not built by this corpus.

---