Here is an example of proving something using induction in Sage. Suppose we want to prove that:
\begin{equation*}
\sum_{k=1}^{n}k^{2}=\frac{n(n+1)(2n+1)}{6}
\end{equation*}
n = var('n') A = n*(n+1)*(2*n+1)/6 print(f"Up to n:\n {A}") B = A + (n+1)^2 print(f"Induction Step:\n {B.factor()}") u = var('u') print(f"In terms of n+1:\n {B.substitute(n==u-1).factor()}")
Up to n: 1/6*(2*n + 1)*(n + 1)*n Induction Step: 1/6*(2*n + 3)*(n + 2)*(n + 1) Inn terms of n+1: 1/6*(2*u + 1)*(u + 1)*u