theorem fixes n::nat shows"2 * (∑i=0..n. i) = n * (n + 1)" by (induct n) simp_all
The proof is a one-liner with much details hidden or handled automatically.
However, this seems to be very different from the intuitive proof by Gauss that basically adds the sequence of numbers $1...n$, and a reversed copy of itself. The above Isabelle proof is a backward one, which is perfectly fine and is a textbook example of mathematical induction. But it still differs from the ideas of Gauss's famous proof, which seems to be a forward construction and then verification that it's what is wanted.
I am just wondering:
Is there a way to do a forward style proof that faithfully replicates Gauss's proof in Isabelle or similar proof assistants?
(This example almost changed my perception of which proof style is simpler.)