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 only [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]
rw [my_deriv_pow (n+1) x, my_deriv_one_minus_y]
simp
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 only [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]
have hsub : deriv (fun y => 1 - y^(n+1)) x = -(n+1) * x^n := by
rw [my_deriv_sub (fun _ => (1 : ℚ)) (fun y => y^(n+1)) x]
rw [my_deriv_const, my_deriv_pow (n+1) x]
simp
ring_nf
rw [hsub, 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 (n : ℕ) : 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) ∧
(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 →
(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
/- more obviously -/
theorem Proven {n : ℕ} : n*(n+1)/2 + Tail_S n = -1/12 := by
unfold Tail_S Sf Sum_S Tail_B
simp
ring_nf
I heavily edited this proof, completely redoing what Claude did. I wanted to define things in a more intuitive order. This result is finite. It is a real thing. It passes the checker. The difference between the value and the limit are subtle, and correctly handled. The definitions chain back to F, the justification for the choice of B. Goal is the main thing being proven.
Not that it does not mention infinity, or infinite iteration at all. It is a recursive fixed point. It is completely finite, due to the use of this phenomenon:
-- Take the limit for large N if you want. If Tail_X[n] goes to 0, then the series would be called convergent. Here, it is just algebra. It is irrelevant whether or not it converges. If we say that X has some kind of value at all, it will have the same value no matter how many times we do a finite expansion of the Sum_X[n].
The full proof of Goal: