feat(OEIS): add solutions from AlphaProof Nexus#4384
Conversation
…ain theorems in all .wip.lean files
… in all .wip.lean files
|
👋 This is an automated welcome message. 🤖 A few friendly reminders while the review gets started:
Thanks again for helping improve Formal Conjectures. |
| 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}$. |
There was a problem hiding this comment.
There is no verbatim citation of the conjecture: all elements in absolute value are Fibonacci numbers. It seems like the conjecture is that all values are integers.
|
|
||
| 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. |
There was a problem hiding this comment.
This isn't the full statement of the conjecture.
Conjecture: All the rational numbers Sum_{i=j..k} 1/a(i) with 0 < min{2,k} <= j <= k have pairwise distinct fractional parts.
|
|
||
| @[category test, AMS 11] | ||
| lemma a_one : a 1 = 1 := by rfl | ||
|
|
| 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$. | ||
|
|
There was a problem hiding this comment.
The statement of the conjecture is missing.
| -/ | ||
| @[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 |
There was a problem hiding this comment.
The statement is for a(m, n), a more general sequence. It seems to me the proof is just for m=8, it doesn't prove the full conjecture.
| 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). |
There was a problem hiding this comment.
The conjecture statement is missing.
|
|
||
|
|
||
| /-- | ||
| The sequence $b_n$ such that $A227582(n) = b_{n-1}$ for $n \ge 1$. |
There was a problem hiding this comment.
As before this comment is duplicated with the one above.
|
|
||
| @[category test, AMS 11] | ||
| lemma a_four : a 4 = 674708032182398976 := by sorry | ||
|
|
|
|
||
|
|
||
| /-- | ||
| A237271: Number of parts in the symmetric representation of $\sigma(n)$. |
There was a problem hiding this comment.
Same observations as before about the comment.
| 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). |
There was a problem hiding this comment.
There are multiple conjectures in the webpage, should all be included here?
2 participants
This upstreams the findings of https://github.com/google-deepmind/alphaproof-nexus-results/tree/main/APNOutputs/OEIS
from https://arxiv.org/abs/2605.22763.
As a follow up we plan to also potenially add the (cleaned-up) unsolved questions that remain, see here:
https://github.com/google-deepmind/formal-conjectures/tree/auto_oeis/FormalConjectures/OEIS/Auto