Lagrange's Theorem for Binary Squares

Authors P. Madhusudan , Dirk Nowotka , Aayush Rajasekaran, Jeffrey Shallit

Thumbnail PDF


  • Filesize: 448 kB
  • 14 pages

Document Identifiers

Author Details

P. Madhusudan
  • Department of Computer Science, Thomas M. Siebel Center for Computer Science, 201 North Goodwin Avenue, Urbana, IL 61801-2302, USA
Dirk Nowotka
  • Department of Computer Science, Kiel University, D-24098 Kiel, Germany
Aayush Rajasekaran
  • School of Computer Science, University of Waterloo, Waterloo, ON N2L 3G1, Canada
Jeffrey Shallit
  • School of Computer Science, University of Waterloo, Waterloo, ON N2L 3G1, Canada

Cite AsGet BibTex

P. Madhusudan, Dirk Nowotka, Aayush Rajasekaran, and Jeffrey Shallit. Lagrange's Theorem for Binary Squares. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


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 theorem: every natural number > 686 is the sum of at most 4 natural numbers whose canonical base-2 representation is a binary square, that is, a string of the form xx for some block of bits x. Here the number 4 is optimal. While we cannot embed this theorem itself in a decidable theory, we show that stronger lemmas that imply the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Constructive mathematics
  • Mathematics of computing → Discrete mathematics
  • binary square
  • theorem-proving
  • finite automaton
  • decision procedure
  • decidable theory
  • additive number theory


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. W. D. Banks. Every natural number is the sum of forty-nine palindromes. INTEGERS - Electronic J. Combinat. Number Theory, 16, 2016. #A3. Google Scholar
  2. J. Cilleruelo, F. Luca, and L. Baxter. Every positive integer is a sum of three palindromes. Math. Comp., 2017. Published electronically at URL:
  3. R. C. Crocker. On the sum of two squares and two powers of k. Colloq. Math., 112:235-267, 2008. Google Scholar
  4. W. J. Ellison. Waring’s problem. Amer. Math. Monthly, 78:10-36, 1971. Google Scholar
  5. E. Grosswald. Representations of Integers as Sums of Squares. Springer-Verlag, 1985. Google Scholar
  6. M. Heizmann, D. Dietsch, M. Greitschus, J. Leike, B. Musa, C. Schätzle, and A. Podelski. Ultimate automizer with two-track proofs. In M. Chechik and J.-F. Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, volume 9636 of Lecture Notes in Computer Science, pages 950-953. Springer-Verlag, 2016. Google Scholar
  7. M. Heizmann, J. Hoenicke, and A. Podelski. Software model checking for people who love automata. In N. Sharygina and H. Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, volume 8044 of Lecture Notes in Computer Science, pages 36-52. Springer-Verlag, 2013. Google Scholar
  8. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979. Google Scholar
  9. D. M. Kane, C. Sanna, and J. Shallit. Waring’s theorem for binary powers. Preprint, available at, 2018.
  10. J.-L. Lagrange. Démonstration d'un théoréme d'arithmétique. Nouv. Mém. Acad. Roy. Sc. de Berlin, pages 123-133, 1770. Also in Oeuvres de Lagrange, 3 (1869), pp. 189-201. Google Scholar
  11. C. J. Moreno and S. S. Wagstaff, Jr. Sums of Squares of Integers. Chapman and Hall/CRC, 2005. Google Scholar
  12. M. B. Nathanson. Additive Number Theory: The Classical Bases. Springer-Verlag, 1996. Google Scholar
  13. M. B. Nathanson. Elementary Methods in Number Theory. Springer-Verlag, 2000. Google Scholar
  14. D. Platt and T. Trudgian. On the sum of two squares and at most two powers of 2. Preprint, available at, 2016.
  15. A. Rajasekaran. Using automata theory to solve problems in additive number theory. Master’s thesis, School of Computer Science, University of Waterloo, 2018. Google Scholar
  16. A. Rajasekaran, J. Shallit, and T. Smith. Sums of palindromes: an approach via nested-word automata. Preprint, available at, 2017.
  17. A. Rajasekaran, J. Shallit, and T. Smith. Sums of palindromes: an approach via automata. In R. Niedermeier and B. Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018), Leibniz International Proceedings in Informatics, pages 54:1-54:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  18. N. J. A. Sloane. The on-line encyclopedia of integer sequences. Available at, 2016.
  19. C. Small. Waring’s problem. Math. Mag., 50:12-16, 1977. Google Scholar
  20. R. C. Vaughan. The Hardy–Littlewood Method, volume 125 of Cambridge Tracts in Mathematics. Cambridge University Press, 2nd edition, 1997. Google Scholar
  21. R. C. Vaughan and T. Wooley. Waring’s problem: a survey. In M. A. Bennett, B. C. Berndt, N. Boston, H. G. Diamond, A. J. Hildebrand, and W. Philipp, editors, Number Theory for the Millennium. III, pages 301-340. A. K. Peters, 2002. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail