We present a survey of algorithms, mostly drawn from the broad field of logic in computer science, that rely on Schanuel's conjecture for termination and/or correctness. Schanuel's conjecture is a central hypothesis in transcendental number theory that generalises many existing classical results such as the Lindemann-Weierstrass theorem and Baker's theorem on linear independence of logarithms of algebraic numbers. The algorithmic use of Schanuel's conjecture was spearheaded by computer algebraists in the 1970s, as well as by Macintyre and Wilkie in the 1990s, most notably to establish the decidability of real arithmetic expanded with the exponential function. Since then, many further applications have been recorded in the literature. We present and discuss several of these algorithms, with a particular focus on the precise role played by Schanuel's conjecture.
Proceedings of the Colloquium on Principles of Formal Quantitative Analysis, 2025. 19 pages.
PDF
© 2025 Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine,
Mihir Vahanwala, and James Worrell.