How to translate mathematical intuition into a rigorous proof?

I've seen a lot of questions about how to develop mathematical intuition, but often I have the opposite problem.

Several times I have run into a situation where I want to solve a math problem, and I play around with it until my intuition reaches the point where I have a good idea of how the complete proof might be structured. But then when it comes to actually write out the proof, I have trouble translating this intuition into a rigorous proof. I want to give the following example, from this PDF of Putnam training problems.

1.13. Prove that for every $n\ge 2$, the expansion of $(1+x+x^2)^n$ contains at least one even coefficient.

When first thinking about this problem, I wanted to look at the polynomials $\pmod{2}$ so that "even coefficient" is simplified to "zero coefficient."

Then from doing a few computations, I notice a pattern.

\begin{align*} (1+x+x^2)^2&=(1+x+x^2)+x(1+x+x^2)+x^2(1+x+x^2)\\ &=1+x+x^2\\ &+x+x^2+x^3\\ &+x^2+x^3+x^4\\ &=1+x^2+x^4 \end{align*}

I notice that multiplying a polynomial by $(1+x+x^2)$ is like adding that polynomial with itself three times, each shifted over. The $x$ shifts it over by one place and the $x^2$ shifts it over by two places.

Continuing this pattern, we can get the coefficients of $(1+x+x^2)^3$ as follows:

\begin{array}{ccccccc} 1&0&1&0&1&&\\ &1&0&1&0&1&\\ &&1&0&1&0&1\\ \hline 1&1&0&1&0&1&1 \end{array}

So $(1+x+x^2)^3\equiv 1+x+x^3+x^5+x^6 \pmod{2}$

Let's make a triangle of a few more results:

\begin{array}{cccccccccccc} 0:&&&&&&1&&&&&\\ 1:&&&&&1&1&1&&&&\\ 2:&&&&1&0&1&0&1&&&\\ 3:&&&1&1&0&1&0&1&1&&\\ 4:&&1&0&0&0&1&0&0&0&1&\\ 5:&1&1&1&0&1&1&1&0&1&1&1\\ \end{array}

We see that the structure of our problem is essentially the same as an elementary cellular automaton (specifically, rule 150). I will come back to this later.

I notice another peculiar pattern with the $1$st, $2$nd, and $4$th rows: There are only $1$s on the ends and in the center. Perhaps this pattern continues for all powers of $2$. And it does, which is not hard to prove with induction.

Claim: $\forall n\ge 0,\ (1+x+x^2)^{2^n}\equiv 1+x^{2^n}+x^{2^{n+1}}\pmod{2}$

Base case: $(1+x+x^2)^{2^0}\equiv 1+x+x^2\equiv 1+x^{2^0}+x^{2^1}\pmod{2}$

Inductive Step:

\begin{align*} (1+x+x^2)^{2^n}&\equiv ((1+x+x^2)^{2^{n-1}})^2\\ &\equiv (1+x^{2^{n-1}}+x^{2^n})^2\\ &\equiv 1+x^{2^n}+x^{2^{n+1}}\pmod{2} \end{align*}

This is where the intuition comes in that is hard for me to express rigorously. On one of the $2^n$th rows, look at the $0$ equidistant from the leftmost $1$ and the $1$ in the center. If the rightmost $1$ wasn't there, then that $0$ would stay a $0$ forever because of symmetry: any effect from the left is cancelled by an effect from the right.

However, the rightmost $1$ does exist, so it will eventually change that $0$. But since effects are local in this automaton, it will require over $2^n$ more rows until the rightmost $1$ affects the $0$ we are looking at (there are over $2^n$ spaces between them). In other words, we have shown that the $0$ will stay a $0$ for all rows up to the $2^{n+1}$th row. Applying this logic on each power of two row, we show that there is always a zero coefficient from row $2$ onwards.

Is there a more rigorous way I can express those last two paragraphs? And in general, what advice do you have for translating intuition to a rigorous proof?

• In your example you changed the question. Originally it asked for a $0$ in every row. Your version only talks about rows of the form $2^n$, but you show a very special form for those rows. Your induction is fine and proves what you wanted to prove, but it is not the original question. It might be a step along the way I can imagine (but I am speculating) that you can show a partial row starting with $1$, a bunch of $0$s and a $1$ will always have a $0$ somewhere. If you can do that you are done in conjunction with what you have done. – Ross Millikan Jun 25 '18 at 4:15
• @RossMillikan I did not change the question in any way. The observation I made about the $2^n$ rows was a stepping stone in my proof. Look at the last three paragraphs. – Riley Jun 25 '18 at 4:18
• You said you would come back to rule 150 but I don't think you did – Mark Jun 25 '18 at 4:49
• @Mark I meant that I will come back to framing the problem in terms of cellular automata, which I did when discussing the "effects" of the $1$s, and the locality of the automaton. – Riley Jun 25 '18 at 4:51
• [Just a comment as the question is about the automaton-intuition being turned into a proof.] Another way of thinking about this expression is, the coefficient of $x^m$ in the expansion shows the number of ways to achieve a total of $m$ by rolling a die with sides $0, 1, 2$ a total of $n$ times. To see why, try making a three by three times table model to see the result of squaring the expression; then, erase the base of $x$. – Benjamin Dickman Jun 25 '18 at 5:17

You have proved that these binary strings are symmetric so it suffices to prove the result for only the "half-strings." Imagine cutting your triangle down the middle. Let $x_n$ be the $n^{th}$ bit string, which is length $n+1$.

We have $x_0 = 1$, $x_1 = 11$, $x_2 = 101$, etc.

Now you can address the $j^{th}$ bit inside $x_n$ as $x_{n,j}$.

This addressing system will make it easier to talk more concretely about the action of the automaton.

You can pin down a definition of "locality of action" by saying that there is some function $f(a, b, c)$ such that $\forall n, j: x_{n,j} = f(x_{n-1, j-1}, x_{n-1,j}, x_{n-1,j+1})$ (with some additional nuisance conditions about the boundary). This means that the $j^{th}$ bit in the current string can be computed by neary-by bits in the previous string. Here $f$ represents the action of this rule 150 you mention.

Now use $f$ again to show $x_{n,j} = f(f(x_{n-2, j-2}, x_{n-2,j-1}, x_{n-2, j}), f(x_{n-2, j-1}, x_{n-2,j}, x_{n-2, j+1}), f(x_{n-2, j}, x_{n-2,j+1}, x_{n-2, j+2}))$

Now you can see when we repeat this procedure $k$ times we will end up with a trinary abstract syntax tree depth $k$. To avoid having to talk about the exact structure of the expression at the $k^{th}$ level, we can reason about this substitution process purely formally as a process operating on the (countably infinite) set of symbols $\{ \underline{f}, \underline{(}, \underline{)} \} \cup \{ \underline{x_{i,j}} \}_{(i,j) \in \mathbb{N}^2}$ (here the commas are not meant to be part of the symbol set, they are just there to separate symbols from each other). You can prove by induction, that for any $k$, that $x_{n,j}$ is computed by an expression using the symbols $\{ \underline{f}, \underline{(}, \underline{)} \} \cup \{\underline{ x_{n-k, j-k}},\underline{ x_{n-k, j-k+1}}, …,\underline{ x_{n-k, j+k-1}},\underline{ x_{n-k, j+k} }\}$ (the $2k+1$ bits in the $(n-k)^{th}$ string centered on the $j^{th}$ bit) intermixed with function applications of $f$.

Fix $n$ and let $k_n$ be the distance to the previous power of $2$. (So if $n=13$, $k_n=5$ since the previous power of $2$ is $8$). And define $j_n \equiv (n-k_n)/2$. This is the index of the central bit of the $(n-k_n)^{th}$ bit string.

You have demonstrated that those bits at indices $\{ (n-k_n, m) \}_{1 \le m \lt n }$ are all zero since $n-k_n$ is a power of $2$. So any well-formed expression using only the symbols $\{ \underline {f}, \underline{(}, \underline{)}\} \cup \{ \underline{x_{n-k_n, j_n-k_n}}, \underline{x_{n-k_n, j_n-k_n+1}}, …,\underline{x_{n-k_n, j_n+k_n-1}}, \underline{x_{n-k_n, j_n+k_n}}\}$ will evaluate to zero by $f(0,0,0) = 0$, and in particular the expression representing $x_{n,j_n}$ (created from the $k_n$ iterations of the formal symbol substitution procedure) evaluates to $0$.

So as $n$ increments, $x_{n,j_n}$ traces out the path of the central bits you were referring to, all of which are zero.

General thoughts about formalization: There are certain technical devices which are work horses of the formalization process. Two of them I have used in this proof:

• indexing time and space, with a numeric coordinate system
• encoding a time evolving system as function application

A third device which I used is not as common, and comes from computer science and logic:

