The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x. Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erdos in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.

1.1 Some examples of rule induction on permutations . . . . . . . 6 1.2 Ways of making new permutations . . . . . . . . . . . . . . . 7 1.3 Further results . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Removing elements . . . . . . . . . . (...) . . . . . . . . . . . . . . 8.. (shrink)

We are working on formalizing a proof of the prime number theorem using Isabelle/HOL. In support of this project we formalized a very general notion of O notation.

This paper examines the creation of what I have called “The Other Average Man” of nineteenth-century science. This other average man was created during the course of the career of the Belgian polymath Adolphe Quetelet and his development of physique sociale and the controversial l’homme moyen. Rather than discuss Quetelet’s abstract average man, which has received considerable attention, the paper focuses on the real average men that Quetelet imagined would do the work of providing data for physique sociale. To do (...) so, it investigates three moments in Quetelet’s administrative career in Belgium: his early life in Ghent and Brussels during the brief polity of the United Kingdom of the Netherlands, his remarkable transformation of the Académie Royale de Belgique in the 1820s, and an 1846 debate at the Academy on the possible determinism entailed by Quetelet’s statistical account of human behavior. These stories not only point to the creation of another average man in Quetelet’s social physics, but also demonstrate the importance of Belgium’s unique historical context for understanding one of nineteenth-century Europe’s most enduring contributions to the social sciences. (shrink)