Essentially what we need to do is find a lower bound on the sum:
$$
\sum_{i=1}^{n}\sum_{j=1}^{n}\operatorname{gcd}(i,j) \tag{1}
$$
This is the total of the entries in the $n\times n$ table of GCD's. We can compute this sum more efficiently by noting that the GCD is commutative, so the table is symmetric about its diagonal. Therefore, the sum (1) is equal to twice the sum of the lower triangular part, minus the sum of the diagonal entries (which would otherwise be counted twice):
$$
\sum_{i=1}^{n}\sum_{j=1}^{n}\operatorname{gcd}(i,j) = 2\sum_{i=1}^{n}\sum_{j=1}^{i}\operatorname{gcd}(i,j) - \sum_{i=1}^{n}\operatorname{gcd}(i,i) \tag{2}
$$
We can start simplifying this with the identity:
$$
\operatorname{gcd}(i,i)=i
$$
Which is true for all nonnegative integers $i$. This turns the last part of (2) into the well-known:
$$
\sum_{i=1}^{n}i=\frac{n(n+1)}{2} \tag{3}
$$
Now we will tackle the sum:
$$
\sum_{j=1}^{i}\operatorname{gcd}(i,j) \tag{4}
$$
For any two integers $i$ and $j$, if we know that:
$$
\operatorname{gcd}(i,j)=d
$$
Then, by the definition of the GCD, we know that there exists a unique pair of coprime integers $a$ and $b$ such that:
$$
\begin{align}
i &= ad \\
j &= bd
\end{align}
$$
Now in the sum (4) we have $0<j\le i$. This means that $0<bd\le ad$, and for positive $d$, $0<b\le a$. Now for a given value of $a$, the number of integers $b$ satisfying these two conditions ($0<b\le a$ and $b$ is coprime to $a$) is defined as $\varphi(a)$, the Euler totient function.
For given values of $i$ and $d$, $a$ is fixed, and therefore $\varphi(a)$ is also the number of values of $j$ that yield $\operatorname{gcd}(i,j)=d$. This means that for every value of $d$ that appears in (4), the number of times it appears is $\varphi(i/d)$, allowing us to rearrange the sum:
$$
\sum_{j=1}^{i}\operatorname{gcd}(i,j)=\sum_{d|i}d\cdot\varphi\left(\frac{i}{d}\right)
$$
Where the notation $\sum_{d|i}$ means the sum over all $d$ that divide $i$.
Our final trick is to reverse the order of the sum. For every divisor $d$, $i/d$ is also a divisor, allowing us to switch the two:
$$
\sum_{d|i}d\cdot\varphi\left(\frac{i}{d}\right)=\sum_{d|i}\varphi(d)\left(\frac{i}{d}\right) \tag{5}
$$
Now we can work on the outer part of the sum from (2). We can use (5) to rewrite the inner part:
$$
\sum_{i=1}^{n}\sum_{j=1}^{i}\operatorname{gcd}(i,j) =\sum_{i=1}^{n}\sum_{d|i}\varphi(d)\left(\frac{i}{d}\right) \tag{6}
$$
Now for a given value of $d$, the integers $i$ for which $d$ are a divisor are $d,2d,3d,\ldots,kd$. The largest $k$ such that $kd\le n$ is $\lfloor n/d\rfloor$. This allows us to change the order of the sums for $i$ and $d$:
$$
\sum_{i=1}^{n}\sum_{d|i}\varphi(d)\left(\frac{i}{d}\right) = \sum_{d=1}^{n}\sum_{k=1}^{\lfloor n/d\rfloor}\varphi(d)\left(\frac{kd}{d}\right)
$$
Moving $\varphi(d)$ out of the inner sum and canceling the factors of $d$ gives us:
$$
\sum_{d=1}^{n}\sum_{k=1}^{\lfloor n/d\rfloor}\varphi(d)\left(\frac{kd}{d}\right) = \sum_{d=1}^{n}\varphi(d)\sum_{k=1}^{\lfloor n/d\rfloor}k
$$
The inner sum simplifies to just:
$$
\sum_{d=1}^{n}\varphi(d)\sum_{k=1}^{\lfloor n/d\rfloor}k = \sum_{d=1}^{n}\varphi(d)\frac{1}{2}\left\lfloor\frac{n}{d}\right\rfloor\left(\left\lfloor\frac{n}{d}\right\rfloor+1\right) \tag{7}
$$
Now we can substitute (3) and (7) into (2), giving us an expression for the sum of the entire table:
$$
\sum_{i=1}^{n}\sum_{j=1}^{n}\operatorname{gcd}(i,j) = \sum_{d=1}^{n}\varphi(d)\left\lfloor\frac{n}{d}\right\rfloor\left(\left\lfloor\frac{n}{d}\right\rfloor+1\right) - \frac{n(n+1)}{2} \tag{8}
$$
We can obtain a lower bound on (8) by replacing $\lfloor n/d\rfloor \to n/d-1$:
$$
\sum_{d=1}^{n}\varphi(d)\left(\frac{n^2}{d^2}-\frac{n}{d}\right) - \frac{n^2}{2}-\frac{n}{2} = \left[\sum_{d=1}^{n}\frac{\varphi(d)}{d^2}-\frac{1}{2}\right]n^2 - \left[\sum_{d=1}^{n}\frac{\varphi(d)}{d}+\frac{1}{2}\right]n \tag{9}
$$
We are only interested in values of $n$ above $700$. Therefore, we can take the first $700$ terms of sum (8)—which are always present when $n\ge 700$—and drop the remaining terms. Since all the terms in (8) are positive, this is a lower bound on the true value of the sum. Dropping the corresponding terms in (9) lets us obtain our final lower bound:
$$
(4.1801349420713611\ldots)n^2-(426.1576422933951583\ldots)n \tag{10}
$$
This lower bound doesn't actually exceed $4n^2$ until $n\ge 2366$, so we need to check all the sums from $700\le n\le 2365$. We can do this quickly using the untruncated sum (8).
If we do this, we find that Professor Halfbrain's theorem is:
correct.
Inspired by the paper:
Olivier Bordellès. "The Composition of the gcd and Certain
Arithmetic Functions." Journal of Integer Sequences, Vol. 13 (2010)
