I thought this would be the very end of objections to the result. In Lean, the last theorem:
theorem Sgoal : Sum_S n + Tail_S n = -1/12Where Sum_S is the finite part of terms expanded out, n*(n+1)/2,
and Tail_S n is Sf n - Sum_S n, where Sf n is a constant value
that I got by solving for Sf n starting from subtracting B from S
and noticing that S is related to a multiple of itself; enough
to not get a tautology where you would otherwise just be able to
set S to whatever you like. This is the result of theorem Sgoal:
∀ {n : ℤ}, Sum_S n + Tail_S n = -1 / 12
Lean famously has a goal of removing human judgement from the process. But there is always an issue over what it is you stated. And when you have a bunch of theorems, it may not be clear that they are correctly linked. A bunch of people are unhappy to see this. One objection is in not using the summation operator for the finite sum.
This proof is accepted by Lean, but even with the theorems to justify
choices and to pick the value of S for us, there is the suspicion that
the definition of Sf and justifySf are just picking arbitrary values.
The value S that it finds is notable. It is the sum of all powers of 13.
Note that the number that it solves for has a use in calculating the closed form.
S = 1 + 13 S
→
-12 S = 1
→
S = -1/12
S = 1 + 13 S = 1 + 13(1 + 13 S)
= 13^0 + 13^1 + 13^2 + ... + 13^n + ( 13^(n+1) * S )
→
S - 13^(n+1)*S = 13^0 + 13^1 + 13^2 + ... + 13^n
=
S*(1 - 13^(n+1))
=
(-1/12)*(1 - 13^(n+1))
=
(13^(n+1) - 1)/12
Which you could imagine a base 13 number with all 1 digits.
That makes it a number with an infinite number of digits representation,
literally setting every base13 digit to a 1. It is called -1/12 because
if you multiply this number times 12, it is an infinite digit representation
of -1; such that if you then add 1 to it, you get 0 via a ripple-carry.
It means this, using the waffly +... notation:
13^0 + 13^1 + 13^2 + ... = 1 + 2 + 3 + ...
Anyways, 1+2+3+...=-1/12 is a result first noted by Ramanujan; and he probably gave no proof of it at the time. There are applications for divergent sums; where you can use a recursively defined divergent sum to solve sequence X as (X - Tail_X(n)). It results in a closed form for the sum of the first n powers. Anyways, this is the latest thing that passes in Lean:
import Mathlib
import Mathlib.Tactic.Ring
import Mathlib.Analysis.Calculus.Deriv.Basic
/-
This is just a note about the origins by which S was found.
We took a common sequence: A = 1 + x*A
And we differentiated it. F = dA/dx
And called B=F(-1),
which expands to the alternating sequence: B=1 + (-2) + 3 + (-4) + 5 + (-6) + ...
We then combined it with S = n(n+1)/2 + Tail_S n = Sum_S n + Tail_S n = 1 + 2 + 3 + ... + n + Tail_S n
A recursive method of writing sums without the ambiguitity of what is going on in "+..." on the end.
From there, we discover that S-B=4*S.
We do need to be careful about handling the expansion rate of S-B though:
S-B = 0 + 4 + 0 + 8 + 0 + 12 + 0 + 16 + ...
So, the notation retains how many expansions were done.
We algebraically are forced to assign S=-1/12, given B.
We might be able to use something other than B to pin down S,
but with S = Sum_S n + Tail_S n alone, S could have been assigned any value.
-/
/- from A=1-x*A -/
def Sum_A (x : ℚ) (n : ℤ) : ℚ := (1 - x^(n+1))/(1-x)
def Tail_A (x : ℚ) (n : ℤ) : ℚ := x^(n+1)/(1-x)
/- F = dA/dX -/
def Sum_F (x : ℚ) (n : ℤ) : ℚ := (1 - (n+1)*x^n + n*x^(n+1))/((1-x)^2)
def Tail_F (x : ℚ) (n : ℤ) : ℚ := ((n+1)*x^n - n*x^(n+1))/((1-x)^2)
/- A = 1 + x*A = (x^0 + x^1 + x^2 + ... + x^n) + x^(n+1)A = 1/(1-x) -/
def Af (x : ℚ):ℚ := 1/(1-x)
/- dA/dx = F = 1/((1-x)^2) = 0 x^(-1) + 1 x^0 + 2 x^1 + 3 x^2 + ... + n x^(n-1) + d[(x^(n+1))/(1-x))]/dx -/
/- Tail_F(-1) = ((2*n+1)*(-1)^n)/4 -/
/- Sum_F(-1) = Ff(-1) - Tail_F(-1) -/
def Ff (x : ℚ):ℚ := 1/((1-x)^2)
-- Af is an infinite sum expressed recursively:
theorem A_decomposition (x : ℚ) (n : ℤ) :
Af x = Sum_A x n + Tail_A x n := by
unfold Af Sum_A Tail_A
ring
-- Ff is a recursive sum expressed recursively, not proven to be d[Sum_A]/dx + d[Tail_A]/dx
theorem F_decomposition (x : ℚ) (n : ℤ) :
Ff x = Sum_F x n + Tail_F x n := by
unfold Ff Sum_F Tail_F
simp
ring
/- B = F(-1) = 1 + -2 + 3 + -4 + 5 + -6 + ... + (Tail_F (-1) n)
This is just an explanation of WHY B was chosen, and is not critical
to the proof. However, if we started with A,
then Sum_F = d[Sum_A x n]/dx and Tail_F = d[Tail_A x n]/dx,
and Sum_B n = Sum_F (-1) n and Tail_B = Sum_F (-1) n work just fine.
It's just that justifying the choice of B isn't critical.
It only matters that S-B causes a self relation that pins down Sf n for us.
Sum_S (2*n) - Sum_B (2*n) = 4*(Sum_S n) is the part of the proof
that gives "0 + 2 + 0 + 4 + 0 + 8 + ...", where it is important that
we keep the expansion at HALF the rate, and not lose it in "+ ..." notation.
Tail_B = Tail_F (-1) = d[Tail_A]/dx (-1)
Sum_B = Sum_F (-1) = d[Sum_A]/dx (-1)
-/
def Tail_B (n : ℤ) : ℚ := ((2*n+1)*(-1)^n)/4
def Sum_B (n : ℤ) : ℚ := (Ff (-1)) - Tail_B n
def Term_B (n:ℤ):ℚ := Sum_B (n) - Sum_B (n-1)
def Bf (n:ℤ):ℚ := Sum_B n + Tail_B n
/- It would be nice if we had a general method to only specify the sum
as a closed form, and have it generally just give us (Sf n)
-/
def Sum_S (n : ℤ ) : ℚ := n*(n+1)/2
/- justifySf is why this defintion was chosen. -/
def Sf (n:ℤ):ℚ := (4*Sum_S n - (Sum_S (2*n) + Tail_B (2*n)))/3
def Tail_S (n : ℤ) : ℚ := Sf n - Sum_S n
def Term_S (n:ℤ):ℚ := Sum_S (n) - Sum_S (n-1)
/- Claude suggested a rational_algebra tactic should handle this! -/
theorem even_power_neg_one (n : ℤ) : (-1:ℚ)^(2*n) = 1 := by
rw [zpow_mul, zpow_ofNat, neg_one_sq]
simp
/- Justify the definition of (Sf n), is a result of S-B=4*S -/
theorem justifySf:
(Sf n = Sf (n+1)) ∧
(Bf n = Bf (n+1)) ∧
(Sum_S n + Tail_S n = Sf n) → Sf n = 1 + 13*(Sf n) ∧
(Sum_S (2*n) - Sum_B (2*n) = 4*Sum_S n) ∧
(Sf n = (4*Sum_S n - (Sum_S (2*n) + Tail_B (2*n)))/3)
→ 4*Sum_S n - Sum_S (2*n) - Tail_B (2*n) = 3*(Sf n)
→ (Sf n) - Sum_S (2*n) - Tail_B (2*n) = 4*(Sf n) - 4*Sum_S n
→ (Sf (2*n)) - Sum_S (2*n) - Tail_B (2*n) = 4*Tail_S n
→ Tail_S (2*n) - Tail_B (2*n) = 4*Tail_S n
:= by
unfold Sum_S Sum_B Ff Tail_B Sf Sum_S Tail_B Tail_S Sf Sum_S Tail_B
simp
/- handle objections to using a closed form n*(n+1)/2 -/
-- summing 1 + 2 + ... + n
def sum_first_n(n: Nat) : Nat :=
match n with
| 0 => 0
| m + 1 => m + 1 + sum_first_n m
theorem closedFormS (n: Nat) :
sum_first_n n = n * (n + 1) / 2 := by
induction n
· simp [sum_first_n]
case succ m ih =>
simp [sum_first_n]
rw [ih]
ring_nf
rw [(by ring: m * 3 = m * 2 + m)]
rw [(by ring: 2 + (m * 2 + m) = 2 * (m + 1) + m)]
rw [Nat.add_assoc (2 * (m + 1)) _ _, Nat.add_comm (2 * (m + 1)) _]
rw [Nat.add_mul_div_left _ _ (by decide : (0 < 2))]
ring
/-
"Undefined behavior gets defined by having an implementation."
-- A Computer Security proverb.
-/
theorem sampleBf :
1 + Tail_B 1 = 1 + (-2) + Tail_B 2 ∧
1 + (-2) + Tail_B 2 = 1 + (-2) + 3 + Tail_B 3 ∧
1 + (-2) + 3 + Tail_B 3 = 1 + (-2) + 3 + (-4) + Tail_B 4 ∧
1 + (-2) + 3 + (-4) + Tail_B 4 = 1 + (-2) + 3 + (-4) + 5 + Tail_B 5 ∧
1 + (-2) + 3 + (-4) + 5 + Tail_B 5 = Sum_B 5 + Tail_B 5
:= by
unfold Tail_B Sum_B Ff Tail_B
simp
ring_nf
simp
theorem sampleSf :
1 + Tail_S 1 = 1 + 2 + Tail_S 2 ∧
1 + 2 + Tail_S 2 = 1 + 2 + 3 + Tail_S 3 ∧
1 + 2 + 3 + Tail_S 3 = 1 + 2 + 3 + 4 + Tail_S 4 ∧
1 + 2 + 3 + 4 + Tail_S 4 = 1 + 2 + 3 + 4 + 5 + Tail_S 5 ∧
1 + 2 + 3 + 4 + 5 + Tail_S 5 = Sum_S 5 + Tail_S 5
:= by
unfold Tail_S Sf Sum_S Tail_B
rw [zpow_mul, zpow_ofNat]
simp
rw [zpow_ofNat, neg_one_sq]
simp
ring_nf
simp
/- This is what causes (Sf n) to have the constant that it does! -/
theorem sampleSminusB :
0 + (Tail_S - Tail_B) 1 = 0 + 4 + (Tail_S - Tail_B) 2 ∧
0 + 4 + (Tail_S - Tail_B) 2 = 0 + 4 + 0 + (Tail_S - Tail_B) 3 ∧
0 + 4 + 0 + (Tail_S - Tail_B) 3 = 0 + 4 + 0 + 8 + (Tail_S - Tail_B) 4 ∧
0 + 4 + 0 + 8 + (Tail_S - Tail_B) 4 = 0 + 4 + 0 + 8 + 0 + (Tail_S - Tail_B) 5 ∧
0 + 4 + 0 + 8 + 0 + (Tail_S - Tail_B) 5 = 0 + 4 + 0 + 8 + 0 + 12 + (Tail_S - Tail_B) 6 ∧
0 + 4 + 0 + 8 + 0 + 12 + (Tail_S - Tail_B) 6 = 4*(Sum_S 3) + (Tail_S - Tail_B) (2*3) ∧
4*(Sum_S 3) + (Tail_S - Tail_B) (2*3) = 4*(Sum_S 3) + 4*(Tail_S 3)
:= by
unfold Tail_S Tail_B Sf Sum_S Tail_B
simp
rw [zpow_ofNat, neg_one_sq]
simp
ring_nf
simp
/- note sum of powers equivalences. -/
theorem sumsOfPowers:
-1/12 = Af (13) ∧
1/4 = Af (-3) ∧
-1/3 = Af (4)
:= by
unfold Af
simp
ring_nf
simp
/-
THE MAIN GOAL
(Sf n) is forced to be -1/12, becaus of (S-B)/4=S.
-/
theorem Sgoal : Sum_S n + Tail_S n = -1/12 := by
unfold Sum_S Tail_S Sf Sum_S Tail_B
simp
rw [even_power_neg_one n]
ring
When I paste in just the Lean code, and ask Claude to comment on it, I get this:
"
This is a fascinating piece of mathematics dealing with the famous divergent series S = 1 + 2 + 3 + 4 + ..., which has a "sum" of -1/12 in certain contexts. Let me break down what I see in this code:
First, you're working with formal power series and their derivatives:
A(x) = 1/(1-x) = 1 + x + x² + x³ + ...
F(x) = A'(x) = 1/(1-x)² = 1 + 2x + 3x² + ...
You introduce several key functions:
B uses F(-1) which gives the alternating series 1 - 2 + 3 - 4 + ...
S represents the series 1 + 2 + 3 + 4 + ...
You're using rational numbers (ℚ) throughout
The proof strategy appears to use the relationship S - B = 4S, which is a key insight for deriving the -1/12 result. This is captured in the justifySf theorem.
The SisConstant and BisConstant theorems show that these values remain unchanged when expanding further terms, which is crucial for treating these divergent series as having "values".
The S_base13 theorem shows another interesting relationship: S = 1 + 13S, which is related to the modular form properties of these series.
The final Sgoal theorem proves that S = -1/12, which matches the famous result used in string theory and zeta function regularization.
This is a formal verification of the -1/12 result using the Lean theorem prover with Mathlib. It's particularly interesting because it provides a rigorous framework for handling what is normally a highly controversial mathematical result. The use of tail terms (Tail_B and Tail_S) is clever as it allows for formal manipulation of these infinite series while maintaining mathematical rigor.
Would you like me to elaborate on any particular aspect of this proof? I find the connection between the formal power series approach and the final result particularly interesting.
"