Verified Real Asymptotics in Isabelle/HOL

by Manuel Eberl

In: Proceedings of ISSAC 2019

SIGSAM Distinguished Student Author Award




Interactive theorem provers (or proof assistants) are software with which mathematical definitions and theorems can be formalised. They assist the user in writing formal proofs and check the correctness of these proofs, typically down to the level of basic logical inference steps. This provides a very high degree of assurance that any proof accepted by them is actually sound. Theorem provers contain varying amounts of tools for automation to assist the user, but unlike computer algebra systems, their focus is not on efficient automatic computation.

In this work, we focus on the particular problem of symbolically determining and proving asymptotics of real-valued functions: limits, ‘Big-O’ statements, and asymptotic expansions. The tool that is presented here uses an approach based on multiseries expansions and can handle functions built from basic arithmetic and standard functions like exp, ln, sin, |ยท|, etc. as well as parameters. The procedure is efficient enough to handle big problems and it is fully automatic in many cases.

Download preprint PDF (626 KiB)


 author = {Eberl, Manuel},
 title = {Verified Real Asymptotics in {I}sabelle/{HOL}},
 booktitle = {Proceedings of the International Symposium on Symbolic and Algebraic Computation},
 series = {ISSAC '19},
 year = {2019},
 isbn = {978-1-4503-6084-5/19/07},
 location = {Beijing, China},
 doi = {10.1145/3326229.3326240},
 publisher = {ACM},
 address = {New York, NY, USA}

Download BibTeX (403 Bytes)