Algorytmiczna teoria liczb – do zadań tej teorii zaliczamy przeprowadzanie dowodów własności programów wykonywanych w dziedzinie liczb naturalnych (lub w innych strukturach liczbowych). Rozważane własności to między innymi: własność stopu, poprawność programu względem warunków początkowego i końcowego, równoważność dwu programów.
Na sformalizowaną teorię algorytmiczną składają się: język programów i formuł algorytmicznych rachunek programów inaczej logika algorytmiczna i zbiór aksjomatów specyficznych tej teorii
Początki tej nauki sięgają starożytności, kiedy Euklides podał algorytm obliczania największego wspólnego dzielnika, a Eratostenes – metodę znajdowania liczb pierwszych zwaną sitem Eratostenesa. W czasach nowożytnych pojawiły się między innymi nowe testy pierwszości oraz metody faktoryzacji.
Algorytmiczna teoria liczb naturalnych W 1969 r. podano aksjomat osiągalności. Wykazano, że teoria ta jest kategoryczna, tzn. z dokładnością do izomorfizmu opisuje standardowy model liczb naturalnych. por. [AlgoLog], s. 155.