Solution (source code)

= Solution

For the odd-square sum, the initial case $n=1$ gives $1=(4-1)/3$. Assume the formula at $n$. Adding the next square gives
$$
\sum_{j=1}^{n+1}(2j-1)^2
=\frac{4n^3-n}{3}+(2n+1)^2
=\frac{4n^3+12n^2+11n+3}{3}
=\frac{4(n+1)^3-(n+1)}3.
$$
The initial case and this <induction> step prove $\boxed{\sum_{j=1}^n(2j-1)^2=(4n^3-n)/3}$ for every positive <integer> $n$.

For the <divisibility> assertion, $1^3+5\cdot1=6$. The change when $n$ is replaced by $n+1$ is
$$
(n+1)^3+5(n+1)-(n^3+5n)=3n(n+1)+6.
$$
One of the consecutive <integers> $n,n+1$ is even, so the displayed change is divisible by $6$. If $n^3+5n$ is divisible by $6$, its successor is too. Thus <induction> proves $\boxed{6\mid n^3+5n}$ for every $n\geq1$.