Sequences of the online encyclopedia of integer sequences

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2024-10-24.
Last modified on 2025-08-09.

This file records formalized sequences of the Online Encyclopedia of Integer Sequences [OEIS].

module literature.oeis where
Imports 
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.function-types

Sequences

The number of groups of order n

OEIS: A000001

open import finite-group-theory.finite-groups using
  ( number-of-groups-of-order)

The Kolakoski sequence

OEIS: A000002

open import elementary-number-theory.kolakoski-sequence using
  ( kolakoski)

The zero sequence

OEIS: A000004

A000004 : ℕ → ℕ
A000004 _ = zero-ℕ

The characteristic function for 0

OEIS: A000007

A000007 : ℕ → ℕ
A000007 zero-ℕ = 1
A000007 (succ-ℕ _) = 0

Euler’s totient function

OEIS: A000010

open import elementary-number-theory.eulers-totient-function using
  ( eulers-totient-function-relatively-prime)

All 1’s sequence

OEIS: A000012

A000012 : ℕ → ℕ
A000012 _ = 1

The positive integers

OEIS: A000027

A000027 : ℕ → ℕ
A000027 = succ-ℕ

The prime numbers

OEIS: A000040

open import elementary-number-theory.infinitude-of-primes using
  ( prime-ℕ)

The Fibonacci sequence

OEIS: A000045

open import elementary-number-theory.fibonacci-sequence using
  ( Fibonacci-ℕ)

Sylvester’s sequence

OEIS: A000058

open import elementary-number-theory.sylvesters-sequence using
  ( sylvesters-sequence-ℕ)

Powers of 2

OEIS: A000079

A000079 : ℕ → ℕ
A000079 = exp-ℕ 2

The Catalan numbers

OEIS: A000108

open import elementary-number-theory.catalan-numbers using
  ( catalan-numbers)

The Bell numbers

OEIS: A000110

open import elementary-number-theory.bell-numbers using
  ( bell-number-ℕ)

Factorials

OEIS: A000142

open import elementary-number-theory.factorials using
  ( factorial-ℕ)

The Fermat numbers

OEIS: A000215

open import elementary-number-theory.fermat-numbers using
  ( fermat-number-ℕ)

Powers of 3

OEIS: A000244

A000244 : ℕ → ℕ
A000244 = exp-ℕ 3

The prime counting function

OEIS: A000720

open import elementary-number-theory.infinitude-of-primes using
  ( prime-counting-ℕ)

The Euclid–Mullin sequence

OEIS: A000945

open import elementary-number-theory.euclid-mullin-sequence using
  ( euclid-mullin-ℕ)

Pisano periods

OEIS: A001175

open import elementary-number-theory.pisano-periods using
  ( pisano-period)

The cofibonacci sequence

OEIS: A001177

open import elementary-number-theory.cofibonacci using
  ( cofibonacci)

The natural numbers

OEIS: A001477

A001477 : ℕ → ℕ
A001477 = id

The number of main classes of Latin squares of order n

OEIS: A003090

open import univalent-combinatorics.main-classes-of-latin-squares using
  ( number-of-main-classes-of-Latin-squares-of-order)

Collatz’ bijection

OEIS: A006369

open import elementary-number-theory.collatz-bijection using
  ( map-collatz-bijection)

The number of semigroups of order n up to isomorphism

OEIS: A027851

open import finite-group-theory.finite-semigroups using
  ( number-of-semigroups-of-order)

The main diagonal of the Ackermann–Péter function

OEIS: A046859

open import elementary-number-theory.ackermann-function using
  ( simplified-ackermann-ℕ)

The number of monoids of order n up to isomorphism

OEIS: A058129

open import finite-group-theory.finite-monoids using
  ( number-of-monoids-of-order)

References

[OEIS]
OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. website. URL: https://oeis.org.

Recent changes