Re: [math-fun] Gosper's EllipticK formula. Status and suggested proof.

Now. I think these formulas should be provable, thus demonstrating the correctness of everything, as follows. You note that y=K(x) and y=K(sqrt(1-x^2)) are the basis solutions of the linear differential equation (EQ 1.3.8 in Borwein book "pi & the AGM")

(x^3 - x) * y'' + (3*x^3-1) * y' + x*y = 0.

--sorry, typo: this diffl equation should read (x^3 - x) * y'' + (3*x^2-1) * y' + x*y = 0.