Technical reports

Formalizing basic number theory

Thomas Marthedal Rasmussen

September 2000, 20 pages

DOI: 10.48456/tr-502

Abstract

This document describes a formalization of basic number theory including two theorems of Fermat and Wilson.

Most of this has (in some context) been formalized before but we present a new generalized approach for handling some central parts, based on concepts which seem closer to the original mathematical intuition and likely to be useful in other (similar) developments.

Our formulation has been mechanized in the Isabelle/HOL system.

Full text

PDF (1.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-502,
  author =	 {Rasmussen, Thomas Marthedal},
  title = 	 {{Formalizing basic number theory}},
  year = 	 2000,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-502.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-502},
  number = 	 {UCAM-CL-TR-502}
}