Turán's theorem for triangles, otherwise known as Mantel's theorem, is the statement that the largest number of edges that a triangle-free graph on $n$ vertices can have is $\lfloor n/2\rfloor\lceil n/2\rceil$, with equality attained if and only if the graph is a complete bipartite graph /and the two vertex sets are as close in size as possible.
Here is a sketch of a proof of the result. We shall prove it by induction on $n$. Write $t_3(n)$ for the quantity $\lfloor n/2\rfloor\lceil n/2\rceil$. The theorem is trivial for $n=1$, since a 1-vertex graph has $t_3(1)=0$ edges. In general, if $G$ is an $(n+1)$-vertex graph with $m$ edges and no triangles, then the average degree is $2m/(n+1)$, so one can find a vertex of degree at most $2m/(n+1)$. Removing that vertex gives a graph with at least $m(1-2/(n+1))$ edges and at most $t_3(n)$ edges, by the inductive hypothesis, so we obtain an upper bound for $m$. Some slightly tedious calculation shows that we can obtain an upper bound of $t_3(n+1)$. Furthermore, if we have equality, then the graph we obtain after removing a minimal-degree vertex must have exactly $t_3(n)$ edges (again by a small calculation) so it is a complete bipartite graph with vertex sets of almost equal size or equal size, and then it is easy to see that the best we can do to extend it is to connect the new vertex to all the vertices in one of the vertex classes -- and if they are not of exactly equal size to connect it to the larger one.
However, this post is not about finding that proof, but about a slightly different question. Suppose that instead of being asked to prove the result as just stated, one is simply asked how many edges a triangle-free graph with $n$ vertices can have, and which graphs maximize the number of edges. First of all, it is not altogether clear how to ask this question formally, since it is not enough to prove that there exists a maximal number of edges and a class of graphs that achieves the maximum: we are required to identify the maximal number and the class. In practice that means giving a formula for the maximal number, and a description of all graphs that achieve the maximum. But what constitutes a formula, and what constitutes a description.
As an example of an unsatisfactory answer to the second question, suppose we have written a formula for $t_3(n)$. It would not be all right to say that the class of graphs that achieves the maximum is precisely the class of all triangle-free graphs with $n$ vertices and $t_3(n)$ edges. Somehow we want a description that doesn't trivially imply the property we want it to imply.
Using the analogy of solving equations, which I find repeatedly helpful, it is as though one were asked to find a real number $x$ such that $x^3+8x=51$. If one argued first that $x\mapsto x^3+8x$ is a strictly increasing function that takes both positive and negative values, so there is a unique $x$ such that it equals 51, then that would be correctly showing that such an $x$ existed but it would not be finding one. If on the other hand one points out that $3^3+8\cdot 3=51$, then that certainly would count as a solution.
Typically, to solve equations we simplify them until they reach a particularly basic form and only then allow ourselves a trivial solution. For instance, we might complete the square to turn a quadratic equation into $(x-1)^2=2$, at which point we would allow the trivial solution $x-1=\pm\sqrt 2$, which we would then put into the form $x-1=1\pm\sqrt 2$.
So for us, even if "find" isn't a formally defined mathematical word, and there is no single universally accepted notion of "explicit solution", what we can aspire for the program to do is create a metavariable and then simplify the problem state until it can use a very easy problem, the solution to which is in the library. This raises questions about when the program would recognise that that was the right strategy and when it would try to find a pure existence proof, but that is a topic for another post.
Suppose, then, that we gave the program a problem state looking something like this.
$$ \begin{array} \hline G^\bullet: \text{graph}\\ n: \text{non-negative integer}\\ m^\bullet: \text{non-negative integer}\\ \hline \\ \hline V(G^\bullet)=\{1,2,\dots,n\}\\ |E(G^\bullet)|=m^\bullet\\ G^\bullet\ \text{is triangle free}\\ \forall H:\text{graph}\ V(H)=\{1,2,\dots,n\}\ \wedge\ H\ \text{is triangle free}\implies|E(H)\leq m^\bullet|\\ \hline \end{array} $$
The question now is how a program (possibly directed by a human mathematician) might manipulate a problem state like this in order to obtain a sensible conjecture for what $m^\bullet$ and $G^\bullet$ might be. (More precisely, we would want it to end up specifying properties of $G^\bullet$ that would be easily seen to determine it uniquely up to isomorphism.)
This is considerably more advanced than anything we can do at the moment, so I am not going to continue in tableau form. Instead, I want to discuss a few ways in which a human might come up with the right conjecture, and think about what capabilities a program would need to have to reproduce what the human did.
We know that $G^\bullet$ will have to be maximal such that it contains no triangles. Let us think about how we might prove that $G^\bullet$ contains no triangles. Expanding, we will find ourselves with three distinct vertices and will want to prove that at least two of them are not joined by an edge. Are there any results around that say that for any three objects it must be possible to find two of them that are related in some way? Well, the pigeonhole principle tells us that if $r$ objects are put into $r-1$ pigeonholes, then it must be possible to find two of them that are in the same pigeonhole. That's a pretty good match. It tells us that if we can partition the vertices into two classes and ensure that no two vertices in the same class are joined, then we will have a suitable graph. If we now concentrate on maximizing the number of edges, then first we observe that the proof used nothing about the edges between the two classes, so we might as well put them in. Then we note that if the classes have size $t$ and $n-t$, then the number of edges is $t(n-t)$. And finally, we calculate that this is maximized when $t=\lfloor n/2\rfloor$.
Of course, that is not a proof of Turán's theorem, but what I'm trying to get at here is the process one often goes through of trying to guess what the extremal example might be before proving that it really is the extremal example. (It's important to stress that for many, indeed I'd say most, extremal problems it is not realistic to find an explicit description of the best possible examples, and instead one tries to find good examples and prove that they aren't far from being as good as possible. But for this problem there happens to be a nice exact solution.)
The method here was to do some somewhat speculative backwards library reasoning, which then resulted in a much easier problem. The use of the pigeonhole principle might seem a bit out of the blue, but I think that the match was good enough that it wasn't too much of a "magic" step.
Here's a more systematic approach, but again not one that is guaranteed to give the right example: it is to see what happens if we try to build up an example greedily. That is, we decide we'll add vertices one at a time, at each stage maximizing the number of edges we add. There is no guarantee that being greedy early on won't hurt us later, but we can still see what we get with this approach.
Recall that we are taking the vertices to be $1,2,\dots,n$. So I'll start by picking the vertex 1, which I can't join to anything. Then I'll pick 2, which I can join to 1. Then if I pick 3, I can join it to 1 or 2, but not both, so without loss of generality I'll join it to 1. Now if I join 4 to 1, I won't be able to join it to either 2 or 3, and if I join it to either 2 or 3, I won't be able to join it to 1. So after a little bit of thought I join 4 to 2 and 3. After a couple more steps of this, I find that I am building up a complete bipartite graph, and at each stage I have a complete bipartite graph with two vertex sets with sizes as equal as possible. So I am led to conjecture that that is the extremal example.
The method here was to run a fairly basic algorithm, see what its output was, spot a pattern, generalize it, and conjecture that the resulting generalization was the extremal example. This kind of activity is very common in mathematical problem solving, and clearly a challenge to automate.
Amusingly, this method was suggested to me by ChatGPT. I don't like it as much as the first two methods, but it's not stupid. It was simply to consider some well-known families of graphs and see if any of them look good. Since complete bipartite graphs are a very basic class of graphs, they are likely to come up early on in any such search, so they count as a reasonable guess rather than a wild guess.
One reason I like this method less is that the first two methods generalize without fuss to higher cases of Turán's theorem, whereas this one doesn't so much -- complete $(k-1)$-partite graphs aren't nearly as early in a list of well-known families of graphs as complete bipartite graphs. Also, carefully considered guesswork is better than pure guesswork.
We begin by observing that $G$ contains no triangles if and only if whenever two vertices $x$ and $y$ are joined by a path of length 2, they are not joined by an edge. Now the number of labelled paths of length 2 is equal to $\sum_xd(x)^2-\sum_xd(x)$ (writing $d(x)$ for the degree of $x$ -- the second term here is counting degenerate paths). By Cauchy-Schwarz that is at least $n^{-1}(\sum_xd(x))^2-\sum_xd(x)$, with equality if and only if $G$ is regular of degree $d$ for some $d$. Let's suppose that equality occurs. If $G$ has $m$ edges and no triangles, then $xyz$ is not a labelled path of length 2 if $xz$ is an edge. From this we see that the number of labelled paths of length 2 is at most $d(n(n-1)-dn)=nd(n-1-d)$. From all that we get that $d^2n-dn\leq nd(n-1-d)$, which implies that $d-1\leq n-1-d$, or $d\leq n/2$.
For equality to occur we need $G$ to be regular of degree $n/2$, so for convenience assume that $n$ is even. Now the only way for $x$ and $y$ to be joined is if their neighbourhoods are disjoint, and if they each have a neighbourhood of size $n/2$ that implies that the neighbourhood of $x$ is the complement of the neighbourhood of $y$. So if $xy$ is an edge, then every $z$ joined to $x$ must have neighbourhood equal to the neighbourhood of $y$, and every $z$ joined to $y$ must have neighbourhood equal to the neighbourhood of $x$. Thus $G$ is the complete bipartite graph with vertex sets of equal sizes. It is now reasonable to conjecture that if $n$ is odd, then the maximal graph will be as similar to this as possible.
It would take some work to analyse what strategies I was using there, but in very general terms I was exploring some consequences of $G$ being triangle free. I also guessed that an inequality I proved would, for a graph with the maximal number of edges, be sharp. (In due course that guess was vindicated, but at the time I made it it was conceivable that by making a sacrifice there I would end up gaining later.)
As with many such questions, the answer depends on what we whether we are looking for a proof that can be generated by a human-operated point-and-click system (that is, a "motivated proof") or one that can be fully automatically generated. The first method seems the closest to the kinds of methods we are thinking about at the moment -- it requires some abstraction, library search, and backwards reasoning. The second would require a whole subproject to be undertaken -- one where we produce an algorithm that experiments with small examples, spots patterns, and generalizes. However, there is a lot to be said for such a subproject, given that these are clearly activities that help with a lot of problems. The third method should be easy to implement, but it is not all that powerful or robust -- if it works, great, but very often it won't. And the fourth method isn't all that well specified, though it might be a useful exercise to try to do so.