@inproceedings{e2ac07fc75ba42b385c02c8dc520da8a,
title = "Lagrange{\textquoteright}s theorem for binary squares",
abstract = "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{\textquoteright}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.",
keywords = "Additive number theory, Binary square, Decidable theory, Decision procedure, Finite automaton, Theorem-proving",
author = "P. Madhusudan and Dirk Nowotka and Aayush Rajasekaran and Jeffrey Shallit",
note = "This material is based upon work supported by the National Science Foundation under Grant No. 1527395.; 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018 ; Conference date: 27-08-2018 Through 31-08-2018",
year = "2018",
month = aug,
day = "1",
doi = "10.4230/LIPIcs.MFCS.2018.18",
language = "English (US)",
isbn = "9783959770866",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Igor Potapov and James Worrell and Paul Spirakis",
booktitle = "43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018",
}