Lagrange's Theorem for Binary Squares

Parthasarathy Madhusudan, Dirk Nowotka, Aayush Rajasekaran +1

We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange's theo…