I thought this would be the very end of objections to the result. In Lean, the last theorem, was stated like this initially:
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
It is now stated a bit more indirectly that if you multiply it times 12, and add 1, you then get 0.
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.
The closed form
n*(n+1)/2is expansion ofnterms, and prevents us from doing any new parenthesis re-arrange.
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 + ...
This is about self-relations due to recursion.
B is defined from A, by differentiating it and evaluating it
at -1, to get 1 + -2 + 3 + -4 + 5 + -6 + ....
Note that the FINITE sum from 1+2+3+...+n has this relationship
Sum_S (2*n) - Sum_B (2*n) = 4*(Sum_S n)
So, we assign (Sf n) by solving this, where remember
that Sf n = Sum_S n + Tail_S n and Bf n = Sum_B n + Tail_B n
helps to do the solve for Sf n:
Tail_S (2*n) - Tail_B (2*n) = 4*(Tail_B n)
And it happens to be that Sf n cancels out all uses of n, and only -1/12 remains.
All of the other things like explaining the relationship to S = 1 + 13 S is because so many people
doubt this easily reproduceable result.
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
/-
This is a finite proof of -1/12 = 1+2+3+...
I could stop the moment that -1/12 appears, but there is so much resistance to this result in any form, including Lean.
In order for this to be done clearly, use recursion to represent infinite sums.
There is a sense in which you can interpret it like this:
"The resulting number is all 1 digits in base13. It's called -1/12, because if you multiply it times 12,
you get an infinite digit representation of -1. You add 1 to that number, and it ripple-carries to 0."
-/
/-
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)
/- 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)
/- 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)
/- 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 -/
def Ff (x : ℚ):ℚ := 1/((1-x)^2)
-- Complete set of derivative rules we need, written by Claude3.5
-- for some reason, deriv from mathlib is way too hard to use, maybe because of ℚ
axiom my_deriv_pow (n : ℕ) (x : ℚ) : deriv (fun y => y^n) x = n * x^(n-1)
axiom my_deriv_const (c : ℚ) (x : ℚ) : deriv (fun _ => c) x = 0
axiom my_deriv_id (x : ℚ) : deriv (fun y => y) x = 1
axiom my_deriv_sub (f g : ℚ → ℚ) (x : ℚ) : deriv (fun y => f y - g y) x = deriv f x - deriv g x
axiom my_deriv_one_minus_y (x : ℚ) : deriv (fun y => 1 - y) x = -1
axiom my_deriv_div (f g : ℚ → ℚ) (x : ℚ) (h : 1 - x ≠ 0) : deriv (fun y => f y / g y) x = (g x * deriv f x - f x * deriv g x) / (g x)^2
-- show Tail_F x = deriv Tail_A x -- Tail_F is not made up
theorem tail_deriv (n : ℕ) (x : ℚ) (hx : x ≠ 1) :
deriv (fun y => Tail_A y n) x = Tail_F x n := by
simp [Tail_A, Tail_F]
have h1: 1 - x ≠ 0 := by
intro h
rw [sub_eq_zero] at h
exact hx h.symm
rw [my_deriv_div (fun y => y^(n+1)) (fun y => 1-y) x h1]
simp [my_deriv_pow, my_deriv_sub, my_deriv_const, my_deriv_id, my_deriv_one_minus_y]
ring_nf
-- show Sum_F x = deriv Sum_A x -- Sum_F is not made up
theorem sum_deriv (n: ℕ) (x :ℚ) (hx : x ≠ 1) :
deriv (fun y => Sum_A y n) x = Sum_F x n := by
simp [Sum_A, Sum_F]
have h1: 1 - x ≠ 0 := by
intro h
rw [sub_eq_zero] at h
exact hx h.symm
rw [my_deriv_div (fun y => 1 - y^(n+1)) (fun y => 1-y) x h1]
simp [my_deriv_pow, my_deriv_sub, my_deriv_const, my_deriv_id, my_deriv_one_minus_y]
ring_nf
-- show Ff x = deriv Af x -- Ff is not made up
theorem all_deriv (x : ℚ) (hx : x ≠ 1) :
deriv (fun y => Af y) x = Ff x := by
unfold Af Ff
have h1: 1 - x ≠ 0 := by
intro h
rw [sub_eq_zero] at h
exact hx h.symm
rw [my_deriv_div (fun y => 1) (fun y => 1-y) x h1]
simp [my_deriv_const, my_deriv_one_minus_y]
-- 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, shown 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
Sum_F = d[Sum_A x n]/dx
Tail_F = d[Tail_A x n]/dx
B = Ff (-1)
Ff x = deriv (Af x)
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 + 4 + 0 + 8 + 0 + 12 + ...", where it is important that
we keep the expansion at HALF the rate, and not lose it in "+ ..." notation.
Tail_B = Tail_F (-1) = (deriv Tail_A) (-1)
Sum_B = Sum_F (-1) = (deriv Sum_A) (-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
theorem tailb_is_tailf_negone: Tail_B n = Tail_F (-1) n := by
unfold Tail_B Tail_F
simp
ring_nf
/- 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)
/- Justify the definition of (Sf n), is a result of S-B=4*S -/
theorem justifySf:
(Sf n = Sf (n+1)) ∧ -- Sf is a constant
(Bf n = Bf (n+1)) ∧ -- Bf is a constant
(Sf n = Sum_S n + Tail_S n) ∧ -- (Sf n) is sum plus tail
(Sum_S (2*n) - Sum_B (2*n) = 4*Sum_S n) ∧ -- because of this finite sum identity,
(Sf n = (4*Sum_S n - (Sum_S (2*n) + Tail_B (2*n)))/3) -- ... we can show that tails solve for (Sf n)
→ 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
→ (Sf n) - (Bf n) = 4*(Sf n) -- Bf is a constant, as is Sf
)
:= by
unfold Sf Bf Sum_S Tail_B Sum_B Tail_S Ff Sf Sum_S Tail_B
simp
ring_nf
simp
/-
"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
simp
ring_nf
simp
/- This is what causes (Sf n) to have the constant that it does!
The intuition:
4*(1 + 2 + 3 + ...) = 0 + 4 + 0 + 8 + 0 + 12 + ...
The right side expands at half the rate(!) due to zeroes, but 4x larger.
-/
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
ring_nf
simp
-- Another self-similar pattern: (Sf n) = 13^0 + 13^1 + 13^2 + ... + 13^n + 13^(n+1)*(Sf n)
theorem negOneTwelfthRecurrence:
(Sf n) = 1 + 13*(Sf n) := by
unfold Sf Sum_S Tail_B
simp
ring_nf
/- note sum of powers equivalences elsewhere. -/
theorem sumsOfPowers:
-1/12 = Af (13) ∧ -- sum of powers of 13, all 1s in base13
1/4 = Af (-3) ∧ -- sum of powers of (-3), all 1s in base (-3)
-1/3 = Af (4) -- sum of powers of 4, all 1s base 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.
The reason this works is that (Sf n) is a thing such that if you multiply
it times 12, and add 1, a ripple-carry happens to turn that infinite-digit
representation of -1 into 0.
-/
theorem Sgoal : 12*(Sum_S n + Tail_S n) + 1 = 0 := by
unfold Sum_S Tail_S Sf Sum_S Tail_B
simp
ring
