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/12

Where 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.

$\frac{n*(n+1)}{2} = \sum_j^{1 \dots n}j = 1 + 2 + 3 + \dots + n$

The closed form n*(n+1)/2 is expansion of n terms, 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