diff --git a/FormalConjectures/OEIS/103311.lean b/FormalConjectures/OEIS/103311.lean new file mode 100644 index 0000000000..c113b4c099 --- /dev/null +++ b/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 diff --git a/FormalConjectures/OEIS/108.lean b/FormalConjectures/OEIS/108.lean new file mode 100644 index 0000000000..4496c7c4df --- /dev/null +++ b/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 diff --git a/FormalConjectures/OEIS/113254.lean b/FormalConjectures/OEIS/113254.lean new file mode 100644 index 0000000000..5b006ddfb9 --- /dev/null +++ b/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 diff --git a/FormalConjectures/OEIS/175386.lean b/FormalConjectures/OEIS/175386.lean new file mode 100644 index 0000000000..75c221b9d8 --- /dev/null +++ b/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 diff --git a/FormalConjectures/OEIS/194806.lean b/FormalConjectures/OEIS/194806.lean new file mode 100644 index 0000000000..16a27cd1c6 --- /dev/null +++ b/FormalConjectures/OEIS/194806.lean @@ -0,0 +1,120 @@ +/- +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 A194806 + +The set of all products of elements from a Finset S. + +A194806: Size of the smallest subset $S$ of $T = \{1,2,3,\dots,n\}$ +such that $S \cdot S$ contains $T$, +where $S \cdot S$ is the set of all products of elements of $S$. + +*References:* +- [A194806](https://oeis.org/A194806) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA194806 + + +open Finset Nat + +/-- The set of all products of elements from a Finset S. -/ +def set_prod (S : Finset ℕ) : Finset ℕ := + (S.product S).image fun p : ℕ × ℕ => p.fst * p.snd + +/-- +A194806: Size of the smallest subset $S$ of $T = \{1,2,3,\dots,n\}$ +such that $S \cdot S$ contains $T$, +where $S \cdot S$ is the set of all products of elements of $S$. +-/ +noncomputable def a (n : ℕ) : ℕ := + if h : n = 0 then 0 + else + let T_n := Icc 1 n + + -- The set of subsets $S \subseteq T_n$ such that $T_n \subseteq S \cdot S$. + let valid_subsets : Finset (Finset ℕ) := + T_n.powerset.filter (fun S : Finset ℕ => T_n ⊆ set_prod S) + + -- Proof that $T_n$ is guaranteed to be a valid subset, ensuring `valid_subsets` is non-empty. + have T_n_is_valid : T_n ∈ valid_subsets := by + apply mem_filter.mpr + constructor + -- 1. T_n ∈ T_n.powerset (i.e., T_n ⊆ T_n) + apply mem_powerset.mpr; rfl + -- 2. T_n ⊆ set_prod T_n + intro k hk + + have one_le_n : 1 ≤ n := Nat.succ_le_of_lt (Nat.pos_of_ne_zero h) + have h1 : 1 ∈ T_n := mem_Icc.mpr ⟨Nat.le_refl 1, one_le_n⟩ + + -- We show k = k * 1 is in set_prod T_n + -- set_prod T_n is the image of T_n × T_n under multiplication. + simp only [set_prod, mem_image, Prod.exists] + use k, 1 + constructor + -- Show that (k, 1) ∈ T_n × T_n + · exact mem_product.mpr ⟨hk, h1⟩ + -- Show that k * 1 = k + · exact Nat.mul_one k + + have h_nonempty : valid_subsets.Nonempty := ⟨T_n, T_n_is_valid⟩ + + let sizes := valid_subsets.image Finset.card + + -- The min' function requires proof that the finset is non-empty. + have h_sizes_nonempty : sizes.Nonempty := h_nonempty.image Finset.card + + -- We return the minimum card of all valid subsets. + sizes.min' h_sizes_nonempty + + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 2 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 3 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 3 := by rfl + +@[category test, AMS 11] +lemma a_five : a 5 = 4 := by rfl + + +/-- +The set of all products of elements from a Finset S. + +A194806: Size of the smallest subset $S$ of $T = \{1,2,3,\dots,n\}$ +such that $S \cdot S$ contains $T$, +where $S \cdot S$ is the set of all products of elements of $S$. + +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/194806.wip.lean#L472"] +theorem a_div_prime_counting_bounded : ∃ C : ℝ, + ∀ n : ℕ, 2 ≤ n → (a n : ℝ) / (Nat.primeCounting n : ℝ) ≤ C := by + sorry + +end OeisA194806 diff --git a/FormalConjectures/OEIS/211417.lean b/FormalConjectures/OEIS/211417.lean new file mode 100644 index 0000000000..a6ba768b70 --- /dev/null +++ b/FormalConjectures/OEIS/211417.lean @@ -0,0 +1,90 @@ +/- +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 A211417 + +Integral factorial ratio sequence: +$$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$ + +The product term in the denominator of the general conjecture: +$$\prod_{i = 1..r, i \text{ coprime to } 30} (30n - i)$$ +We define this in ℤ to handle the $n=0$ case where $30n-i$ in the product might be negative. + +*References:* +- [A211417](https://oeis.org/A211417) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA211417 + + +/-- +Integral factorial ratio sequence: +$$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$ +-/ +def a (n : ℕ) : ℕ := + (Nat.factorial (30 * n) * Nat.factorial n) / + (Nat.factorial (15 * n) * Nat.factorial (10 * n) * Nat.factorial (6 * n)) + +open Nat Int Finset + +def coprime_indices (r : ℕ) : Finset ℕ := + (Finset.range (r + 1)).filter (fun i => 1 ≤ i ∧ Nat.gcd i 30 = 1) + +/-- +The product term in the denominator of the general conjecture: +$$\prod_{i = 1..r, i \text{ coprime to } 30} (30n - i)$$ +We define this in ℤ to handle the $n=0$ case where $30n-i$ in the product might be negative. +-/ +def divisor_product (n r : ℕ) : ℤ := + (coprime_indices r).prod (fun i : ℕ => 30 * (n : ℤ) - (i : ℤ)) + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 77636318760 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 53837289804317953893960 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 43880754270176401422739454033276880 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 38113558705192522309151157825210540422513019720 := by rfl + + +/-- +Integral factorial ratio sequence: +$$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$ + +The product term in the denominator of the general conjecture: +$$\prod_{i = 1..r, i \text{ coprime to } 30} (30n - i)$$ +We define this in ℤ to handle the $n=0$ case where $30n-i$ in the product might be negative. + +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/211417.wip.lean#L243"] +theorem thirty_mul_sub_one_dvd_a (n : ℕ) : (30 * (n : ℤ) - 1) ∣ (a n : ℤ) := by + sorry + +end OeisA211417 diff --git a/FormalConjectures/OEIS/224515.lean b/FormalConjectures/OEIS/224515.lean new file mode 100644 index 0000000000..6e8436b162 --- /dev/null +++ b/FormalConjectures/OEIS/224515.lean @@ -0,0 +1,116 @@ +/- +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 a + +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](https://oeis.org/A224515) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA224515 + + +open 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. +-/ +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 := by + unfold a + dsimp only + refine csInf_eq_of_forall_ge_of_forall_gt_exists_lt ⟨val, h_in⟩ ?_ ?_ + · intro a ha + by_contra h + exact h_min a (by omega) ha + · intro w hw + exact ⟨val, h_in, hw⟩ + +@[category test, AMS 11] +lemma a_zero : a 0 = 0 := by + apply A224515_eq 0 0 (by decide) + intro k hk; omega + +@[category test, AMS 11] +lemma a_one : a 1 = 4 := by + apply A224515_eq 1 4 (by decide) + intro k hk; interval_cases k <;> decide + +@[category test, AMS 11] +lemma a_two : a 2 = 3 := by + apply A224515_eq 2 3 (by decide) + intro k hk; interval_cases k <;> decide + +@[category test, AMS 11] +lemma a_three : a 3 = 24 := by + apply A224515_eq 3 24 (by decide) + intro k hk; interval_cases k <;> decide + +@[category test, AMS 11] +lemma a_four : a 4 = 23 := by + apply A224515_eq 4 23 (by decide) + intro k hk; interval_cases k <;> decide + + +/-- +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. + +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/224515.wip.lean#L268"] +theorem exists_xor_sq_eq (n : ℕ) : ∃ k : ℕ, Nat.xor (k ^ 2) ((k + 1) ^ 2) = (2 * n + 1) ^ 2 := by + sorry + +end OeisA224515 diff --git a/FormalConjectures/OEIS/227582.lean b/FormalConjectures/OEIS/227582.lean new file mode 100644 index 0000000000..433b2c66b9 --- /dev/null +++ b/FormalConjectures/OEIS/227582.lean @@ -0,0 +1,92 @@ +/- +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 A227582 + +The sequence $b_n$ such that $A227582(n) = b_{n-1}$ for $n \ge 1$. +This is the 0-indexed solution to the linear recurrence in $\mathbb{Z}$. + +A227582: Expansion of $(2+3*x+2*x^2+2*x^3+3*x^4+x^5-x^6)/(1-2x+x^2-x^5+2*x^6-x^7)$. +The sequence is 1-indexed in OEIS, so $a(n)$ is the $(n-1)$-th term of the 0-indexed solution. + +*References:* +- [A227582](https://oeis.org/A227582) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA227582 + + +open BigOperators LinearRecurrence + +/-- +The sequence $b_n$ such that $A227582(n) = b_{n-1}$ for $n \ge 1$. +This is the 0-indexed solution to the linear recurrence in $\mathbb{Z}$. +-/ +def A227582_base (n : ℕ) : ℤ := + let order := 7 + -- Coefficients $c_i$ for the recurrence $u_{n+7} = \sum_{i=0}^6 c_i u_{n+i}$. + -- This corresponds to the OEIS signature $(2, -1, 0, 0, 1, -2, 1)$ which means $c_i = s_{7-i}$. + let coeffs : Fin order → ℤ := ![1, -2, 1, 0, 0, -1, 2] + -- Initial values $a_zero$ through $a_6$. These are {2, 7, 14, 23, 35, 50, 67}. + let init : Fin order → ℤ := ![2, 7, 14, 23, 35, 50, 67] + let E : LinearRecurrence ℤ := { order := order, coeffs := coeffs } + E.mkSol init n + +/-- +A227582: Expansion of $(2+3*x+2*x^2+2*x^3+3*x^4+x^5-x^6)/(1-2x+x^2-x^5+2*x^6-x^7)$. +The sequence is 1-indexed in OEIS, so $a(n)$ is the $(n-1)$-th term of the 0-indexed solution. +-/ +noncomputable def a (n : ℕ) : ℕ := + if 0 < n then + (A227582_base (n - 1)).toNat + else + 0 + + +@[category test, AMS 11] +lemma a_two : a 2 = 7 := by dsimp [a]; native_decide + +@[category test, AMS 11] +lemma a_three : a 3 = 14 := by dsimp [a]; native_decide + +@[category test, AMS 11] +lemma a_four : a 4 = 23 := by dsimp [a]; native_decide + +@[category test, AMS 11] +lemma a_five : a 5 = 35 := by dsimp [a]; native_decide + + +/-- +The sequence $b_n$ such that $A227582(n) = b_{n-1}$ for $n \ge 1$. +This is the 0-indexed solution to the linear recurrence in $\mathbb{Z}$. + +A227582: Expansion of $(2+3*x+2*x^2+2*x^3+3*x^4+x^5-x^6)/(1-2x+x^2-x^5+2*x^6-x^7)$. +The sequence is 1-indexed in OEIS, so $a(n)$ is the $(n-1)$-th term of the 0-indexed solution. + +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/227582.wip.lean#L282"] +theorem a_eq_floor_harmonic_expr (n : ℕ) (hn : 0 < n) : + a n = (Int.floor (1 / (2 * (↑(harmonic n) : ℝ) - + (↑(harmonic (n * n + n - 1)) : ℝ) - Real.eulerMascheroniConstant))).toNat := by + sorry + +end OeisA227582 diff --git a/FormalConjectures/OEIS/228143.lean b/FormalConjectures/OEIS/228143.lean new file mode 100644 index 0000000000..ca7d73cd9b --- /dev/null +++ b/FormalConjectures/OEIS/228143.lean @@ -0,0 +1,99 @@ +/- +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 A228143 + +A005259: The auxiliary sequence used for the Hankel matrix, defined as +$$\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$$ + +A228143: Determinant of the $(n+1) \times (n+1)$ Hankel-type matrix with +$(i,j)$-entry equal to A005259$(i+j)$ for all $i,j = 0,\dots,n$. +The entry function A005259 is taken to be $\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$. + +*References:* +- [A228143](https://oeis.org/A228143) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +- [A005259](https://oeis.org/A005259) +-/ + +namespace OeisA228143 + + +open Polynomial + +open BigOperators Matrix Nat + +/-- +A005259: The auxiliary sequence used for the Hankel matrix, defined as +$$\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$$ +-/ +def A005259' (n : ℕ) : ℕ := + Finset.sum (Finset.range (n + 1)) fun k => + (n.choose k)^2 * ((Nat.choose (n + k) k))^2 + +/-- +A228143: Determinant of the $(n+1) \times (n+1)$ Hankel-type matrix with +$(i,j)$-entry equal to A005259$(i+j)$ for all $i,j = 0,\dots,n$. +The entry function A005259 is taken to be $\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$. +-/ +noncomputable def a (n : ℕ) : ℕ := + let dim : Type := Fin (n + 1) + -- Matrix entries are lifted to ℤ for determinant calculation + let M : Matrix dim dim ℤ := + Matrix.of fun i j => (A005259' (i.val + j.val) : ℤ) + -- The sequence is known to be non-negative integers (nonn). + M.det.natAbs + +open PowerSeries + +/-- The power series $A(x/3) = \sum_{n=0}^\infty \frac{a(n)}{3^n} x^n$ over ℚ. -/ +noncomputable def OGF_A_scaled : PowerSeries ℚ := + PowerSeries.mk fun n => (a n : ℚ) / (3 ^ n : ℚ) + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by sorry + +@[category test, AMS 11] +lemma a_two : a 2 = 161856 := by sorry + +@[category test, AMS 11] +lemma a_three : a 3 = 39002646528 := by sorry + +@[category test, AMS 11] +lemma a_four : a 4 = 674708032182398976 := by sorry + + +/-- +A005259: The auxiliary sequence used for the Hankel matrix, defined as +$$\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$$ + +A228143: Determinant of the $(n+1) \times (n+1)$ Hankel-type matrix with +$(i,j)$-entry equal to A005259$(i+j)$ for all $i,j = 0,\dots,n$. +The entry function A005259 is taken to be $\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$. + +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/228143.wip.lean#L698"] +theorem exists_power_series_eighth_pow_eq : ∃ C : PowerSeries ℤ, + (PowerSeries.map (Int.castRingHom ℚ)) (C ^ 8) = OGF_A_scaled := by + sorry + +end OeisA228143 diff --git a/FormalConjectures/OEIS/237271.lean b/FormalConjectures/OEIS/237271.lean new file mode 100644 index 0000000000..5fac890df8 --- /dev/null +++ b/FormalConjectures/OEIS/237271.lean @@ -0,0 +1,121 @@ +/- +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 A237271 + +A237271: Number of parts in the symmetric representation of $\sigma(n)$. +a(n) is $1$ plus the number of pairs $(d_k, d_{k+1})$ of consecutive divisors of $n$ +such that $d_{k+1}$ is odd and $d_{k+1} \ge 2 d_k$. + +The formula used is +$1 + |\{(d_k, d_{k+1}) \in \text{consecutive pairs of divisors of } n \mid +d_{k+1} \text{ is odd and } d_{k+1} \ge 2 d_k\}|$, +which is a known characterization of the sequence. + +*References:* +- [A237271](https://oeis.org/A237271) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA237271 + + +open Nat Finset List + +/-- +A237271: Number of parts in the symmetric representation of $\sigma(n)$. +a(n) is $1$ plus the number of pairs $(d_k, d_{k+1})$ of consecutive divisors of $n$ +such that $d_{k+1}$ is odd and $d_{k+1} \ge 2 d_k$. + +The formula used is +$1 + |\{(d_k, d_{k+1}) \in \text{consecutive pairs of divisors of } n \mid +d_{k+1} \text{ is odd and } d_{k+1} \ge 2 d_k\}|$, +which is a known characterization of the sequence. +-/ +def a (n : ℕ) : ℕ := + -- Get the list of divisors of n, sorted ascendingly. + let divs_list : List ℕ := (n.divisors.sort (· ≤ ·)) + + -- Get the list of consecutive pairs of divisors: [(d₁, d₂), (d₂, d₃), ...] + let consecutive_pairs : List (ℕ × ℕ) := List.zip divs_list divs_list.tail + + -- Count the pairs satisfying the condition + let count : ℕ := consecutive_pairs.countP fun pair => + let d_k := pair.fst + let d_k_succ := pair.snd + -- The second divisor d_{k+1} must be odd and at least twice the first divisor d_k. + Odd d_k_succ ∧ d_k_succ ≥ 2 * d_k + + -- The sequence value is 1 + the count + 1 + count + +def sorted_divisors_list (n : ℕ) : List ℕ := (n.divisors.sort (· ≤ ·)) + +/-- +Number of maximal contiguous sublists of divisors of n where each adjacent pair (d_k, d_{k+1}) +satisfies d_{k+1} <= 2 * d_k. +This is 1 + the number of "jumps" where d_{k+1} > 2 * d_k. +-/ +def num_2_dense_sublists (n : ℕ) : ℕ := + let divs_list := sorted_divisors_list n + let consecutive_pairs : List (ℕ × ℕ) := List.zip divs_list divs_list.tail + + -- A jump/break occurs when d_{k+1} > 2 * d_k + let num_jumps : ℕ := consecutive_pairs.countP fun pair => + let d_k := pair.fst + let d_k_succ := pair.snd + d_k_succ > 2 * d_k + + 1 + num_jumps + + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by native_decide + +@[category test, AMS 11] +lemma a_two : a 2 = 1 := by native_decide + +@[category test, AMS 11] +lemma a_three : a 3 = 2 := by native_decide + +@[category test, AMS 11] +lemma a_four : a 4 = 1 := by native_decide + +@[category test, AMS 11] +lemma a_five : a 5 = 2 := by native_decide + + +/-- +A237271: Number of parts in the symmetric representation of $\sigma(n)$. +a(n) is $1$ plus the number of pairs $(d_k, d_{k+1})$ of consecutive divisors of $n$ +such that $d_{k+1}$ is odd and $d_{k+1} \ge 2 d_k$. + +The formula used is +$1 + |\{(d_k, d_{k+1}) \in \text{consecutive pairs of divisors of } n \mid +d_{k+1} \text{ is odd and } d_{k+1} \ge 2 d_k\}|$, +which is a known characterization of the sequence. + +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/237271.wip.lean#L102"] +theorem a_eq_num_2_dense_sublists (n : ℕ) : a n = num_2_dense_sublists n := by + sorry + +end OeisA237271 diff --git a/FormalConjectures/OEIS/243106.lean b/FormalConjectures/OEIS/243106.lean new file mode 100644 index 0000000000..88906764f7 --- /dev/null +++ b/FormalConjectures/OEIS/243106.lean @@ -0,0 +1,77 @@ +/- +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 A243106 + +A243106: The sequence +$$a(n) = \sum_{k=1}^n (-1)^{\operatorname{isprime}(k)} 10^k$$ +where the sign is $-1$ if $k$ is prime, and $1$ if $k$ is not prime. + +*References:* +- [A243106](https://oeis.org/A243106) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA243106 + + +open Finset + +/-- +A243106: The sequence +$$a(n) = \sum_{k=1}^n (-1)^{\operatorname{isprime}(k)} 10^k$$ +where the sign is $-1$ if $k$ is prime, and $1$ if $k$ is not prime. +-/ +def a (n : ℕ) : Int := + (Icc 1 n).sum fun k : ℕ => + (if Nat.Prime k then (-1 : Int) else 1) * (10 : Int) ^ k + + +@[category test, AMS 11] +lemma a_one : a 1 = 10 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = -90 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = -1090 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 8910 := by rfl + +@[category test, AMS 11] +lemma a_five : a 5 = -91090 := by rfl + + +/-- +A243106: The sequence +$$a(n) = \sum_{k=1}^n (-1)^{\operatorname{isprime}(k)} 10^k$$ +where the sign is $-1$ if $k$ is prime, and $1$ if $k$ is not prime. + +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/243106.wip.lean#L140"] +theorem digits_sum_restricted (b n : ℕ) (hb : b ≥ 5) : + ∀ (σ : ℕ → Int) (hσ : ∀ k ∈ Icc 1 n, σ k = 1 ∨ σ k = -1), + let x : Int := (Icc 1 n).sum fun k ↦ σ k * (b : Int) ^ k; + ∀ d ∈ (b.digits x.natAbs), d = 0 ∨ d = 1 ∨ d = b - 2 ∨ d = b - 1 := by + sorry + +end OeisA243106 diff --git a/FormalConjectures/OEIS/248802.lean b/FormalConjectures/OEIS/248802.lean new file mode 100644 index 0000000000..bc3560ca5f --- /dev/null +++ b/FormalConjectures/OEIS/248802.lean @@ -0,0 +1,94 @@ +/- +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 A248802 + +A248802: Smallest prime factor of $2^{(2^n+2)} + 3$. + +An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67. + +*References:* +- [A248802](https://oeis.org/A248802) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA248802 + + +/-- +A248802: Smallest prime factor of $2^{(2^n+2)} + 3$. +-/ +def a (n : ℕ) : ℕ := (2 ^ (2 ^ n + 2) + 3).minFac + +/-- An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67. -/ +def covered_by_C1 (k : ℕ) : Prop := ∃ m : ℕ, k = 10 * m + 2 + +/-- An index k is covered by Conjecture 2 if k = 36m + 16 for some m >= 0, +and m is not 1 mod 5, predicting a(k)=271. -/ +def covered_by_C2 (k : ℕ) : Prop := ∃ m : ℕ, k = 36 * m + 16 ∧ m % 5 ≠ 1 + +/-- An index k is covered by Conjecture 3 if k = 84m + 22 for some m >= 0, +and m is not 0 mod 5, predicting a(k)=523. -/ +def covered_by_C3 (k : ℕ) : Prop := ∃ m : ℕ, k = 84 * m + 22 ∧ m % 5 ≠ 0 + + +@[category test, AMS 11] +lemma a_zero : a 0 = 11 := by native_decide + +@[category test, AMS 11] +lemma a_one : a 1 = 19 := by native_decide + +@[category test, AMS 11] +lemma a_two : a 2 = 67 := by native_decide + +@[category test, AMS 11] +lemma a_three : a 3 = 13 := by native_decide + +@[category test, AMS 11] +lemma a_four : a 4 = 262147 := by native_decide + + +/-- +A248802: Smallest prime factor of $2^{(2^n+2)} + 3$. + +An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67. + +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/248802.wip.lean#L208"] +theorem a_ten_mul_add_two_eq (n : ℕ) : a (10 * n + 2) = 67 := by + sorry + + +/-- +A248802: Smallest prime factor of $2^{(2^n+2)} + 3$. + +An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67. + +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/248802.wip.lean#L982"] +theorem a_fifty_eight_mul_add_twenty_six_eq (n : ℕ) : + (¬covered_by_C1 (58 * n + 26) ∧ ¬covered_by_C2 (58 * n + 26) ∧ + ¬covered_by_C3 (58 * n + 26)) → a (58 * n + 26) = 1399 := by + sorry + +end OeisA248802 diff --git a/FormalConjectures/OEIS/256012.lean b/FormalConjectures/OEIS/256012.lean new file mode 100644 index 0000000000..37cdd7d9ec --- /dev/null +++ b/FormalConjectures/OEIS/256012.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 a + +a: Number of partitions of $n$ into distinct parts that are not squarefree. +This is the number of finite subsets of positive integers $P$ such that +$\sum_{k \in P} k = n$ and every element $k \in P$ is not squarefree. + +*References:* +- [A256012](https://oeis.org/A256012) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA256012 + + +open Nat Finset + +/-- +a: Number of partitions of $n$ into distinct parts that are not squarefree. +This is the number of finite subsets of positive integers $P$ such that +$\sum_{k \in P} k = n$ and every element $k \in P$ is not squarefree. +-/ +def a (n : ℕ) : ℕ := + -- The parts must be $\le n$ to sum to $n$. + -- This is $\{1, 2, \dots, n\}$ + let potential_parts : Finset ℕ := range (n + 1) \ {0} + + -- We count all subsets P of potential_parts that satisfy the sum and the property. + card <| filter (fun P : Finset ℕ => + P.sum id = n ∧ + (∀ k ∈ P, ¬ Squarefree k) + ) (powerset potential_parts) + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by decide + +@[category test, AMS 11] +lemma a_one : a 1 = 0 := by native_decide + +@[category test, AMS 11] +lemma a_two : a 2 = 0 := by native_decide + +@[category test, AMS 11] +lemma a_three : a 3 = 0 := by native_decide + +@[category test, AMS 11] +lemma a_four : a 4 = 1 := by native_decide + + +/-- +a: Number of partitions of $n$ into distinct parts that are not squarefree. +This is the number of finite subsets of positive integers $P$ such that +$\sum_{k \in P} k = n$ and every element $k \in P$ is not squarefree. + +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/256012.wip.lean#L91"] +theorem a_pos_of_gt (n : ℕ) (hn : n > 23) : a n > 0 := by + sorry + +end OeisA256012 diff --git a/FormalConjectures/OEIS/258667.lean b/FormalConjectures/OEIS/258667.lean new file mode 100644 index 0000000000..cd2b19ba38 --- /dev/null +++ b/FormalConjectures/OEIS/258667.lean @@ -0,0 +1,150 @@ +/- +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 a + +The inner sum of the formula used in a: +$$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$ + +a: A total of $n$ married couples, including a mathematician M and his wife, are to be seated +at the $2n$ chairs around a circular table, with no man seated next to his wife. After the ladies +are seated at every other chair, M is the first man allowed to choose one of the remaining chairs. +The sequence gives the number of ways of seating the other men, with no man seated next to his +wife, if M chooses the chair that is 9 seats clockwise from his wife's chair. + +$$a(n) = \begin{cases} 0 & \text{if } n \le 5 \\ +\sum_{k=0}^{n-1}(-1)^k(n-k-1)! \sum_{\max(k-n+5, 0) \le j \le \min(k,4)} +\binom{8-j}{j}\binom{2n-k+j-10}{k-j} & \text{if } n > 5 \end{cases}$$ + +*References:* +- [A258667](https://oeis.org/A258667) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA258667 + + +open scoped Topology + +open BigOperators Nat Int Real Asymptotics Filter + +/-- +The inner sum of the formula used in a: +$$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$ +-/ +private def A258667_inner_sum (n k : ℕ) : ℤ := + let L : ℕ := max 0 (k + 5 - n) + let U : ℕ := min k 4 + Finset.sum (Finset.Icc L U) fun j => + let term1 := Nat.choose (8 - j) j + -- The top argument of the second binomial coefficient is written in Nat subtraction form. + let term2 := Nat.choose (2 * n + j - (k + 10)) (k - j) + ofNat term1 * ofNat term2 + +/-- +a: A total of $n$ married couples, including a mathematician M and his wife, are to be seated +at the $2n$ chairs around a circular table, with no man seated next to his wife. After the ladies +are seated at every other chair, M is the first man allowed to choose one of the remaining chairs. +The sequence gives the number of ways of seating the other men, with no man seated next to his +wife, if M chooses the chair that is 9 seats clockwise from his wife's chair. + +$$a(n) = \begin{cases} 0 & \text{if } n \le 5 \\ +\sum_{k=0}^{n-1}(-1)^k(n-k-1)! \sum_{\max(k-n+5, 0) \le j \le \min(k,4)} +\binom{8-j}{j}\binom{2n-k+j-10}{k-j} & \text{if } n > 5 \end{cases}$$ +-/ +def a (n : ℕ) : ℕ := + if n ≤ 5 then 0 else + (Finset.sum (Finset.range n) fun k => + let sign : ℤ := if k % 2 = 0 then 1 else -1 + -- Nat.factorial (n - 1 - k) is safe since h implies n > 5 and k < n. + let fac_term : ℤ := ofNat (Nat.factorial (n - 1 - k)) + + sign * fac_term * A258667_inner_sum n k + ).natAbs + +noncomputable def nat_fac_to_real (n : ℕ) : ℝ := (Nat.factorial n : ℝ) + +/-- The denominator term $k! (n-1)_k$ represented as a Real number. -/ +noncomputable def menage_denom_term (n k : ℕ) : ℝ := + let k_fac_R := nat_fac_to_real k + -- (n-1)_k is the falling factorial. Nat.descFactorial (n-1) k is (n-1)!/(n-1-k)! + let falling_fac := (Nat.descFactorial (n - 1) k : ℝ) + k_fac_R * falling_fac + +/-- The infinite series part of the asymptotic expansion: +$\sum_{k \ge 1} \frac{(-1)^k}{k!(n-1)_k}$. -/ +noncomputable def A258667_asymptotic_sum_part (n : ℕ) : ℝ := + -- The sum is effectively finite since (n-1)_k is 0 for k >= n. + Finset.sum (Finset.range n) fun k => + if k = 0 then 0 + else + let denom := menage_denom_term n k + -- Denominator is non-zero if n >= 1 and 1 <= k < n. + if denom = 0 then 0 + else ((-1 : ℝ) ^ k) / denom + +/-- The proposed asymptotic expression for a(n). -/ +noncomputable def A258667_asymptotic_term (n : ℕ) : ℝ := + if n ≤ 2 then 0 -- Avoid division by zero, irrelevant for n -> infinity + else + let n_R : ℝ := n + let n_fac_R := nat_fac_to_real n + let prefactor : ℝ := exp (-2) * (n_fac_R / (n_R - 2)) + prefactor * (1 + A258667_asymptotic_sum_part n) + + +@[category test, AMS 11] +lemma a_one : a 1 = 0 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 0 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 0 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 0 := by rfl + +@[category test, AMS 11] +lemma a_five : a 5 = 0 := by rfl + + +/-- +The inner sum of the formula used in a: +$$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$ + +a: A total of $n$ married couples, including a mathematician M and his wife, are to be seated +at the $2n$ chairs around a circular table, with no man seated next to his wife. After the ladies +are seated at every other chair, M is the first man allowed to choose one of the remaining chairs. +The sequence gives the number of ways of seating the other men, with no man seated next to his +wife, if M chooses the chair that is 9 seats clockwise from his wife's chair. + +$$a(n) = \begin{cases} 0 & \text{if } n \le 5 \\ +\sum_{k=0}^{n-1}(-1)^k(n-k-1)! \sum_{\max(k-n+5, 0) \le j \le \min(k,4)} +\binom{8-j}{j}\binom{2n-k+j-10}{k-j} & \text{if } n > 5 \end{cases}$$ + +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/258667.wip.lean#L427"] +theorem a_is_equivalent_asymptotic_term : + IsEquivalent atTop (fun n : ℕ => (a n : ℝ)) A258667_asymptotic_term := by + sorry + +end OeisA258667 diff --git a/FormalConjectures/OEIS/267581.lean b/FormalConjectures/OEIS/267581.lean new file mode 100644 index 0000000000..29e4ca52c5 --- /dev/null +++ b/FormalConjectures/OEIS/267581.lean @@ -0,0 +1,110 @@ +/- +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 A267581 + +The rule function for Rule 167. Inputs must be 0 or 1. + +The state of the Rule 167 elementary cellular automaton at time $t$ and position $x$. +The initial condition is a single ON cell at $x=0$. +$C(t, x)$ is structurally recursive on $t$. + +*References:* +- [A267581](https://oeis.org/A267581) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA267581 + + +open Nat Int + +/-- The rule function for Rule 167. Inputs must be 0 or 1. -/ +def ca_rule_167 (c_L c_C c_R : ℕ) : ℕ := + let R : ℕ := 167 + let index : ℕ := 4 * c_L + 2 * c_C + c_R + -- Rule 167 is determined by the index-th bit of R. + (R / (2 ^ index)) % 2 + +/-- +The state of the Rule 167 elementary cellular automaton at time $t$ and position $x$. +The initial condition is a single ON cell at $x=0$. +$C(t, x)$ is structurally recursive on $t$. +-/ +def ca_state (t : ℕ) (x : ℤ) : ℕ := + match t with + | 0 => if x = 0 then 1 else 0 + | t' + 1 => + let C_t' (y : ℤ) := ca_state t' y + ca_rule_167 (C_t' (x - 1)) (C_t' x) (C_t' (x + 1)) + +/-- The sequence of bits forming the middle column of the CA pattern, $C_{t, 0}$. -/ +def middle_column_bit (t : ℕ) : ℕ := ca_state t 0 + +/-- +A267581: Decimal representation of the middle column of the "Rule 167" elementary cellular automaton +starting with a single ON (black) cell. +The term $a(n)$ is the decimal value of the binary number $C_{0, 0} C_{1, 0} \dots C_{n, 0}$, +where $C_{i, 0}$ is the state of the center cell at time $i$. +$$a(n) = \sum_{k=0}^n C_{k, 0} \cdot 2^{n-k}$$ +-/ +noncomputable def a (n : ℕ) : ℕ := + Finset.sum (Finset.range (n + 1)) fun k => (middle_column_bit k) * (2^ (n - k)) + +/-- The floor term in the conjectured recurrence relation for A267581. +This term, $\lfloor (1/2)^{(2^{n+1} \bmod n)} \rfloor$, simplifies to 1 if $(2^{n+1} \bmod n) = 0$ +(i.e., $n \mid 2^{n+1}$), and 0 otherwise. +Since the recurrence is only stated for $n \ge 2$, the $n=0$ case is irrelevant +to the conjecture. -/ +def oeis_floor_term (n : ℕ) : ℕ := + if n = 0 then 0 + else if (2 ^ (n + 1)) % n = 0 then 1 else 0 + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 3 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 6 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 13 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 26 := by rfl + + +/-- +The rule function for Rule 167. Inputs must be 0 or 1. + +The state of the Rule 167 elementary cellular automaton at time $t$ and position $x$. +The initial condition is a single ON cell at $x=0$. +$C(t, x)$ is structurally recursive on $t$. + +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/267581.wip.lean#L190"] +theorem a_recurrence (n : ℕ) (hn : 2 ≤ n) : a n = 2 * a (n - 1) + 1 - oeis_floor_term n := by + sorry + +end OeisA267581 diff --git a/FormalConjectures/OEIS/271591.lean b/FormalConjectures/OEIS/271591.lean new file mode 100644 index 0000000000..f8a4149837 --- /dev/null +++ b/FormalConjectures/OEIS/271591.lean @@ -0,0 +1,104 @@ +/- +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 A271591 + +The Tribonacci numbers $T_n$ (A000073). +$T_0=0, T_1=0, T_2=1$, and $T_n = T_{n-1} + T_{n-2} + T_{n-3}$ for $n \ge 3$. + +A271591: Second most significant bit of the tribonacci number A000073(n). +This is formalized by extracting the bit at position $\lfloor \log_2 T_n \rfloor - 1$. + +*References:* +- [A271591](https://oeis.org/A271591) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +- [A000073](https://oeis.org/A000073) +-/ + +namespace OeisA271591 + + +open Nat + +/-- +The Tribonacci numbers $T_n$ (A000073). +$T_0=0, T_1=0, T_2=1$, and $T_n = T_{n-1} + T_{n-2} + T_{n-3}$ for $n \ge 3$. +-/ +def tribonacci (n : ℕ) : ℕ := + match n with + | 0 => 0 + | 1 => 0 + | 2 => 1 + | n + 3 => (tribonacci (n + 2)) + (tribonacci (n + 1)) + (tribonacci n) + +/-- +A271591: Second most significant bit of the tribonacci number A000073(n). +This is formalized by extracting the bit at position $\lfloor \log_2 T_n \rfloor - 1$. +-/ +def a (n : ℕ) : ℕ := + let T := tribonacci n + -- The index of the MSB is T.log2. The index of the second MSB is T.log2 - 1. + if T ≤ 1 then + 0 + else + let j_smsb : ℕ := T.log2 - 1 + if T.testBit j_smsb then 1 else 0 + +def is_maximal_run (v : ℕ) (n L : ℕ) : Prop := + n ≥ 2 ∧ L ≥ 1 ∧ + -- The run consists of L consecutive $v$'s starting at n + (∀ i : ℕ, i < L → a (n + i) = v) ∧ + -- The run is not followed by $v$ + (a (n + L) ≠ v) ∧ + -- The run is not preceded by $v$ + (a (n - 1) ≠ v) + + +@[category test, AMS 11] +lemma a_four : a 4 = 0 := by rfl + +@[category test, AMS 11] +lemma a_five : a 5 = 0 := by rfl + +@[category test, AMS 11] +lemma a_six : a 6 = 1 := by rfl + +@[category test, AMS 11] +lemma a_seven : a 7 = 1 := by rfl + +@[category test, AMS 11] +lemma a_eight : a 8 = 1 := by rfl + + +/-- +The Tribonacci numbers $T_n$ (A000073). +$T_0=0, T_1=0, T_2=1$, and $T_n = T_{n-1} + T_{n-2} + T_{n-3}$ for $n \ge 3$. + +A271591: Second most significant bit of the tribonacci number A000073(n). +This is formalized by extracting the bit at position $\lfloor \log_2 T_n \rfloor - 1$. + +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/271591.wip.lean#L497"] +theorem maximal_run_lengths : (∀ n L, is_maximal_run 0 n L → (L = 4 ∨ L = 5)) ∧ + (∀ n L, is_maximal_run 1 n L → (L = 3 ∨ L = 4)) := by + sorry + +end OeisA271591 diff --git a/FormalConjectures/OEIS/278070.lean b/FormalConjectures/OEIS/278070.lean new file mode 100644 index 0000000000..92be93de71 --- /dev/null +++ b/FormalConjectures/OEIS/278070.lean @@ -0,0 +1,80 @@ +/- +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 a + +a: $a(n) = \text{hypergeometric}([n, -n], [], -1)$. +This is equivalent to the combinatorial sum: +$$a(n) = \sum_{k=0}^n \binom{n}{k} \binom{n+k-1}{k} k!$$ +The expression uses $\mathbb{N}$ arithmetic throughout, safely handling +the subtraction via `Nat.pred`. + +*References:* +- [A278070](https://oeis.org/A278070) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA278070 + + +open Nat Finset + +/-- +a: $a(n) = \text{hypergeometric}([n, -n], [], -1)$. +This is equivalent to the combinatorial sum: +$$a(n) = \sum_{k=0}^n \binom{n}{k} \binom{n+k-1}{k} k!$$ +The expression uses $\mathbb{N}$ arithmetic throughout, safely handling +the subtraction via `Nat.pred`. +-/ +def a (n : ℕ) : ℕ := + (Finset.range (n + 1)).sum fun k => + (n.choose k) * ((n + k).pred.choose k) * (k.factorial) + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 2 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 11 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 106 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 1457 := by rfl + + +/-- +a: $a(n) = \text{hypergeometric}([n, -n], [], -1)$. +This is equivalent to the combinatorial sum: +$$a(n) = \sum_{k=0}^n \binom{n}{k} \binom{n+k-1}{k} k!$$ +The expression uses $\mathbb{N}$ arithmetic throughout, safely handling +the subtraction via `Nat.pred`. + +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/278070.wip.lean#L68"] +theorem a_modeq : ∀ (n k : ℕ), Nat.ModEq k (a (n + k)) (a n) := by + sorry + +end OeisA278070 diff --git a/FormalConjectures/OEIS/282779.lean b/FormalConjectures/OEIS/282779.lean new file mode 100644 index 0000000000..ffbfe6c3d4 --- /dev/null +++ b/FormalConjectures/OEIS/282779.lean @@ -0,0 +1,93 @@ +/- +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 a + +a: Period of cubes mod $n$. +The $n$-th term $a(n)$ is the smallest positive integer $T$ such that +$\forall k \in \mathbb{N}$, $(k+T)^3 \equiv k^3 \pmod n$. + +The length of the minimal positive period of the sequence $k^p \pmod n$. +$a_p(n) = \min \{ T \in \mathbb{N}^+ \mid \forall k \in \mathbb{N}, (k+T)^p \equiv k^p \pmod n \}$. + +*References:* +- [A282779](https://oeis.org/A282779) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA282779 + + +open Nat Set Classical + +/-- +a: Period of cubes mod $n$. +The $n$-th term $a(n)$ is the smallest positive integer $T$ such that +$\forall k \in \mathbb{N}$, $(k+T)^3 \equiv k^3 \pmod n$. +-/ +noncomputable def a (n : ℕ) : ℕ := + if n = 0 then 0 -- Handle the non-sequence index n=0 + else + -- sInf computes the infimum of the set, which is the minimum since ℕ is well-ordered. + sInf { T : ℕ | 0 < T ∧ ∀ k : ℕ, (k + T) ^ 3 % n = k ^ 3 % n } + +/-- +The length of the minimal positive period of the sequence $k^p \pmod n$. +$a_p(n) = \min \{ T \in \mathbb{N}^+ \mid \forall k \in \mathbb{N}, (k+T)^p \equiv k^p \pmod n \}$. +-/ +noncomputable def period_of_power_mod (p n : ℕ) : ℕ := + if n = 0 then 0 + else + sInf { T : ℕ | 0 < T ∧ ∀ k : ℕ, (k + T) ^ p % n = k ^ p % n } + + + +/-- +a: Period of cubes mod $n$. +The $n$-th term $a(n)$ is the smallest positive integer $T$ such that +$\forall k \in \mathbb{N}$, $(k+T)^3 \equiv k^3 \pmod n$. + +The length of the minimal positive period of the sequence $k^p \pmod n$. +$a_p(n) = \min \{ T \in \mathbb{N}^+ \mid \forall k \in \mathbb{N}, (k+T)^p \equiv k^p \pmod n \}$. + +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/282779.wip.lean#L104"] +theorem period_of_power_mod_eq (p n : ℕ) (hp : Nat.Prime p) (hn : n > 0) : + period_of_power_mod p n = if p ^ 2 ∣ n then n / p else n := by + sorry + + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by exact period_of_power_mod_eq 3 1 (by decide) (by decide) + +@[category test, AMS 11] +lemma a_two : a 2 = 2 := by exact period_of_power_mod_eq 3 2 (by decide) (by decide) + +@[category test, AMS 11] +lemma a_three : a 3 = 3 := by exact period_of_power_mod_eq 3 3 (by decide) (by decide) + +@[category test, AMS 11] +lemma a_four : a 4 = 4 := by exact period_of_power_mod_eq 3 4 (by decide) (by decide) + +@[category test, AMS 11] +lemma a_five : a 5 = 5 := by exact period_of_power_mod_eq 3 5 (by decide) (by decide) + +end OeisA282779 diff --git a/FormalConjectures/OEIS/28859.lean b/FormalConjectures/OEIS/28859.lean new file mode 100644 index 0000000000..0daa834200 --- /dev/null +++ b/FormalConjectures/OEIS/28859.lean @@ -0,0 +1,75 @@ +/- +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 A28859 + +A028859 (OEIS): $a(n+2) = 2 \cdot a(n+1) + 2 \cdot a(n)$; $a(0) = 1$, $a(1) = 3$. + +*References:* +- [A28859](https://oeis.org/A28859) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA28859 + + +/-- +A028859 (OEIS): $a(n+2) = 2 \cdot a(n+1) + 2 \cdot a(n)$; $a(0) = 1$, $a(1) = 3$. +-/ +def a (n : ℕ) : ℕ := + match n with + | 0 => 1 + | 1 => 3 + | (n + 2) => 2 * a (n + 1) + 2 * a n +termination_by n + +set_option linter.unusedVariables false + + +@[category test, AMS 11] +lemma a_two : a 2 = 8 := by native_decide + +@[category test, AMS 11] +lemma a_three : a 3 = 22 := by native_decide + +@[category test, AMS 11] +lemma a_four : a 4 = 60 := by native_decide + + +/-- +A028859 (OEIS): $a(n+2) = 2 \cdot a(n+1) + 2 \cdot a(n)$; $a(0) = 1$, $a(1) = 3$. + +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/28859.wip.lean#L402"] +theorem exists_finset_sequence (n : ℕ) : + let L := n + 1 + let Sequence := Fin L → ℕ + let S : Set Sequence := + {σ : Sequence | + L > 0 ∧ + (∀ i : Fin L, σ i > 0) ∧ + let max_val := Finset.sup Finset.univ σ + (∀ k : ℕ, 1 ≤ k ∧ k ≤ max_val → ∃ i : Fin L, σ i = k) ∧ + (∀ i j : Fin L, i < j → j.val ≠ i.val + 1 → σ i ≥ σ j)} + ∃ (F : Finset Sequence), (F : Set Sequence) = S ∧ F.card = a n := by + sorry + +end OeisA28859 diff --git a/FormalConjectures/OEIS/289411.lean b/FormalConjectures/OEIS/289411.lean new file mode 100644 index 0000000000..511801cfc8 --- /dev/null +++ b/FormalConjectures/OEIS/289411.lean @@ -0,0 +1,80 @@ +/- +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 a + +a: $\mathrm{a}(n) = \sum_{k=0}^n \mathrm{sign}(\mathrm{A007953}(5k) - \mathrm{A007953}(k))$. +$\mathrm{A007953}(n)$ is the digital sum of $n$ in base 10. +The sequence is non-negative, so the sum over $\mathbb{Z}$ is converted to $\mathbb{N}$. + +*References:* +- [A289411](https://oeis.org/A289411) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +- [A007953](https://oeis.org/A007953) +-/ + +namespace OeisA289411 + + +open Nat + +/-- +a: $\mathrm{a}(n) = \sum_{k=0}^n \mathrm{sign}(\mathrm{A007953}(5k) - \mathrm{A007953}(k))$. +$\mathrm{A007953}(n)$ is the digital sum of $n$ in base 10. +The sequence is non-negative, so the sum over $\mathbb{Z}$ is converted to $\mathbb{N}$. +-/ +def a (n : ℕ) : ℕ := + let digital_sum_ten (m : ℕ) : ℕ := (Nat.digits 10 m).sum + (Finset.range (n + 1)).sum (fun k => + Int.sign ((digital_sum_ten (5 * k) : ℤ) - (digital_sum_ten k : ℤ))) + |>.toNat + + + +@[category test, AMS 11] +lemma a_zero : a 0 = 0 := by native_decide + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by native_decide + +@[category test, AMS 11] +lemma a_two : a 2 = 0 := by native_decide + +@[category test, AMS 11] +lemma a_three : a 3 = 1 := by native_decide + +@[category test, AMS 11] +lemma a_four : a 4 = 0 := by native_decide + + +/-- +a: $\mathrm{a}(n) = \sum_{k=0}^n \mathrm{sign}(\mathrm{A007953}(5k) - \mathrm{A007953}(k))$. +$\mathrm{A007953}(n)$ is the digital sum of $n$ in base 10. +The sequence is non-negative, so the sum over $\mathbb{Z}$ is converted to $\mathbb{N}$. + +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/289411.wip.lean#L167"] +theorem a_symm (k : ℕ) (hk : 0 < k) : + let m_k : ℕ := (10 ^ k) / 2 - 1 + ∀ i : ℕ, i ≤ m_k → a (m_k - i) = a (m_k + i) := by + sorry + +end OeisA289411 diff --git a/FormalConjectures/OEIS/2897.lean b/FormalConjectures/OEIS/2897.lean new file mode 100644 index 0000000000..a35caf0b13 --- /dev/null +++ b/FormalConjectures/OEIS/2897.lean @@ -0,0 +1,105 @@ +/- +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 A2897 + +The sequence $a(n)$ is defined by $a(n) = \binom{2n}{n}^3$. +We use `Nat.choose (2 * n) n` for the central binomial coefficient. + +The finsupp corresponding to the monomial $x^n y^n z^n$. +This is the map $\lambda i. n$. Since `Fin 3` is finite, this function is finitely supported. +We mark it noncomputable as it builds a mathematical object defined in terms of finite support. + +*References:* +- [A2897](https://oeis.org/A2897) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA2897 + + +open Polynomial + +open Nat MvPolynomial + +/-- +The sequence $a(n)$ is defined by $a(n) = \binom{2n}{n}^3$. +We use `Nat.choose (2 * n) n` for the central binomial coefficient. +-/ +def a (n : ℕ) : ℕ := (Nat.choose (2 * n) n) ^ 3 + +abbrev Vars := Fin 3 + +/-- +The finsupp corresponding to the monomial $x^n y^n z^n$. +This is the map $\lambda i. n$. Since `Fin 3` is finite, this function is finitely supported. +We mark it noncomputable as it builds a mathematical object defined in terms of finite support. +-/ +noncomputable def xyz_pow_n (n : ℕ) : Finsupp Vars ℕ := + Finsupp.ofSupportFinite (fun _ : Vars => n) (Set.toFinite _) + +local notation "P" => MvPolynomial Vars ℤ + +/-- +The polynomial $P_n(X, Y, Z) = (1 + X + Y + Z)^{2n} (1 + X + Y - Z)^n (1 + X - Y + Z)^n$. +We identify $X_0, X_1, X_2$ with $X, Y, Z$. +We mark it noncomputable due to dependencies in the polynomial ring structure. +-/ +noncomputable def P_n (n : ℕ) : P := + let X := MvPolynomial.X 0 + let Y := MvPolynomial.X 1 + let Z := MvPolynomial.X 2 + let p1 : P := 1 + X + Y + Z + let p2 : P := 1 + X + Y - Z + let p3 : P := 1 + X - Y + Z + p1 ^ (2 * n) * p2 ^ n * p3 ^ n + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 8 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 216 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 8000 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 343000 := by rfl + + +/-- +The sequence $a(n)$ is defined by $a(n) = \binom{2n}{n}^3$. +We use `Nat.choose (2 * n) n` for the central binomial coefficient. + +The finsupp corresponding to the monomial $x^n y^n z^n$. +This is the map $\lambda i. n$. Since `Fin 3` is finite, this function is finitely supported. +We mark it noncomputable as it builds a mathematical object defined in terms of finite support. + +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/2897.wip.lean#L408"] +theorem a_eq_coeff (n : ℕ) : (a n : ℤ) = MvPolynomial.coeff (xyz_pow_n n) (P_n n) := by + sorry + +end OeisA2897 diff --git a/FormalConjectures/OEIS/300997.lean b/FormalConjectures/OEIS/300997.lean new file mode 100644 index 0000000000..c9517ea5d0 --- /dev/null +++ b/FormalConjectures/OEIS/300997.lean @@ -0,0 +1,103 @@ +/- +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 A300997 + +A300997: $a(n)$ is the number of steps needed to reach a stable configuration in the 1D cellular +automaton initialized with one cell with mass $n$ and based on the rule "each cell gives half of +its mass, rounded down, to its right neighbor". +The stable configuration is $n$ cells with mass 1. + +*References:* +- [A300997](https://oeis.org/A300997) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA300997 + + +open List Nat Function Set + +/-- +A300997: $a(n)$ is the number of steps needed to reach a stable configuration in the 1D cellular +automaton initialized with one cell with mass $n$ and based on the rule "each cell gives half of +its mass, rounded down, to its right neighbor". +The stable configuration is $n$ cells with mass 1. +-/ +noncomputable def a (n : ℕ) : ℕ := + let half_ceil (m : ℕ) : ℕ := (m + 1) / 2 + let half_floor (m : ℕ) : ℕ := m / 2 + + let trim_trailing_zeros (l : List ℕ) : List ℕ := + (List.reverse l).dropWhile (fun x => x = 0) |>.reverse + + let ca_step (config : List ℕ) : List ℕ := + let base_masses := config.map half_ceil ++ [0] + let received_masses := 0 :: config.map half_floor + + let next_config_long := List.zipWith Nat.add base_masses received_masses + + trim_trailing_zeros next_config_long + + if n = 0 then + 0 + else + let initial_config : List ℕ := [n] + let target_config : List ℕ := List.replicate n 1 + + -- State after t steps, computed by folding ca_step t times using foldl over a range. + let S (t : ℕ) : List ℕ := (List.range t).foldl (fun acc _ => ca_step acc) initial_config + + -- The set of time steps k at which the configuration is stable. + let stable_steps : Set ℕ := {k | S k = target_config} + + -- a(n) is the smallest k in this set, defined by the set infimum (sInf). + sInf stable_steps + + +@[category test, AMS 11] +lemma a_one : a 1 = 0 := by sorry + +@[category test, AMS 11] +lemma a_two : a 2 = 1 := by sorry + +@[category test, AMS 11] +lemma a_three : a 3 = 3 := by sorry + +@[category test, AMS 11] +lemma a_four : a 4 = 4 := by sorry + +@[category test, AMS 11] +lemma a_five : a 5 = 6 := by sorry + + +/-- +A300997: $a(n)$ is the number of steps needed to reach a stable configuration in the 1D cellular +automaton initialized with one cell with mass $n$ and based on the rule "each cell gives half of +its mass, rounded down, to its right neighbor". +The stable configuration is $n$ cells with mass 1. + +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/300997.wip.lean#L1153"] +theorem a_succ_eq : ∀ n : ℕ, 1 ≤ n → a (n + 1) = a n + 1 ∨ a (n + 1) = a n + 2 := by + sorry + +end OeisA300997 diff --git a/FormalConjectures/OEIS/306424.lean b/FormalConjectures/OEIS/306424.lean new file mode 100644 index 0000000000..b72c9b17be --- /dev/null +++ b/FormalConjectures/OEIS/306424.lean @@ -0,0 +1,83 @@ +/- +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 A306424 + +A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each +$b = 3..k-1$ never contains more than two distinct digits. + +The sequence A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each +$b = 3..k-1$ never contains more than two distinct digits. + +*References:* +- [A306424](https://oeis.org/A306424) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA306424 + + +open List Finset Nat + +/-- +A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each +$b = 3..k-1$ never contains more than two distinct digits. +-/ +def A306424_condition (k : ℕ) : Prop := + -- The bases $b$ range over $3 \le b \le k-1$, expressed as $3 \le b$ and $b < k$. + ∀ b : ℕ, 3 ≤ b ∧ b < k → ((Nat.digits b k).toFinset.card) ≤ 2 + +/-- +The sequence A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each +$b = 3..k-1$ never contains more than two distinct digits. +-/ +noncomputable def a (n : ℕ) : ℕ := n.nth A306424_condition + + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by sorry + +@[category test, AMS 11] +lemma a_two : a 2 = 2 := by sorry + +@[category test, AMS 11] +lemma a_three : a 3 = 3 := by sorry + +@[category test, AMS 11] +lemma a_four : a 4 = 4 := by sorry + +@[category test, AMS 11] +lemma a_five : a 5 = 5 := by sorry + + +/-- +A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each +$b = 3..k-1$ never contains more than two distinct digits. + +The sequence A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each +$b = 3..k-1$ never contains more than two distinct digits. + +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/306424.wip.lean#L276"] +theorem forty_three_is_max : A306424_condition 43 ∧ ∀ k : ℕ, 43 < k → ¬A306424_condition k := by + sorry + +end OeisA306424 diff --git a/FormalConjectures/OEIS/307865.lean b/FormalConjectures/OEIS/307865.lean new file mode 100644 index 0000000000..1558cdf41c --- /dev/null +++ b/FormalConjectures/OEIS/307865.lean @@ -0,0 +1,91 @@ +/- +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 A307865 + +A307865: $a(n)$ is the number of natural bases $b < 2n+1$ such that $b^n \equiv -1 \pmod{2n+1}$. +The bases $b$ are interpreted as $b \in \{1, 2, \dots, 2n\}$. +We check the condition in the ring $\mathbb{Z}/(2n+1)\mathbb{Z}$. + +A natural number $m > 1$ is an absolute Euler pseudoprime if it is composite and +for all $b$ coprime to $m$, $b^{(m-1)/2} \equiv \pm 1 \pmod m$. + +*References:* +- [A307865](https://oeis.org/A307865) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA307865 + + +open Nat Finset ZMod + +/-- +A307865: $a(n)$ is the number of natural bases $b < 2n+1$ such that $b^n \equiv -1 \pmod{2n+1}$. +The bases $b$ are interpreted as $b \in \{1, 2, \dots, 2n\}$. +We check the condition in the ring $\mathbb{Z}/(2n+1)\mathbb{Z}$. +-/ +def a (n : ℕ) : ℕ := + let m : ℕ := 2 * n + 1 + -- The set of bases is $\{1, 2, \dots, 2n\} = \text{Ico } 1 m$. + (Ico 1 m).filter (fun b : ℕ => (b : ZMod m) ^ n = (-1 : ZMod m)) |>.card + +variable {n : ℕ} + +/-- +A natural number $m > 1$ is an absolute Euler pseudoprime if it is composite and +for all $b$ coprime to $m$, $b^{(m-1)/2} \equiv \pm 1 \pmod m$. +-/ +def IsAbsoluteEulerPseudoprime (m : ℕ) : Prop := + m > 1 ∧ ¬ Nat.Prime m ∧ + (∀ b : ℕ, Nat.Coprime b m → (b : ZMod m) ^ ((m - 1) / 2) = 1 ∨ (b : ZMod m) ^ ((m - 1) / 2) = -1) + + +@[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 = 2 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 3 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 0 := by rfl + + +/-- +A307865: $a(n)$ is the number of natural bases $b < 2n+1$ such that $b^n \equiv -1 \pmod{2n+1}$. +The bases $b$ are interpreted as $b \in \{1, 2, \dots, 2n\}$. +We check the condition in the ring $\mathbb{Z}/(2n+1)\mathbb{Z}$. + +A natural number $m > 1$ is an absolute Euler pseudoprime if it is composite and +for all $b$ coprime to $m$, $b^{(m-1)/2} \equiv \pm 1 \pmod m$. + +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/307865.wip.lean#L190"] +theorem a_eq_zero_of_pseudoprime (h : IsAbsoluteEulerPseudoprime (2 * n + 1)) : a n = 0 := by + sorry + +end OeisA307865 diff --git a/FormalConjectures/OEIS/309132.lean b/FormalConjectures/OEIS/309132.lean new file mode 100644 index 0000000000..a95cc2a03e --- /dev/null +++ b/FormalConjectures/OEIS/309132.lean @@ -0,0 +1,89 @@ +/- +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 A309132 + +A309132: a(n) is the denominator of F(n) = A027641(n-1)/n + A027642(n-1)/n^2. + +Definition of a Carmichael number $n$: a composite number s.t. +$b^{n-1} \equiv 1 \pmod n$ for all $b$ coprime to $n$. + +*References:* +- [A309132](https://oeis.org/A309132) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +- [A027641](https://oeis.org/A027641) +- [A027642](https://oeis.org/A027642) +-/ + +namespace OeisA309132 + + +open Rat Nat + +/-- +A309132: a(n) is the denominator of F(n) = A027641(n-1)/n + A027642(n-1)/n^2. +-/ +noncomputable def a (n : ℕ) : ℕ := + if n = 0 then 0 + else + let n_q : ℚ := n + let B_nm1 : ℚ := bernoulli (n - 1) + let F_n : ℚ := (B_nm1.num : ℚ) / n_q + (B_nm1.den : ℚ) / (n_q * n_q) + F_n.den + +/-- Definition of a Carmichael number $n$: a composite number s.t. +$b^{n-1} \equiv 1 \pmod n$ for all $b$ coprime to $n$. -/ +def is_carmichael_number (n : ℕ) : Prop := + (¬ Nat.Prime n ∧ n > 1) ∧ (∀ b : ℕ, Nat.gcd b n = 1 → b ^ (n - 1) ≡ 1 [MOD n]) + +/-- Helper definition for "composite number" -/ +def is_composite (n : ℕ) : Prop := ¬ Nat.Prime n ∧ n > 1 + + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by delta a; norm_num [bernoulli] + +@[category test, AMS 11] +lemma a_two : a 2 = 1 := by delta a; norm_num [bernoulli] + +@[category test, AMS 11] +lemma a_three : a 3 = 1 := by delta a; norm_num [bernoulli] + +@[category test, AMS 11] +lemma a_four : a 4 = 16 := by delta a; norm_num [bernoulli] + +@[category test, AMS 11] +lemma a_five : a 5 = 1 := by delta a; norm_num [bernoulli] + + +/-- +A309132: a(n) is the denominator of F(n) = A027641(n-1)/n + A027642(n-1)/n^2. + +Definition of a Carmichael number $n$: a composite number s.t. +$b^{n-1} \equiv 1 \pmod n$ for all $b$ coprime to $n$. + +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/309132.wip.lean#L353"] +theorem carmichael_iff_squarefree_a : + ∀ (n : ℕ), (is_composite n ∧ Squarefree (a n)) ↔ is_carmichael_number n := by + sorry + +end OeisA309132 diff --git a/FormalConjectures/OEIS/323557.lean b/FormalConjectures/OEIS/323557.lean new file mode 100644 index 0000000000..2e323bb5d0 --- /dev/null +++ b/FormalConjectures/OEIS/323557.lean @@ -0,0 +1,92 @@ +/- +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 A323557 + +A323557: G.f.: $\sum_{n\ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 + x^{n+1})^{n+1}}$. +The $m$-th term $a(m)$ is the coefficient of $x^m$, which is explicitly given by the sum: +$$ a(m) = \sum_{n=0}^m \sum_{k=0}^n \binom{n}{k} (-1)^j \binom{n+j}{j},$$ +where $j = \frac{m - n(k+1)}{n+1}$, and the term is zero unless $j$ is a natural number. + +*References:* +- [A323557](https://oeis.org/A323557) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA323557 + + +open scoped Classical + +open Nat + +/-- +A323557: G.f.: $\sum_{n\ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 + x^{n+1})^{n+1}}$. +The $m$-th term $a(m)$ is the coefficient of $x^m$, which is explicitly given by the sum: +$$ a(m) = \sum_{n=0}^m \sum_{k=0}^n \binom{n}{k} (-1)^j \binom{n+j}{j},$$ +where $j = \frac{m - n(k+1)}{n+1}$, and the term is zero unless $j$ is a natural number. +-/ +def a (m : ℕ) : ℤ := + Finset.sum (Finset.range (m + 1)) fun n => + Finset.sum (Finset.range (n + 1)) fun k => + let exp_x_num := n * (k + 1) + if exp_x_num ≤ m then + let remainder := m - exp_x_num + if (n + 1) ∣ remainder then + let j : ℕ := remainder / (n + 1) + let c₁ : ℤ := (n.choose k) + let c₂ : ℤ := (choose (n + j) j) + let sign : ℤ := if Even j then 1 else -1 + sign * c₁ * c₂ + else + 0 + else + 0 + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 0 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 3 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = -2 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 2 := by rfl + + +/-- +A323557: G.f.: $\sum_{n\ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 + x^{n+1})^{n+1}}$. +The $m$-th term $a(m)$ is the coefficient of $x^m$, which is explicitly given by the sum: +$$ a(m) = \sum_{n=0}^m \sum_{k=0}^n \binom{n}{k} (-1)^j \binom{n+j}{j},$$ +where $j = \frac{m - n(k+1)}{n+1}$, and the term is zero unless $j$ is a natural number. + +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/323557.wip.lean#L193"] +theorem odd_a_implies_pronic (m : ℕ) : Odd (a m) → ∃ n : ℕ, m = n * (n + 1) := by + sorry + +end OeisA323557 diff --git a/FormalConjectures/OEIS/325046.lean b/FormalConjectures/OEIS/325046.lean new file mode 100644 index 0000000000..99a087fcf9 --- /dev/null +++ b/FormalConjectures/OEIS/325046.lean @@ -0,0 +1,99 @@ +/- +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 A325046 + +A325046: G.f.: $\sum_{n \ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 - x^{n+1})^{n+1}}$. + +The term $a(N)$ is the coefficient of $x^N$ in the generating function. +Expanding the terms, we get a formula for $a(N)$: +$$a(N) = \sum_{n=0}^N \sum_{k=0}^n \mathbf{1}_{n + nk + (n+1)j = N} \binom{n}{k} \binom{n+j}{j}$$ +where $j = \frac{N - n(k+1)}{n+1}$. + +*References:* +- [A325046](https://oeis.org/A325046) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA325046 + + +open Nat + +open Finset + +/-- +A325046: G.f.: $\sum_{n \ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 - x^{n+1})^{n+1}}$. + +The term $a(N)$ is the coefficient of $x^N$ in the generating function. +Expanding the terms, we get a formula for $a(N)$: +$$a(N) = \sum_{n=0}^N \sum_{k=0}^n \mathbf{1}_{n + nk + (n+1)j = N} \binom{n}{k} \binom{n+j}{j}$$ +where $j = \frac{N - n(k+1)}{n+1}$. +-/ +def a (N : ℕ) : ℕ := + -- The outer sum runs over $n$ from $0$ to $N$. + (range (N + 1)).sum (fun n => + -- The inner sum runs over $k$ from $0$ to $n$. + (range (n + 1)).sum (fun k => + let R : ℕ := N - n * (k + 1) + let m : ℕ := n + 1 + -- We require $R = N - n(k+1) \ge 0$ and $m = n+1$ must divide $R$. + if n * (k + 1) ≤ N ∧ R % m = 0 then + -- $j = R / m$. + let j : ℕ := R / m + -- The summand is $\binom{n}{k} \binom{n+j}{j}$. + n.choose k * (n + j).choose j + else + 0 + ) + ) + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 2 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 3 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 4 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 6 := by rfl + + +/-- +A325046: G.f.: $\sum_{n \ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 - x^{n+1})^{n+1}}$. + +The term $a(N)$ is the coefficient of $x^N$ in the generating function. +Expanding the terms, we get a formula for $a(N)$: +$$a(N) = \sum_{n=0}^N \sum_{k=0}^n \mathbf{1}_{n + nk + (n+1)j = N} \binom{n}{k} \binom{n+j}{j}$$ +where $j = \frac{N - n(k+1)}{n+1}$. + +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/325046.wip.lean#L166"] +theorem odd_a_implies_pronic (N : ℕ) : a N % 2 = 1 → ∃ k : ℕ, N = k * (k + 1) := by + sorry + +end OeisA325046 diff --git a/FormalConjectures/OEIS/340737.lean b/FormalConjectures/OEIS/340737.lean new file mode 100644 index 0000000000..290aeae85d --- /dev/null +++ b/FormalConjectures/OEIS/340737.lean @@ -0,0 +1,145 @@ +/- +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 a + +a: Numerators of a sequence of fractions converging to $e$. +$$a(1) = 3, a(2) = 5$$ +For $n > 2$: +$$a(n) = \begin{cases} \left(\frac{n+2}{2}\right) a(n-1) - a(n-2) - +\left(\frac{n-2}{2}\right) a(n-3) +& \text{if } n \text{ is even} \\ 2 a(n-1) + n a(n-2) & \text{if } n \text{ is odd} \end{cases}$$ + +*References:* +- [A340737](https://oeis.org/A340737) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +- [A340738](https://oeis.org/A340738) +-/ + +namespace OeisA340737 + + +open MeasureTheory + +open scoped Real + +open Nat + +/-- +a: Numerators of a sequence of fractions converging to $e$. +$$a(1) = 3, a(2) = 5$$ +For $n > 2$: +$$a(n) = \begin{cases} \left(\frac{n+2}{2}\right) a(n-1) - a(n-2) - +\left(\frac{n-2}{2}\right) a(n-3) +& \text{if } n \text{ is even} \\ 2 a(n-1) + n a(n-2) & \text{if } n \text{ is odd} \end{cases}$$ +-/ +noncomputable def a (n : ℕ) : ℕ := + match n with + | 0 => 0 -- Required for total function, O(1,1) suggests 0 is not relevant. + | 1 => 3 + | 2 => 5 + | n' + 3 => -- n $\ge$ 3 + let n := n' + 3 + + let a_nm1 := a (n - 1) + let a_nm2 := a (n - 2) + let a_nm3 := a (n - 3) + + if n % 2 = 0 then + -- n is even, n $\ge$ 4 + let c1 : ℕ := (n + 2) / 2 + let c2 : ℕ := (n - 2) / 2 + + -- $a(n) = c_1 \cdot a(n-1) - a(n-2) - c_2 \cdot a(n-3)$. + -- We use Int.ofNat for safe subtraction, as the result is known to be positive. + Int.toNat (Int.ofNat c1 * Int.ofNat a_nm1 - Int.ofNat a_nm2 - Int.ofNat c2 * Int.ofNat a_nm3) + else + -- n is odd, n $\ge$ 3 + 2 * a_nm1 + n * a_nm2 +termination_by n + +/-- +A340738: Denominators of a sequence of fractions converging to $e$. +This sequence is defined by the same recurrence relation as a but with +initial values $b(1)=1, b(2)=2$. +$$b(1) = 1, b(2) = 2$$ +For $n > 2$: +$$b(n) = \begin{cases} \left(\frac{n+2}{2}\right) b(n-1) - b(n-2) - +\left(\frac{n-2}{2}\right) b(n-3) +& \text{if } n \text{ is even} \\ 2 b(n-1) + n b(n-2) & \text{if } n \text{ is odd} \end{cases}$$ +-/ +noncomputable def A340738 (n : ℕ) : ℕ := + match n with + | 0 => 0 + | 1 => 1 + | 2 => 2 + | n' + 3 => -- n $\ge$ 3 + let n := n' + 3 + + let b_nm1 := A340738 (n - 1) + let b_nm2 := A340738 (n - 2) + let b_nm3 := A340738 (n - 3) + + if n % 2 = 0 then + -- n is even, n $\ge$ 4 + let c1 : ℕ := (n + 2) / 2 + let c2 : ℕ := (n - 2) / 2 + + -- $b(n) = c_1 \cdot b(n-1) - b(n-2) - c_2 \cdot b(n-3)$. + -- We use Int.ofNat for safe subtraction. + Int.toNat (Int.ofNat c1 * Int.ofNat b_nm1 - Int.ofNat b_nm2 - Int.ofNat c2 * Int.ofNat b_nm3) + else + -- n is odd, n $\ge$ 3 + 2 * b_nm1 + n * b_nm2 +termination_by n + + +@[category test, AMS 11] +lemma a_one : a 1 = 3 := by unfold a; rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 5 := by unfold a; rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 19 := by unfold a; unfold a; unfold a; simp + +@[category test, AMS 11] +lemma a_four : a 4 = 49 := by unfold a; unfold a; unfold a; unfold a; simp + +@[category test, AMS 11] +lemma a_five : a 5 = 193 := by unfold a; unfold a; unfold a; unfold a; unfold a; simp + + +/-- +a: Numerators of a sequence of fractions converging to $e$. +$$a(1) = 3, a(2) = 5$$ +For $n > 2$: +$$a(n) = \begin{cases} \left(\frac{n+2}{2}\right) a(n-1) - a(n-2) - +\left(\frac{n-2}{2}\right) a(n-3) +& \text{if } n \text{ is even} \\ 2 a(n-1) + n a(n-2) & \text{if } n \text{ is odd} \end{cases}$$ + +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/340737.wip.lean#L438"] +theorem tendsto_exp_one : + Filter.Tendsto (fun n : ℕ => (a n : ℝ) / (A340738 n : ℝ)) Filter.atTop (nhds (Real.exp 1)) := by + sorry + +end OeisA340737 diff --git a/FormalConjectures/OEIS/341254.lean b/FormalConjectures/OEIS/341254.lean new file mode 100644 index 0000000000..69a13cf578 --- /dev/null +++ b/FormalConjectures/OEIS/341254.lean @@ -0,0 +1,167 @@ +/- +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 A341254 + +The constant $r = (2 + \sqrt{5})/2$. + +The constant $r^2$. + +*References:* +- [A341254](https://oeis.org/A341254) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA341254 + + +open Real + +/-- The constant $r = (2 + \sqrt{5})/2$. -/ +noncomputable def r_const : ℝ := (2 + sqrt 5) / 2 + +/-- The constant $r^2$. -/ +noncomputable def r_sq : ℝ := r_const * r_const + +/-- +A341254: $a(n) = \lfloor r \cdot \lfloor r \cdot n \rfloor \rfloor$, where $r = (2 + \sqrt{5})/2$. +Note: The original OEIS definition has $n$ starting at 1. We define $a(n)$ for all $\mathbb{N}$. +-/ +noncomputable def a (n : ℕ) : ℕ := + let r := r_const + let inner_floor : ℤ := Int.floor (r * n) + (Int.floor (r * inner_floor.cast)).toNat + + +@[category test, AMS 11] +lemma a_one : a 1 = 4 := by + unfold a r_const + dsimp only + push_cast + rw [mul_one] + have h1 : ⌊(2 + Real.sqrt 5) / 2⌋ = 2 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h1] + push_cast + have h2 : ⌊(2 + Real.sqrt 5) / 2 * 2⌋ = 4 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h2] + rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 8 := by + unfold a r_const + dsimp only + push_cast + have h1 : ⌊(2 + Real.sqrt 5) / 2 * 2⌋ = 4 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h1] + push_cast + have h2 : ⌊(2 + Real.sqrt 5) / 2 * 4⌋ = 8 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h2] + rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 12 := by + unfold a r_const + dsimp only + push_cast + have h1 : ⌊(2 + Real.sqrt 5) / 2 * 3⌋ = 6 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h1] + push_cast + have h2 : ⌊(2 + Real.sqrt 5) / 2 * 6⌋ = 12 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h2] + rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 16 := by + unfold a r_const + dsimp only + push_cast + have h1 : ⌊(2 + Real.sqrt 5) / 2 * 4⌋ = 8 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h1] + push_cast + have h2 : ⌊(2 + Real.sqrt 5) / 2 * 8⌋ = 16 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h2] + rfl + +@[category test, AMS 11] +lemma a_five : a 5 = 21 := by + unfold a r_const + dsimp only + push_cast + have h1 : ⌊(2 + Real.sqrt 5) / 2 * 5⌋ = 10 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h1] + push_cast + have h2 : ⌊(2 + Real.sqrt 5) / 2 * 10⌋ = 21 := by + rw [Int.floor_eq_iff] + have h5 : 2236 / 1000 < Real.sqrt 5 ∧ Real.sqrt 5 < 2237 / 1000 := by + norm_num [Real.sqrt_lt, Real.lt_sqrt] + constructor <;> linarith + rw [h2] + rfl + + +/-- +The constant $r = (2 + \sqrt{5})/2$. + +The constant $r^2$. + +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/341254.wip.lean#L188"] +theorem a_bounds (n : ℕ) (hn : 1 ≤ n) : (1 / 4 : ℝ) < (n : ℝ) * r_sq - (a n : ℝ) ∧ + (n : ℝ) * r_sq - (a n : ℝ) < 3 := by + sorry + +end OeisA341254 diff --git a/FormalConjectures/OEIS/363102.lean b/FormalConjectures/OEIS/363102.lean new file mode 100644 index 0000000000..46c02b69d9 --- /dev/null +++ b/FormalConjectures/OEIS/363102.lean @@ -0,0 +1,96 @@ +/- +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 A363102 + +Auxiliary sequence A051403, defined as +$$\frac{(n+2) \sum_{k=0}^n k!}{2}$$ + +A363102: Denominator of the continued fraction $1/(2-3/(3-4/(4-5/(...(n-1)-n/(-2)))))$. +The sequence is defined by the formula: +$$a(n) = \frac{n^2 - 2}{\gcd(n^2 - 2, 2 \cdot A051403(n-3) + n \cdot A051403(n-4))}$$ +The formula is valid for $n \ge 3$. + +*References:* +- [A363102](https://oeis.org/A363102) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +- [A051403](https://oeis.org/A051403) +-/ + +namespace OeisA363102 + + +open Nat Finset + +/-- +Auxiliary sequence A051403, defined as +$$\frac{(n+2) \sum_{k=0}^n k!}{2}$$ +-/ +def a051403 (n : ℕ) : ℕ := + let fact_sum := Finset.sum (range (n + 1)) (fun k => k.factorial) + ((n + 2) * fact_sum) / 2 + +/-- +A363102: Denominator of the continued fraction $1/(2-3/(3-4/(4-5/(...(n-1)-n/(-2)))))$. +The sequence is defined by the formula: +$$a(n) = \frac{n^2 - 2}{\gcd(n^2 - 2, 2 \cdot A051403(n-3) + n \cdot A051403(n-4))}$$ +The formula is valid for $n \ge 3$. +-/ +def a (n : ℕ) : ℕ := + let num : ℕ := n ^ 2 - 2 + let a051403_nm3 := a051403 (n - 3) + let a051403_nm4 := a051403 (n - 4) + let denom_arg := 2 * a051403_nm3 + n * a051403_nm4 + -- The subtraction n^2 - 2 is safe for n >= 3. + num / Nat.gcd num denom_arg + + +@[category test, AMS 11] +lemma a_three : a 3 = 7 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 7 := by rfl + +@[category test, AMS 11] +lemma a_five : a 5 = 23 := by rfl + +@[category test, AMS 11] +lemma a_six : a 6 = 17 := by rfl + +@[category test, AMS 11] +lemma a_seven : a 7 = 47 := by rfl + + +/-- +Auxiliary sequence A051403, defined as +$$\frac{(n+2) \sum_{k=0}^n k!}{2}$$ + +A363102: Denominator of the continued fraction $1/(2-3/(3-4/(4-5/(...(n-1)-n/(-2)))))$. +The sequence is defined by the formula: +$$a(n) = \frac{n^2 - 2}{\gcd(n^2 - 2, 2 \cdot A051403(n-3) + n \cdot A051403(n-4))}$$ +The formula is valid for $n \ge 3$. + +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/363102.wip.lean#L283"] +theorem a_eq_one_or_prime : ∀ n : ℕ, 3 ≤ n → a n = 1 ∨ Nat.Prime (a n) := by + sorry + +end OeisA363102 diff --git a/FormalConjectures/OEIS/363347.lean b/FormalConjectures/OEIS/363347.lean new file mode 100644 index 0000000000..ca4921702b --- /dev/null +++ b/FormalConjectures/OEIS/363347.lean @@ -0,0 +1,104 @@ +/- +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 a + +Helper function for a, which computes the denominator $R_k(n)$ of the continued fraction expression. +For $2 \le k \le n-1$, $R_k(n)$ is defined recursively: +$$R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$$ +The base case is $R_{n-1}(n) = (n-1) - \frac{n}{-4}$. + +*References:* +- [A363347](https://oeis.org/A363347) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA363347 + + +open Rat Nat + +/-- +Helper function for a, which computes the denominator $R_k(n)$ of the continued fraction expression. +For $2 \le k \le n-1$, $R_k(n)$ is defined recursively: +$$R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$$ +The base case is $R_{n-1}(n) = (n-1) - \frac{n}{-4}$. +-/ +def continued_fraction_denominator (n k : ℕ) : ℚ := + if n ≤ 2 then 0 + else + -- The recursive descent involves terms from $k=n-1$ down to $k=2$. + if 2 ≤ k ∧ k ≤ n - 1 then + -- Base Case: k = n - 1. + if k = n - 1 then + -- R_{n-1} = (n-1) + n/4 + (k : ℚ) + (n : ℚ) / 4 + -- Recursive Step: 2 <= k < n - 1. + else + let R_next := continued_fraction_denominator n (k + 1) + -- R_k = k - (k+1) / R_{k+1} + (k : ℚ) - (k + 1 : ℚ) / R_next + else 0 +termination_by n - k + +/-- +a: Denominator of the continued fraction +$$\frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{-4}}}}}} $$ +The value of the continued fraction is $C_n = 1/R_2(n)$. +If $R_2(n) = N/D$ in reduced form, $C_n = D/N$. +The sequence $a(n)$ is the denominator of the final fraction, which is $\vert N \vert$. +-/ +noncomputable def a (n : ℕ) : ℕ := + if n ≤ 2 then 0 -- The sequence is indexed starting from $n=3$. + else + let R2 := continued_fraction_denominator n 2 + R2.num.natAbs + + +@[category test, AMS 11] +lemma a_three : a 3 = 11 := by delta a; repeat rw [continued_fraction_denominator]; norm_num + +@[category test, AMS 11] +lemma a_four : a 4 = 5 := by delta a; repeat rw [continued_fraction_denominator]; norm_num + +@[category test, AMS 11] +lemma a_five : a 5 = 31 := by delta a; repeat rw [continued_fraction_denominator]; norm_num + +@[category test, AMS 11] +lemma a_six : a 6 = 11 := by delta a; repeat rw [continued_fraction_denominator]; norm_num + +@[category test, AMS 11] +lemma a_seven : a 7 = 59 := by delta a; repeat rw [continued_fraction_denominator]; norm_num + + +/-- +Helper function for a, which computes the denominator $R_k(n)$ of the continued fraction expression. +For $2 \le k \le n-1$, $R_k(n)$ is defined recursively: +$$R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$$ +The base case is $R_{n-1}(n) = (n-1) - \frac{n}{-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/363347.wip.lean#L825"] +theorem exists_a_eq_prime : + ∀ p : ℕ, (p.Prime ∧ (p ≡ 1 [MOD 10] ∨ p ≡ 9 [MOD 10])) → ∃ n : ℕ, a n = p := by + sorry + +end OeisA363347 diff --git a/FormalConjectures/OEIS/368692.lean b/FormalConjectures/OEIS/368692.lean new file mode 100644 index 0000000000..11ff8f91ba --- /dev/null +++ b/FormalConjectures/OEIS/368692.lean @@ -0,0 +1,79 @@ +/- +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 A368692 + +A368692: +$$a(n) = \frac{(12n + 6)! \cdot (6n + 9)!}{108 \cdot (4n + 2)! \cdot +(2n + 3)! \cdot ((6n + 5)!)^2}$$ +It is conjectured that $a(n)$ are integers. + +*References:* +- [A368692](https://oeis.org/A368692) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA368692 + + +open Nat + +/-- +A368692: +$$a(n) = \frac{(12n + 6)! \cdot (6n + 9)!}{108 \cdot (4n + 2)! \cdot +(2n + 3)! \cdot ((6n + 5)!)^2}$$ +It is conjectured that $a(n)$ are integers. +-/ +def a (n : ℕ) : ℕ := + let num : ℕ := (12 * n + 6)! * (6 * n + 9)! + let den_base : ℕ := (4 * n + 2)! * (2 * n + 3)! * ((6 * n + 5)!)^2 + num / (108 * den_base) + + +@[category test, AMS 11] +lemma a_zero : a 0 = 14 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 563108 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 54231252075 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 6700034035890000 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 928978310614152999200 := by rfl + + +/-- +A368692: +$$a(n) = \frac{(12n + 6)! \cdot (6n + 9)!}{108 \cdot (4n + 2)! \cdot +(2n + 3)! \cdot ((6n + 5)!)^2}$$ +It is conjectured that $a(n)$ are integers. + +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/368692.wip.lean#L158"] +theorem a_is_int (n : ℕ) : 108 * ((4 * n + 2)! * (2 * n + 3)! * ((6 * n + 5)!) ^ 2) ∣ + (12 * n + 6)! * (6 * n + 9)! := by + sorry + +end OeisA368692 diff --git a/FormalConjectures/OEIS/372761.lean b/FormalConjectures/OEIS/372761.lean new file mode 100644 index 0000000000..a4aa51852a --- /dev/null +++ b/FormalConjectures/OEIS/372761.lean @@ -0,0 +1,116 @@ +/- +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 A372761 + +Recursive function to compute $A_k(n)$, the denominator tail $k - \frac{k+1}{A_{k+1}(n)}$. +The base case is at $k = n - 1$, where $A_{n-1} = (n-1) - \frac{n}{n+4}$. + +The total value of the continued fraction $C_n$. + +*References:* +- [A372761](https://oeis.org/A372761) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA372761 + + +open scoped Nat + +open Rat + +/-- +Recursive function to compute $A_k(n)$, the denominator tail $k - \frac{k+1}{A_{k+1}(n)}$. +The base case is at $k = n - 1$, where $A_{n-1} = (n-1) - \frac{n}{n+4}$. +-/ +noncomputable def continued_fraction_tail (n : ℕ) : ℕ → ℚ +| k => + if n ≥ 4 then + if k = n - 1 then + (n - 1 : ℚ) - (n : ℚ) / (n + 4 : ℚ) + else if 3 ≤ k ∧ k < n - 1 then + let k_succ_val := continued_fraction_tail n (k + 1) + -- Division by zero handling for total function definition + if k_succ_val = 0 then 0 else + (k : ℚ) - (k + 1 : ℚ) / k_succ_val + else + 0 + else + 0 +termination_by k => n - k + +/-- +The total value of the continued fraction $C_n$. +-/ +noncomputable def continued_fraction_val (n : ℕ) : ℚ := + if n ≤ 2 then + 0 + else if n = 3 then + -- Formula for n=3: 1 / (2 - 3 / (3 + 4)) = 7/11 + let val : ℚ := 2 - 3 / 7 + if val = 0 then 0 else 1 / val + else -- n ≥ 4 + let A3 := continued_fraction_tail n 3 + let val : ℚ := 2 - 3 / A3 + + -- Division by zero check for the final rational value + if val = 0 then 0 else 1 / val + +/-- +A372761: Denominator of the continued fraction +$$ \frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{n+4}}}}}} $$ +-/ +noncomputable def a (n : ℕ) : ℕ := + if n < 3 then 0 -- Sequence starts at n=3. + else (continued_fraction_val n).den + + +@[category test, AMS 11] +lemma a_four : a 4 = 4 := by + delta a continued_fraction_val; repeat rw [continued_fraction_tail]; norm_num + +@[category test, AMS 11] +lemma a_five : a 5 = 7 := by + delta a continued_fraction_val; repeat rw [continued_fraction_tail]; norm_num + +@[category test, AMS 11] +lemma a_six : a 6 = 13 := by + delta a continued_fraction_val; repeat rw [continued_fraction_tail]; norm_num + +@[category test, AMS 11] +lemma a_seven : a 7 = 31 := by + delta a continued_fraction_val; repeat rw [continued_fraction_tail]; norm_num + + +/-- +Recursive function to compute $A_k(n)$, the denominator tail $k - \frac{k+1}{A_{k+1}(n)}$. +The base case is at $k = n - 1$, where $A_{n-1} = (n-1) - \frac{n}{n+4}$. + +The total value of the continued fraction $C_n$. + +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/372761.wip.lean#L733"] +theorem exists_unique_a_eq_prime : + ∀ p : ℕ, Nat.Prime p ∧ p % 2 = 1 ∧ p ≠ 3 ∧ p ≠ 5 → ∃! n, n ≥ 3 ∧ a n = p := by + sorry + +end OeisA372761 diff --git a/FormalConjectures/OEIS/382590.lean b/FormalConjectures/OEIS/382590.lean new file mode 100644 index 0000000000..1434c4bdbf --- /dev/null +++ b/FormalConjectures/OEIS/382590.lean @@ -0,0 +1,105 @@ +/- +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 a + +Helper function for a, computing the pair $(a(n), b(n))$ such that: +$a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)$ +$b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)$ + +*References:* +- [A382590](https://oeis.org/A382590) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA382590 + + +open scoped Classical + +open Int + +/-- +Helper function for a, computing the pair $(a(n), b(n))$ such that: +$a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)$ +$b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)$ +-/ +def A382590_pair : ℕ → ℤ × ℤ +| 0 => (1, 1) +| 1 => (2, 1) +| n + 2 => + let (a_n_plus_1, b_n_plus_1) := A382590_pair (n + 1) + let (a_n, b_n) := A382590_pair n + (a_n_plus_1 * b_n + a_n * b_n_plus_1, a_n_plus_1 * b_n - a_n * b_n_plus_1) + +/-- +a: $a(n)$ is the sequence defined by the mutual recurrence relations: +$a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)$ and $b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)$ +starting with $a(0) = b(0) = b(1) = 1$ and a(1) = 2. +The terms are in $\mathbb{Z}$ due to negative values. +-/ +def a (n : ℕ) : ℤ := (A382590_pair n).fst + +open Nat + +/-- +The k-th prime factor of an integer n (where k>=1), counted with multiplicity. +This is defined as the k-th element (0-indexed k-1) of `Nat.primeFactorsList n.natAbs`. +Returns 1 if n has fewer than k prime factors or if n is 0, 1, or -1, +following the informal convention. +-/ +def kth_prime_factor (k : ℕ) (n : ℤ) : ℕ := + if h₀ : k = 0 then 1 else + let n_abs := Int.natAbs n + let L := primeFactorsList n_abs + -- prime factors list length is L.length. We look for k-th element, index k-1. + if h_len : k - 1 ≥ L.length then 1 else + L[k - 1] + + +@[category test, AMS 11] +lemma a_zero : a 0 = 1 := by rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 2 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 3 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 5 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 8 := by rfl + + +/-- +Helper function for a, computing the pair $(a(n), b(n))$ such that: +$a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)$ +$b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)$ + +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/382590.wip.lean#L281"] +theorem kth_prime_factor_periodic : ∀ k : ℕ, k ≥ 2 → ∃ N₀ p : ℕ, p > 0 ∧ + ∀ n : ℕ, n ≥ N₀ → kth_prime_factor k (a (n + p)) = kth_prime_factor k (a n) := by + sorry + +end OeisA382590 diff --git a/FormalConjectures/OEIS/51293.lean b/FormalConjectures/OEIS/51293.lean new file mode 100644 index 0000000000..4166259668 --- /dev/null +++ b/FormalConjectures/OEIS/51293.lean @@ -0,0 +1,114 @@ +/- +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 A51293 + +a: Number of nonempty subsets of $\{1, 2, 3, \dots, n\}$ whose elements have an integer average. + +`S_real n k` is the number of $k$-element subsets of $\{1, 2, \dots, n\}$ +whose sum is divisible by $k$. +By the roots of unity filter, this exact count can be written as: +$S_{n,k} = \frac{1}{k} \sum_{j=0}^{k-1} \sum_{A \in \binom{n}{k}} \omega^{j \sum A}$. +The main term $j=0$ yields exactly $\frac{1}{k} \binom{n}{k}$. +For $j > 0$, the roots of unity evaluated over the subsets yield bounded periodic sums. +The maximal magnitude of these periodic products is achieved when the order of the root is 2, +which bounds the error term magnitude strictly by $2 \cdot 2^{n/2}$. + +*References:* +- [A51293](https://oeis.org/A51293) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA51293 + + +open Polynomial + +open scoped Topology + +/- +Copyright 2025 Google LLC + +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. +-/ + +open Finset Nat Real Filter Asymptotics + +/-- +a: Number of nonempty subsets of $\{1, 2, 3, \dots, n\}$ whose elements have an integer average. +-/ +def a (n : ℕ) : ℕ := + Finset.card ( + (Finset.Icc 1 n).powerset.filter fun S : Finset ℕ => + S.Nonempty ∧ S.card ∣ S.sum id + ) + +noncomputable def a_real (n : ℕ) : ℝ := a n + + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by rfl + +@[category test, AMS 11] +lemma a_two : a 2 = 2 := by rfl + +@[category test, AMS 11] +lemma a_three : a 3 = 5 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 8 := by rfl + +@[category test, AMS 11] +lemma a_five : a 5 = 15 := by rfl + + +/-- +a: Number of nonempty subsets of $\{1, 2, 3, \dots, n\}$ whose elements have an integer average. + +`S_real n k` is the number of $k$-element subsets of $\{1, 2, \dots, n\}$ +whose sum is divisible by $k$. +By the roots of unity filter, this exact count can be written as: +$S_{n,k} = \frac{1}{k} \sum_{j=0}^{k-1} \sum_{A \in \binom{n}{k}} \omega^{j \sum A}$. +The main term $j=0$ yields exactly $\frac{1}{k} \binom{n}{k}$. +For $j > 0$, the roots of unity evaluated over the subsets yield bounded periodic sums. +The maximal magnitude of these periodic products is achieved when the order of the root is 2, +which bounds the error term magnitude strictly by $2 \cdot 2^{n/2}$. + +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/51293.wip.lean#L503"] +theorem tendsto_a_real_asymptotic : + Tendsto (fun n : ℕ => (a_real n - ((2 : ℝ) ^ (n + 1) / (n : ℝ)) * + ((1 : ℝ) + 1 / (n : ℝ) + 3 / ((n : ℝ) ^ 2) + 13 / ((n : ℝ) ^ 3) + + 75 / ((n : ℝ) ^ 4) + 541 / ((n : ℝ) ^ 5))) / + (((2 : ℝ) ^ (n + 1)) / ((n : ℝ) ^ 6))) atTop (nhds 0) := by + sorry + +end OeisA51293 diff --git a/FormalConjectures/OEIS/62567.lean b/FormalConjectures/OEIS/62567.lean new file mode 100644 index 0000000000..16e0add896 --- /dev/null +++ b/FormalConjectures/OEIS/62567.lean @@ -0,0 +1,118 @@ +/- +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 A62567 + +The number whose digits in base 10 are $n$'s digits reversed. + +A062567: First multiple of $n$ whose reverse is also divisible by $n$, +or 0 if no such multiple exists. + +*References:* +- [A62567](https://oeis.org/A62567) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA62567 + + +open Nat Classical + +/-- The number whose digits in base 10 are $n$'s digits reversed. -/ +def reverse_nat (k : ℕ) : ℕ := + ofDigits 10 (digits 10 k).reverse + +/-- +A062567: First multiple of $n$ whose reverse is also divisible by $n$, +or 0 if no such multiple exists. +-/ +noncomputable def a (n : ℕ) : ℕ := + if n = 0 then 0 + else + -- P(k) is the predicate for the multiplier k: k > 0 and n divides the reverse of (k*n). + let P (k : ℕ) : Prop := k > 0 ∧ n ∣ reverse_nat (k * n) + + -- We check if a solution exists (using classical reasoning, since P is decidable). + if h_ex : ∃ k, P k then + -- Nat.find requires a DecidablePred instance, which holds for this property on ℕ. + have HP : DecidablePred P := by infer_instance + -- k_min is the smallest multiplier k >= 1. + let k_min : ℕ := Nat.find h_ex + k_min * n + else + 0 + + +@[category API, AMS 11] +lemma a_eq_self (n : ℕ) (hn : n > 0) (h_rev : n ∣ reverse_nat n) : a n = n := by + unfold a + rw [if_neg (by omega)] + have h_ex : ∃ k, k > 0 ∧ n ∣ reverse_nat (k * n) := ⟨1, ⟨by omega, by rw [one_mul]; exact h_rev⟩⟩ + rw [dif_pos h_ex] + change Nat.find h_ex * n = n + have hf : Nat.find h_ex = 1 := by + rw [Nat.find_eq_iff] + refine ⟨⟨by omega, by rw [one_mul]; exact h_rev⟩, ?_⟩ + intro k hk + interval_cases k + simp + rw [hf, one_mul] + +@[category API, AMS 11] +lemma reverse_nat_of_lt (k : ℕ) (hk0 : k ≠ 0) (hk10 : k < 10) : reverse_nat k = k := by + unfold reverse_nat + rw [Nat.digits_of_lt 10 k hk0 hk10] + rfl + +@[category test, AMS 11] +lemma a_one : a 1 = 1 := by + apply a_eq_self 1 (by omega) (by rw [reverse_nat_of_lt 1 (by decide) (by decide)]) + +@[category test, AMS 11] +lemma a_two : a 2 = 2 := by + apply a_eq_self 2 (by omega) (by rw [reverse_nat_of_lt 2 (by decide) (by decide)]) + +@[category test, AMS 11] +lemma a_three : a 3 = 3 := by + apply a_eq_self 3 (by omega) (by rw [reverse_nat_of_lt 3 (by decide) (by decide)]) + +@[category test, AMS 11] +lemma a_four : a 4 = 4 := by + apply a_eq_self 4 (by omega) (by rw [reverse_nat_of_lt 4 (by decide) (by decide)]) + +@[category test, AMS 11] +lemma a_five : a 5 = 5 := by + apply a_eq_self 5 (by omega) (by rw [reverse_nat_of_lt 5 (by decide) (by decide)]) + + +/-- +The number whose digits in base 10 are $n$'s digits reversed. + +A062567: First multiple of $n$ whose reverse is also divisible by $n$, +or 0 if no such multiple exists. + +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/62567.wip.lean#L324"] +theorem a_three_pow_eq (n : ℕ) : + 2 ≤ n → (a (3 ^ n) = 10 ^ (3 ^ (n - 2)) - 1 ↔ n = 2 ∨ n = 3 ∨ n = 4) := by + sorry + +end OeisA62567 diff --git a/FormalConjectures/OEIS/91669.lean b/FormalConjectures/OEIS/91669.lean new file mode 100644 index 0000000000..5bec6182de --- /dev/null +++ b/FormalConjectures/OEIS/91669.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 A91669 + +A091669: $a(n) = \frac{2^{n-1}}{n!} \prod_{k=1}^{n-1} (2^k-1)$. +The sequence $a(n)$ is composed of natural numbers, thus we define it +as a function $\mathbb{N} \to \mathbb{N}$. + +*References:* +- [A91669](https://oeis.org/A91669) +- [arxiv/2605.22763](https://arxiv.org/abs/2605.22763) *Advancing Mathematics Research with AI-Driven Formal Proof Search* by George Tsoukalas et al. +-/ + +namespace OeisA91669 + + +open Nat BigOperators + +/-- +A091669: $a(n) = \frac{2^{n-1}}{n!} \prod_{k=1}^{n-1} (2^k-1)$. +The sequence $a(n)$ is composed of natural numbers, thus we define it +as a function $\mathbb{N} \to \mathbb{N}$. +-/ +noncomputable def a (n : ℕ) : ℕ := + if n = 0 then 0 -- Sequence is defined for n >= 1. + else + let n_pred : ℕ := n.pred + + -- The numerator of the expression. Both factors are in ℕ. + let numerator : ℕ := (2 ^ n_pred) * (Finset.Ico 1 n).prod (fun k => 2 ^ k - 1) + + -- The denominator is $n!$. + let denominator : ℕ := n.factorial + + -- The division is exact, since the result is an integer sequence. + numerator / denominator + + +@[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 = 2 := by rfl + +@[category test, AMS 11] +lemma a_four : a 4 = 7 := by rfl + +@[category test, AMS 11] +lemma a_five : a 5 = 42 := by rfl + + +/-- +A091669: $a(n) = \frac{2^{n-1}}{n!} \prod_{k=1}^{n-1} (2^k-1)$. +The sequence $a(n)$ is composed of natural numbers, thus we define it +as a function $\mathbb{N} \to \mathbb{N}$. + +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/91669.wip.lean#L250"] +theorem prime_and_primitive_root_of_dvd (n : ℕ) (hn : n > 2) : n ∣ (a (n - 1) + 2 ^ (n - 2)) → + Nat.Prime n ∧ IsPrimitiveRoot (2 : ZMod n) (Nat.totient n) := by + sorry + +end OeisA91669