1. FormalConjectures
  2. OEIS
  3. «224515»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Existence of integers $k$ with $k^2 \operatorname{XOR} (k+1)^2 = (2n+1)^2$

a: $a(n) = \text{least } k \text{ such that } \sqrt{k^2 \operatorname{XOR} (k+1)^2} = 2n+1$, $a(n) = -1 \text{ if there is no such } k$. This is equivalent to finding the smallest $k \in \mathbb{N}$ such that $k^2 \oplus (k+1)^2 = (2n+1)^2$. We use the set infimum ($\operatorname{sInf}$) to denote the least element of the set of natural numbers satisfying the condition. Since Mathlib's sInf on a subset of ℕ gives a result in ℕ, this definition is only completely faithful to the OEIS when the set is non-empty. The OEIS definition implies that the set of k's is non-empty for all n.

References:

    A224515

    arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

namespace OeisA224515open Nat Set

a: $a(n) = \text{least } k \text{ such that } \sqrt{k^2 \operatorname{XOR} (k+1)^2} = 2n+1$, $a(n) = -1 \text{ if there is no such } k$. This is equivalent to finding the smallest $k \in \mathbb{N}$ such that $k^2 \oplus (k+1)^2 = (2n+1)^2$. We use the set infimum ($\operatorname{sInf}$) to denote the least element of the set of natural numbers satisfying the condition. Since Mathlib's sInf on a subset of ℕ gives a result in ℕ, this definition is only completely faithful to the OEIS when the set is non-empty. The OEIS definition implies that the set of k's is non-empty for all n, which is legitimate as shown by the theorem exists_xor_sq_eq below.

