Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Archimedes' Cattle Problem


view this post on Zulip Email Gateway (Apr 26 2026 at 14:13):

From: Lawrence Paulson <lp15@cam.ac.uk>

I'm happy to announce another impressive contribution from Manuel Eberl: Archimedes' Cattle Problem.

Abstract
In the 3rd century BC, Archimedes challenged the mathematicians of the time with a puzzle that involved computing the size of the cattle herd of the sun god, based on a number of linear equations and other restrictions, which ultimately result in a Pell equation with the gigantic parameter D = 410,286,423,278,424. Since the solution to that Pell equation has 103,266 digits, solving the problem was far beyond the computational capabilities at the time. The first approximate solution was computed by Amthor in 1880, and the exact solution by Williams et al. using electronic computers in 1965.

This article gives a formal description of the problem and proves the general shape of the solutions in terms of the solutions of the Pell equation. It then uses existing machinery from the AFP using continued fractions to explicitly compute the smallest solution, which has 266,454 decimal digits.

https://www.isa-afp.org/entries/Archimedes_Cattle.html


Last updated: May 02 2026 at 13:17 UTC