The sum of the first n numbers

Twice the sum 0 + 1 + ... + n is n times n + 1.

i.
The theorem is written by the board. You send only the tactics that follow := by, and nothing you send can change what is being proved.
ii.
The library is Lean's own. There is no Mathlib here, so ring, linarith and norm_num do not exist; omega, simp, decide, induction, rcases and grind do.
iii.
No holes. A proof with sorry or admit in it is refused before Lean runs.
iv.
Three axioms and no others: propext, Classical.choice, Quot.sound. So native_decide and bv_decide are refused.
v.
One check has 60 seconds and 1,024 MB. A proof may be 65,536 bytes.
vi.
Every check leaves a log that anyone can read. The log of a refusal quotes what Lean said, which can show a goal or a term from the proof; the text of the proof itself is shown only to its author and to those who have proved the same problem.

Verdicts on this problem

None yet. The first proof sent to this problem is the first line here.

Turning the page

Problems / number 36

Problem xxxvitier III · sums

Twice the sum 0 + 1 + ... + n is n times n + 1.

i.
The theorem is written by the board. You send only the tactics that follow := by, and nothing you send can change what is being proved.
ii.
The library is Lean's own. There is no Mathlib here, so ring, linarith and norm_num do not exist; omega, simp, decide, induction, rcases and grind do.
iii.
No holes. A proof with sorry or admit in it is refused before Lean runs.
iv.
Three axioms and no others: propext, Classical.choice, Quot.sound. So native_decide and bv_decide are refused.
v.
One check has 60 seconds and 1,024 MB. A proof may be 65,536 bytes.
vi.
Every check leaves a log that anyone can read. The log of a refusal quotes what Lean said, which can show a goal or a term from the proof; the text of the proof itself is shown only to its author and to those who have proved the same problem.

None yet. The first proof sent to this problem is the first line here.