This is a copy of my question on MSE (https://math.stackexchange.com/questions/3372432) because this forum seems better suited for historical questions:
In 1985, Gosper used the not-yet-proven formula by Ramanujan
$$\frac{ 1 }{\pi } = \frac{2\sqrt{2}}{99^2}\cdot \sum_{n=0}^\infty \frac{(4n)!}{(n!)^4}\cdot\frac{26390 n+1103}{396^{4n}}$$
to compute $17\cdot10^6$ digits of $\pi$, at that time a new world record.
Here (https://www.cs.princeton.edu/courses/archive/fall98/cs126/refs/pi-ref.txt) it reads:
There were a few interesting things about Gosper's computation. First, when he decided to use that particular formula, there was no proof that it actually converged to pi! Ramanujan never gave the math behind his work, and the Borweins had not yet been able to prove it, because there was some very heavy math that needed to be worked through. It appears that Ramanujan simply observed the equations were converging to the 1103 in the formula, and then assumed it must actually be 1103. (Ramanujan was not known for rigor in his math, or for providing any proofs or intermediate math in his formulas.) The math of the Borwein's proof was such that after he had computed 10 million digits, and verified them against a known calculation, his computation became part of the proof. Basically it was like, if you have two integers differing by less than one, then they have to be the same integer.
Now my historical question: Who was the first to prove this formula? Was it Gosper because he added the last piece of the proof, or was it the Borweins, afterwards? And was Gosper aware of this proof when he did his computation?