We discuss the formalization, in the Matita Interactive Theorem Prover, of a famous result by Chebyshev concerning the distribution of prime numbers, essentially subsuming, as a corollary, Bertrand's postulate. Even if Chebyshev's result has been later superseded by the stronger prime number theorem, his machinery, and in particular the two functions psi and theta still play a central role in the modern development of number theory. Differently from other recent formalizations of other results innumber theory, our proof is entirely arithmetical. It makes use of most part of the machinary of elementary arithmetics, and in particular of properties of prime numbers, gcd, products and summations, providing a natural benchmark for assessing the actual development of the arithmetical knowleddge base.

A. Asperti, W. Ricciotti (2009). About the Formalization of some Results by Chebyshev in Number Theory [10.1007/978-3-642-02444-3_2].

About the Formalization of some Results by Chebyshev in Number Theory

ASPERTI, ANDREA;RICCIOTTI, WILMER
2009

Abstract

We discuss the formalization, in the Matita Interactive Theorem Prover, of a famous result by Chebyshev concerning the distribution of prime numbers, essentially subsuming, as a corollary, Bertrand's postulate. Even if Chebyshev's result has been later superseded by the stronger prime number theorem, his machinery, and in particular the two functions psi and theta still play a central role in the modern development of number theory. Differently from other recent formalizations of other results innumber theory, our proof is entirely arithmetical. It makes use of most part of the machinary of elementary arithmetics, and in particular of properties of prime numbers, gcd, products and summations, providing a natural benchmark for assessing the actual development of the arithmetical knowleddge base.
2009
19
31
A. Asperti, W. Ricciotti (2009). About the Formalization of some Results by Chebyshev in Number Theory [10.1007/978-3-642-02444-3_2].
A. Asperti; W. Ricciotti
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/75536
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact