4 found
Order:
  1.  49
    A Formally Verified Proof of the Prime Number Theorem.Jeremy Avigad, Kevin Donnelly, David Gray & Paul Raff - 2007 - ACM Transactions on Computational Logic 9 (1).
    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.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  2.  47
    Formalization of O Notation in Isabelle/HOL.Kevin Donnelly - unknown
    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.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  3.  24
    Number Theory.Jeremy Avigad, Kevin Donnelly, David Gray & Adam Kramer - unknown
    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 . . . . . . . . . . (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  4.  1
    The Other Average Man: Science Workers in Quetelet’s Belgium.Kevin Donnelly - 2014 - History of Science 52 (4):401-428.
    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 (...)
    Direct download  
     
    Export citation  
     
    Bookmark