Finite Analogs of Szemer\'edi's Theorem (2009)
One of the "deepest" theorems in mathematics is Endre Szemer\'edi's theorem about the inevitability of arithmetical progressions. Here we try to nibble at it, by doing "finite" analogs. This is...
Spanning Trees in Grid Graphs (2008)
Building on work by Desjarlais, Molina, Faase, and others, a general method is obtained for counting the number of spanning trees of graphs that are a product of an arbitrary graph and either a path...
A formally verified proof of the prime number theorem (2006)
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
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...
A formally verified proof of the prime number theorem (2005)
Avigad, Jeremy, Donnelly, Kevin, Gray, David, Raff, Paul
The prime number theorem, established by Hadamard and de la Vall'ee Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1 / ln x. Whereas their...
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
A formally verified proof of the