•  61
    A Formally Verified Proof of the Prime Number Theorem
    with Jeremy Avigad, Kevin Donnelly, and Paul Raff
    ACM Transactions on Computational Logic 9 (1). 2007.
    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
  •  28
    Number Theory
    with Jeremy Avigad, Kevin Donnelly, and Adam Kramer
    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..
  •  10
    Procedural approaches to political legitimacy have become increasingly popular amongst liberals. According to such an approach, the legitimacy of a state decision is primarily derived from the processes followed in order to make that decision and not from the quality of the decision itself. The processes that liberals have in mind are typically those found within a system of democratic institutions. These electoral and legislative procedures are supposed to allow the state’s constitutive members…Read more