feat(OEIS): add solutions from AlphaProof Nexus

FormalConjectures/OEIS/103311.lean

@@ -0,0 +1,81 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Conjectures associated with A103311
+
+A103311: A transform of the Fibonacci numbers.
+The sequence $a(n)$ satisfies the linear recurrence relation:
+$$a(n) = 3a(n-1) - 4a(n-2) + 2a(n-3) - a(n-4)$$
+with initial terms $a(0)=0, a(1)=1, a(2)=1, a(3)=0$.
+The sequence takes values in $\mathbb{Z}$.
+
+*References:*
+- [A103311](https://oeis.org/A103311)
+- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al.
+-/
+
+namespace OeisA103311
+
+
+/--
+A103311: A transform of the Fibonacci numbers.
+The sequence $a(n)$ satisfies the linear recurrence relation:
+$$a(n) = 3a(n-1) - 4a(n-2) + 2a(n-3) - a(n-4)$$
+with initial terms $a(0)=0, a(1)=1, a(2)=1, a(3)=0$.
+The sequence takes values in $\mathbb{Z}$.
+-/
+def a : ℕ → ℤ
+| 0 => 0
+| 1 => 1
+| 2 => 1
+| 3 => 0
+| n + 4 => 3 * a (n + 3) - 4 * a (n + 2) + 2 * a (n + 1) - a n
+
+
+@[category test, AMS 11]
+lemma a_zero : a 0 = 0 := by rfl
+
+@[category test, AMS 11]
+lemma a_one : a 1 = 1 := by rfl
+
+@[category test, AMS 11]
+lemma a_two : a 2 = 1 := by rfl
+
+@[category test, AMS 11]
+lemma a_three : a 3 = 0 := by rfl
+
+@[category test, AMS 11]
+lemma a_four : a 4 = -2 := by rfl
+
+
+/--
+A103311: A transform of the Fibonacci numbers.
+The sequence $a(n)$ satisfies the linear recurrence relation:
+$$a(n) = 3a(n-1) - 4a(n-2) + 2a(n-3) - a(n-4)$$
+with initial terms $a(0)=0, a(1)=1, a(2)=1, a(3)=0$.
+The sequence takes values in $\mathbb{Z}$.
+
+A formal proof has been found with the methods described in [arxiv/2605.22763](https://arxiv.org/abs/2605.22763).
+-/
+@[category research solved, AMS 11, formal_proof using formal_conjectures at
+"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/103311.wip.lean#L218"]
+theorem a_abs_eq_fib (n : ℕ) : ∃ m : ℕ, Int.natAbs (a n) = Nat.fib m := by
+    sorry
+
+end OeisA103311

FormalConjectures/OEIS/108.lean

@@ -0,0 +1,87 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Conjectures associated with A108
+
+A000108 Catalan numbers: C(n) = binomial(2n,n)/(n+1).
+
+The sum $\sum_{i=j}^k \frac{1}{a(i)}$ of reciprocals of Catalan numbers.
+
+*References:*
+- [A108](https://oeis.org/A108)
+- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al.
+-/
+
+namespace OeisA108
+
+
+open Nat Real Finset
+
+/--
+A000108 Catalan numbers: C(n) = binomial(2n,n)/(n+1).
+-/
+def a (n : ℕ) : ℕ := (Nat.choose (2 * n) n) / (n + 1)
+
+def a_rat (n : ℕ) : ℚ := (a n : ℚ)⁻¹
+
+/-- The sum $\sum_{i=j}^k \frac{1}{a(i)}$ of reciprocals of Catalan numbers. -/
+def catalan_reciprocal_sum (j k : ℕ) : ℚ :=
+  (Finset.Icc j k).sum a_rat
+
+/-- The index condition on $(j, k)$ from the conjecture: $0 < \min\{2,k\} \le j \le k$.
+Since j and k are natural numbers, $0 < \min\{2,k\}$ is equivalent to $1 \le k$. -/
+def oeis_108_index_cond (j k : ℕ) : Prop :=
+  1 ≤ k ∧ min 2 k ≤ j ∧ j ≤ k
+
+open Int (fract)
+
+/-- The fractional part of a rational number, viewed as a real number. Must be noncomputable
+due to dependence on the real floor function. -/
+noncomputable def frac_part (q : ℚ) : ℝ := fract (q : ℝ)
+
+
+@[category test, AMS 11]
+lemma a_zero : a 0 = 1 := by rfl
+
+@[category test, AMS 11]
+lemma a_one : a 1 = 1 := by rfl
+
+@[category test, AMS 11]
+lemma a_three : a 3 = 5 := by rfl
+
+@[category test, AMS 11]
+lemma a_four : a 4 = 14 := by rfl
+
+
+/--
+A000108 Catalan numbers: C(n) = binomial(2n,n)/(n+1).
+
+The sum $\sum_{i=j}^k \frac{1}{a(i)}$ of reciprocals of Catalan numbers.
+
+A formal proof has been found with the methods described in [arxiv/2605.22763](https://arxiv.org/abs/2605.22763).
+-/
+@[category research solved, AMS 11, formal_proof using formal_conjectures at
+"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/108.wip.lean#L255"]
+theorem catalan_reciprocal_sum_frac_part_inj : ∀ ⦃j₁ k₁ j₂ k₂ : ℕ⦄,
+    oeis_108_index_cond j₁ k₁ → oeis_108_index_cond j₂ k₂ →
+    (j₁, k₁) ≠ (j₂, k₂) →
+    frac_part (catalan_reciprocal_sum j₁ k₁) ≠ frac_part (catalan_reciprocal_sum j₂ k₂) := by
+    sorry
+
+end OeisA108

FormalConjectures/OEIS/113254.lean

@@ -0,0 +1,84 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Conjectures associated with A113254
+
+A113254: Corresponds to $m = 8$ in a family of 4th-order linear recurrence sequences.
+
+The sequence $a(n)$ is defined by the initial conditions $a(0)=-1, a(1)=4, a(2)=176, a(3)=3136$,
+and the linear recurrence relation
+$a(n) = -4 * a (n-1) + 256 * a (n-3) + 4096 * a (n-4)$ for $n \ge 4$.
+
+*References:*
+- [A113254](https://oeis.org/A113254)
+- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al.
+-/
+
+namespace OeisA113254
+
+
+open Nat Int
+
+/--
+A113254: Corresponds to $m = 8$ in a family of 4th-order linear recurrence sequences.
+
+The sequence $a(n)$ is defined by the initial conditions $a(0)=-1, a(1)=4, a(2)=176, a(3)=3136$,
+and the linear recurrence relation
+$a(n) = -4 * a (n-1) + 256 * a (n-3) + 4096 * a (n-4)$ for $n \ge 4$.
+-/
+def a (n : ℕ) : ℤ :=
+  match n with
+  | 0 => -1
+  | 1 => 4
+  | 2 => 176
+  | 3 => 3136
+  | n' + 4 => -4 * a (n' + 3) + 256 * a (n' + 1) + 4096 * a n'
+
+
+@[category test, AMS 11]
+lemma a_zero : a 0 = -1 := by rfl
+
+@[category test, AMS 11]
+lemma a_one : a 1 = 4 := by rfl
+
+@[category test, AMS 11]
+lemma a_two : a 2 = 176 := by rfl
+
+@[category test, AMS 11]
+lemma a_three : a 3 = 3136 := by rfl
+
+@[category test, AMS 11]
+lemma a_four : a 4 = -15616 := by rfl
+
+
+/--
+A113254: Corresponds to $m = 8$ in a family of 4th-order linear recurrence sequences.
+
+The sequence $a(n)$ is defined by the initial conditions $a(0)=-1, a(1)=4, a(2)=176, a(3)=3136$,
+and the linear recurrence relation
+$a(n) = -4 * a (n-1) + 256 * a (n-3) + 4096 * a (n-4)$ for $n \ge 4$.
+
+A formal proof has been found with the methods described in [arxiv/2605.22763](https://arxiv.org/abs/2605.22763).
+-/
+@[category research solved, AMS 11, formal_proof using formal_conjectures at
+"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/113254.wip.lean#L130"]
+theorem a_odd_is_square : ∀ n : ℕ, IsSquare (a (2 * n + 1)) := by
+    sorry
+
+end OeisA113254

FormalConjectures/OEIS/175386.lean

@@ -0,0 +1,85 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Conjectures associated with A175386
+
+A175386: $a(n)$ is the denominator of the sum
+$$\sum_{i=1}^n \frac{1}{i} \binom{2n-i-1}{i-1}$$
+
+The sum which A175386 $a(n)$ is the denominator of.
+
+*References:*
+- [A175386](https://oeis.org/A175386)
+- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al.
+-/
+
+namespace OeisA175386
+
+
+/--
+A175386: $a(n)$ is the denominator of the sum
+$$\sum_{i=1}^n \frac{1}{i} \binom{2n-i-1}{i-1}$$
+-/
+def a (n : ℕ) : ℕ :=
+  (Finset.sum (Finset.Icc 1 n) fun i : ℕ =>
+    -- The upper index is $2n - i - 1$, which is equivalent to
+    -- $2n - (i+1)$ in $\mathbb{N}$ for $i \le n$.
+    -- The lower index $i-1$ is standard subtraction in $\mathbb{N}$.
+    let num : ℕ := Nat.choose (2 * n - (i + 1)) (i - 1)
+    (num : ℚ) / (i : ℚ)
+  ).den
+
+/-- The sum which A175386 $a(n)$ is the denominator of. -/
+def S (n : ℕ) : ℚ :=
+  Finset.sum (Finset.Icc 1 n) fun i : ℕ =>
+    let num : ℕ := Nat.choose (2 * n - (i + 1)) (i - 1)
+    (num : ℚ) / (i : ℚ)
+
+
+
+@[category test, AMS 11]
+lemma a_one : a 1 = 1 := by native_decide
+
+@[category test, AMS 11]
+lemma a_two : a 2 = 2 := by native_decide
+
+@[category test, AMS 11]
+lemma a_three : a 3 = 6 := by native_decide
+
+@[category test, AMS 11]
+lemma a_four : a 4 = 4 := by native_decide
+
+@[category test, AMS 11]
+lemma a_five : a 5 = 5 := by native_decide
+
+
+/--
+A175386: $a(n)$ is the denominator of the sum
+$$\sum_{i=1}^n \frac{1}{i} \binom{2n-i-1}{i-1}$$
+
+The sum which A175386 $a(n)$ is the denominator of.
+
+A formal proof has been found with the methods described in [arxiv/2605.22763](https://arxiv.org/abs/2605.22763).
+-/
+@[category research solved, AMS 11, formal_proof using formal_conjectures at
+"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/175386.wip.lean#L304"]
+theorem a_ne_one (n : ℕ) (hn : 1 < n) : a n ≠ 1 := by
+    sorry
+
+end OeisA175386