Something that I have been realizing is that these devices are not obvious (at least to me). Humanity was around for a long time before the Cartesian coordinate system was discovered and used to formalize geometrical intuition. It took even longer to develop the idea that almost every mathematical object could be encoded as an intricate tower of sets (ZFC).

I guess for me it's a matter of building up a library of these devices and binding them to the correct intuitions by repeated use.

In certain areas like computer programming, there are very few tools for converting intuition into proof. There were a couple of very good devices created like

• loop invariants
• Hoare logic

but multithreaded and heap-allocating programs are still an active area of research.

• By the way, I have not verified the claim about the sequence actually evolving as the cellular automata $f$ but I'm trusting it's true. – Mark Jun 25 '18 at 7:01
• I think your definition of $j$ doesn't quite match the way you use it. You're using it as if $j$ represents the $x$ coordinate in the triangle rather than the $j$th bit. Also I think you need to consider whole strings instead of half strings for the automation to work. And I think you need to define $x_{n,j}=0$ when $j$ is out of bounds. Otherwise a great answer. – Riley Jun 25 '18 at 12:50
• Yeah, for it to make sense, we need to start counting things at $0$ as we do in computer programs. $x_{n,j} \cong x[n][j]$. As for the whole strings vs half strings, maybe it will be convenient to use negative indices to talk about the left half of the triangle. – Mark Jun 25 '18 at 14:48

Here is one answer to the question. If $$\, n\ge 2\,$$ then the first $$4$$ entries in each row, namely, $$\, 1 0 1 0, 1 1 0 1, 1 0 0 0, 1 1 1 0, \dots, \,$$ repeat in a period of $$4$$. There is a $$0$$ in each of these first $$4$$ entries. This was not the proof you wanted because it is too simple.

Your proof is essentially the following. You noticed something about a $$0$$ in row $$\, 2^n \,$$ and that this $$0$$ continues up to the row $$\, 2^{n+1}. \,$$ We formalize that observation by working with polynomials over the field with two elements. Define the Laurent polynomials $$\, y(n) := x^n + x^{-n} \,$$ and since the characteristic of the field is $$2$$, $$\, y(0) = 1 + 1 = 0. \,$$ Using simple algebra of exponents we get that $$\, y(n)y(m) = y(n+m) + y(n-m), \,$$ and the special cases $$\, y(n)^2 = y(2n) \,$$ and $$\, y(2^n) = y(1)^{2^n}.$$

Define the row polynomials $$\, r(m) := (1 + y(1))^m. \,$$ The general row is $$\, r(m) = r(2^n+k) \,$$ where $$\, 0\le k < 2^n. \,$$ Notice that $$\, r(2^n) = 1 + y(1)^{2^n} = 1 + y(2^n). \,$$ Also $$\, r(m) = 1 + \sum_{i=1}^m c_i y(i), \,$$ where $$\, c_i \,$$ is the coefficient of $$\, y(i). \,$$ You noticed that $$\, c_{2^{n-1}} = 0 \,$$ but how to prove it? We calculate that $$\, r(m) = (1 \!+\! y(2^n)) r(k) = (1 \!+\! y(2^n))(1 \!+\! cy(2^{n-1}) \!+\! t) = (1 \!+\! y(2^n))(1 \!+\! t) \!+\! c y(3\,2^{n-1}) \,$$ where $$\, t \,$$ is all the terms with $$\, y(i), \,$$ and $$\, i\ne 2^{n-1}, \,i < 2^n. \,$$ But $$\, y(2^n)y(i) = y(2^n-i) \!+\! y(2^n+i) \,$$ and since $$\, i \ne 2^{n-1} \,$$ we get no $$\, y(2^{n-1}) \,$$ terms in the product $$\, (1 \!+\! y(2^n))(1 \!+\! t). \,$$ That proves it.

This answers your particular question, but what about intuition versus rigor? I think there are no good answer to that question. You have to always look for any patterns or regularities and simple or edge cases. You have to be lucky and it helps to have a lot of background experience to draw upon.

• I recognize that there is a simpler answer to the question. It is given in the PDF I liked to. I am not asking for the solution, I am asking about how to translate my ideas into a rigorous proof. – Riley Jun 25 '18 at 4:06
• I thought I was translating your ideas combined with ideas of my own into a proof. But intuitions are tricky to express clearly. Maybe you wanted an "automaton theoretic" proof? – Somos Dec 3 '18 at 19:55