noncomputable def a (n : ℕ) : ℕ := -- The term (2*n + 1)^2 is the target value. let target_sq : ℕ := (2 * n + 1) ^ 2 -- Define the set of candidate k's. sInf { k : ℕ | Nat.xor (k ^ 2) ((k + 1) ^ 2) = target_sq }@[category API, AMS 11] lemma A224515_eq (n val : ℕ) (h_in : Nat.xor (val ^ 2) ((val + 1) ^ 2) = (2 * n + 1) ^ 2) (h_min : ∀ k < val, Nat.xor (k ^ 2) ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2) : a n = val := n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2⊢ a n = val n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2⊢ (have target_sq := (2 * n + 1) ^ 2; sInf {k | (k ^ 2).xor ((k + 1) ^ 2) = target_sq}) = val n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2⊢ sInf {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2} = val n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2⊢ ∀ a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}, val ≤ an:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2⊢ ∀ (w : ℕ), val < w → ∃ a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}, a < w n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2⊢ ∀ a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}, val ≤ a n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2a:ℕha:a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}⊢ val ≤ a n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2a:ℕha:a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}h:¬val ≤ a⊢ False exact h_min a (n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2a:ℕha:a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}h:¬val ≤ a⊢ a < val All goals completed! 🐙) ha n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2⊢ ∀ (w : ℕ), val < w → ∃ a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}, a < w n:ℕval:ℕh_in:(val ^ 2).xor ((val + 1) ^ 2) = (2 * n + 1) ^ 2h_min:∀ k < val, (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * n + 1) ^ 2w:ℕhw:val < w⊢ ∃ a ∈ {k | (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2}, a < w All goals completed! 🐙@[category test, AMS 11] lemma a_0 : a 0 = 0 := ⊢ a 0 = 0 apply A224515_eq 0 0 (⊢ (0 ^ 2).xor ((0 + 1) ^ 2) = (2 * 0 + 1) ^ 2 All goals completed! 🐙) k:ℕhk:k < 0⊢ (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * 0 + 1) ^ 2; All goals completed! 🐙@[category test, AMS 11] lemma a_1 : a 1 = 4 := ⊢ a 1 = 4 apply A224515_eq 1 4 (⊢ (4 ^ 2).xor ((4 + 1) ^ 2) = (2 * 1 + 1) ^ 2 All goals completed! 🐙) k:ℕhk:k < 4⊢ (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2; k:ℕhk:0 < 4⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2k:ℕhk:1 < 4⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2k:ℕhk:2 < 4⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2k:ℕhk:3 < 4⊢ (3 ^ 2).xor ((3 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2 k:ℕhk:0 < 4⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2k:ℕhk:1 < 4⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2k:ℕhk:2 < 4⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2k:ℕhk:3 < 4⊢ (3 ^ 2).xor ((3 + 1) ^ 2) ≠ (2 * 1 + 1) ^ 2 All goals completed! 🐙@[category test, AMS 11] lemma a_2 : a 2 = 3 := ⊢ a 2 = 3 apply A224515_eq 2 3 (⊢ (3 ^ 2).xor ((3 + 1) ^ 2) = (2 * 2 + 1) ^ 2 All goals completed! 🐙) k:ℕhk:k < 3⊢ (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * 2 + 1) ^ 2; k:ℕhk:0 < 3⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 2 + 1) ^ 2k:ℕhk:1 < 3⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 2 + 1) ^ 2k:ℕhk:2 < 3⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 2 + 1) ^ 2 k:ℕhk:0 < 3⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 2 + 1) ^ 2k:ℕhk:1 < 3⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 2 + 1) ^ 2k:ℕhk:2 < 3⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 2 + 1) ^ 2 All goals completed! 🐙@[category test, AMS 11] lemma a_3 : a 3 = 24 := ⊢ a 3 = 24 apply A224515_eq 3 24 (⊢ (24 ^ 2).xor ((24 + 1) ^ 2) = (2 * 3 + 1) ^ 2 All goals completed! 🐙) k:ℕhk:k < 24⊢ (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2; k:ℕhk:0 < 24⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:1 < 24⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:2 < 24⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:3 < 24⊢ (3 ^ 2).xor ((3 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:4 < 24⊢ (4 ^ 2).xor ((4 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:5 < 24⊢ (5 ^ 2).xor ((5 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:6 < 24⊢ (6 ^ 2).xor ((6 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:7 < 24⊢ (7 ^ 2).xor ((7 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:8 < 24⊢ (8 ^ 2).xor ((8 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:9 < 24⊢ (9 ^ 2).xor ((9 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:10 < 24⊢ (10 ^ 2).xor ((10 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:11 < 24⊢ (11 ^ 2).xor ((11 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:12 < 24⊢ (12 ^ 2).xor ((12 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:13 < 24⊢ (13 ^ 2).xor ((13 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:14 < 24⊢ (14 ^ 2).xor ((14 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:15 < 24⊢ (15 ^ 2).xor ((15 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:16 < 24⊢ (16 ^ 2).xor ((16 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:17 < 24⊢ (17 ^ 2).xor ((17 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:18 < 24⊢ (18 ^ 2).xor ((18 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:19 < 24⊢ (19 ^ 2).xor ((19 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:20 < 24⊢ (20 ^ 2).xor ((20 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:21 < 24⊢ (21 ^ 2).xor ((21 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:22 < 24⊢ (22 ^ 2).xor ((22 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:23 < 24⊢ (23 ^ 2).xor ((23 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2 k:ℕhk:0 < 24⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:1 < 24⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:2 < 24⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:3 < 24⊢ (3 ^ 2).xor ((3 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:4 < 24⊢ (4 ^ 2).xor ((4 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:5 < 24⊢ (5 ^ 2).xor ((5 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:6 < 24⊢ (6 ^ 2).xor ((6 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:7 < 24⊢ (7 ^ 2).xor ((7 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:8 < 24⊢ (8 ^ 2).xor ((8 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:9 < 24⊢ (9 ^ 2).xor ((9 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:10 < 24⊢ (10 ^ 2).xor ((10 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:11 < 24⊢ (11 ^ 2).xor ((11 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:12 < 24⊢ (12 ^ 2).xor ((12 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:13 < 24⊢ (13 ^ 2).xor ((13 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:14 < 24⊢ (14 ^ 2).xor ((14 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:15 < 24⊢ (15 ^ 2).xor ((15 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:16 < 24⊢ (16 ^ 2).xor ((16 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:17 < 24⊢ (17 ^ 2).xor ((17 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:18 < 24⊢ (18 ^ 2).xor ((18 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:19 < 24⊢ (19 ^ 2).xor ((19 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:20 < 24⊢ (20 ^ 2).xor ((20 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:21 < 24⊢ (21 ^ 2).xor ((21 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:22 < 24⊢ (22 ^ 2).xor ((22 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2k:ℕhk:23 < 24⊢ (23 ^ 2).xor ((23 + 1) ^ 2) ≠ (2 * 3 + 1) ^ 2 All goals completed! 🐙@[category test, AMS 11] lemma a_4 : a 4 = 23 := ⊢ a 4 = 23 apply A224515_eq 4 23 (⊢ (23 ^ 2).xor ((23 + 1) ^ 2) = (2 * 4 + 1) ^ 2 All goals completed! 🐙) k:ℕhk:k < 23⊢ (k ^ 2).xor ((k + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2; k:ℕhk:0 < 23⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:1 < 23⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:2 < 23⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:3 < 23⊢ (3 ^ 2).xor ((3 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:4 < 23⊢ (4 ^ 2).xor ((4 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:5 < 23⊢ (5 ^ 2).xor ((5 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:6 < 23⊢ (6 ^ 2).xor ((6 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:7 < 23⊢ (7 ^ 2).xor ((7 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:8 < 23⊢ (8 ^ 2).xor ((8 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:9 < 23⊢ (9 ^ 2).xor ((9 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:10 < 23⊢ (10 ^ 2).xor ((10 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:11 < 23⊢ (11 ^ 2).xor ((11 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:12 < 23⊢ (12 ^ 2).xor ((12 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:13 < 23⊢ (13 ^ 2).xor ((13 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:14 < 23⊢ (14 ^ 2).xor ((14 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:15 < 23⊢ (15 ^ 2).xor ((15 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:16 < 23⊢ (16 ^ 2).xor ((16 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:17 < 23⊢ (17 ^ 2).xor ((17 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:18 < 23⊢ (18 ^ 2).xor ((18 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:19 < 23⊢ (19 ^ 2).xor ((19 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:20 < 23⊢ (20 ^ 2).xor ((20 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:21 < 23⊢ (21 ^ 2).xor ((21 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:22 < 23⊢ (22 ^ 2).xor ((22 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2 k:ℕhk:0 < 23⊢ (0 ^ 2).xor ((0 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:1 < 23⊢ (1 ^ 2).xor ((1 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:2 < 23⊢ (2 ^ 2).xor ((2 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:3 < 23⊢ (3 ^ 2).xor ((3 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:4 < 23⊢ (4 ^ 2).xor ((4 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:5 < 23⊢ (5 ^ 2).xor ((5 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:6 < 23⊢ (6 ^ 2).xor ((6 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:7 < 23⊢ (7 ^ 2).xor ((7 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:8 < 23⊢ (8 ^ 2).xor ((8 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:9 < 23⊢ (9 ^ 2).xor ((9 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:10 < 23⊢ (10 ^ 2).xor ((10 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:11 < 23⊢ (11 ^ 2).xor ((11 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:12 < 23⊢ (12 ^ 2).xor ((12 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:13 < 23⊢ (13 ^ 2).xor ((13 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:14 < 23⊢ (14 ^ 2).xor ((14 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:15 < 23⊢ (15 ^ 2).xor ((15 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:16 < 23⊢ (16 ^ 2).xor ((16 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:17 < 23⊢ (17 ^ 2).xor ((17 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:18 < 23⊢ (18 ^ 2).xor ((18 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:19 < 23⊢ (19 ^ 2).xor ((19 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:20 < 23⊢ (20 ^ 2).xor ((20 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:21 < 23⊢ (21 ^ 2).xor ((21 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2k:ℕhk:22 < 23⊢ (22 ^ 2).xor ((22 + 1) ^ 2) ≠ (2 * 4 + 1) ^ 2 All goals completed! 🐙

Conjecture: $a(n) \ge 0$, i.e., for every $n$ there exists $k$ such that $\sqrt{k^2 \oplus (k+1)^2} = 2n+1$.

A formal proof has been found with the methods described in arxiv/2605.22763.

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/224515.wip.lean#L268"] theorem exists_xor_sq_eq (n : ℕ) : ∃ k : ℕ, Nat.xor (k ^ 2) ((k + 1) ^ 2) = (2 * n + 1) ^ 2 := n:ℕ⊢ ∃ k, (k ^ 2).xor ((k + 1) ^ 2) = (2 * n + 1) ^ 2 All goals completed! 🐙end OeisA224515