Formalising Continued Fractions (With Applications to Pell's Equation)
by Manuel Eberl
In: Proceedings of CICM 2026 (to appear)
Abstract:
This article presents an Isabelle/HOL formalisation of simple continued fractions with a focus on executable algorithms. In particular, the two-way correspondence between real numbers and continued fractions is established and various important results are proven, e.g. the connection to best rational approximations.
Additional contributions are: the study of periodic continued fractions, efficient computation of the continued fraction for sqrt(D) where D is a positive non-square integer, the continued fraction expansion of Euler's number, and the connection to Pell's equation.
This machinery is then applied to solve Archimedes' cattle problem, which involves solving an instance of Pell's equation where the solution has over 10^5 decimals.
Download preprint PDF (454 KiB)
BibTeX:
@inproceedings{eberl26cfrac,
author = {Manuel Eberl},
title = {Formalising Continued Fractions (With Applications to {P}ell's Equation)},
booktitle = {Proceedings of {CICM} 2026},
series = {CICM '26},
year = {To appear},
sortyear = {2026}
}