Computation

Computation is the execution of a finite sequence of well-defined operations in order to produce a result. In mathematics, the term refers both to the practical carrying out of algorithms and to the abstract study of what can be computed, by what means, and with what resources.

The modern study of computation lies at the intersection of mathematics, logic, and computer science. It includes formal models of algorithms, the limits of computability, the analysis of time and memory requirements, and the use of computers in mathematical research. Computation also plays an important role in practice, where large-scale search, symbolic manipulation, numerical methods, and formal verification are used to investigate conjectures and certify proofs.

Theory

Models of computation

A central aim of the theory of computation is to describe algorithms in a mathematically precise way. Several formal models are used for this purpose.

A Turing machine, introduced by Alan Turing in 1936, is the standard abstract model of general computation. It consists of an infinite tape, a read/write head, and a finite set of states governed by a transition function. Despite its simplicity, a Turing machine can simulate any algorithm that is ordinarily regarded as effective. It therefore serves as the benchmark against which other notions of computability are measured.

A system or language that can simulate an arbitrary Turing machine is called Turing complete. Many systems not originally designed for general-purpose computation turn out to be Turing complete, including Conway's Game of Life, CSS with user interaction, and Magic: The Gathering.

A finite-state machine is a weaker model of computation: it has only finitely many states and no unbounded external memory. Finite-state machines recognise exactly the regular languages and are fundamental in automata theory, compiler construction, network protocols, and digital circuit design. Related models include the pushdown automaton and the wider Chomsky hierarchy of formal languages.

Another foundational model is the lambda calculus, which describes computation in terms of function abstraction and application rather than machine states and tape symbols. It is equivalent in power to Turing machines and plays a central role in logic, type theory, and the semantics of programming languages.

Computability and its limits

Once computation is formalised, one can ask which problems are solvable in principle. This leads to computability theory, which studies decidable and undecidable problems.

The central negative result is the halting problem: there is no general algorithm that determines, for every program and input, whether the program eventually halts. This shows that there are well-posed mathematical questions that no algorithm can answer in complete generality.

A classical illustration is the Busy Beaver function, usually written BB(n), which asks for the maximum number of 1s that can be printed by any halting n-state Turing machine on a blank tape. The function is uncomputable and grows faster than any computable function. Its exact values are known only for small n.

Known values of BB(n)
n	BB(n)	Year determined
1	1	1962
2	4	1962
3	6	1965
4	13	1983
5	4098	2024
6	at least 10^^15	lower bound

The determination of BB(5) in 2024 was itself a notable feat of large-scale computation and formal verification. For n greater than or equal to 6, only lower bounds are known, and the values quickly exceed most familiar systems of notation.

See also Uncomputability and Hypercomputation.

Complexity

Even when a problem is computable, it may still be infeasible in practice. Computational complexity theory studies the resources required to solve problems, especially time and memory, as functions of input size.

This leads to complexity classes such as P, NP, and many others. A major theme of theoretical computer science is to determine which problems admit efficient algorithms and which appear to require exponential or worse resources.

A central open problem is whether P equals NP. Informally, the question asks whether every problem whose proposed solutions can be verified efficiently can also be solved efficiently. It is one of the Millennium Prize Problems and has major consequences for optimisation, cryptography, logic, and algorithm design.

Mathematical practice

Computation is not only a subject of study but also a method of doing mathematics. It is used to test conjectures, search large finite spaces, generate data, verify exceptional cases, and check formal proofs.

Computer-assisted mathematics takes several forms, including experimental computation, exhaustive search, symbolic and numerical computation, distributed computation, and formal verification. In some theorems the computer plays an auxiliary role; in others, the computation is an essential part of the proof.

Examples in mathematics

Computation has entered mathematics in several distinct ways.

Four Colour Theorem: The Four Colour Theorem is the classic example of computer-assisted proof. In 1976, Kenneth Appel and Wolfgang Haken showed that every planar map can be coloured with four colours by combining a general mathematical argument with a large computer check of 1,936 unavoidable configurations. Its importance for computation lies not only in the theorem itself, but in the way it established exhaustive machine case-analysis as a legitimate mathematical method. The proof was later simplified by Robertson, Sanders, Seymour, and Thomas in 1997, and formally verified in Coq by Georges Gonthier in 2005.

God's number: For the Rubik's Cube, God's number is the minimum number of moves sufficient to solve any position in the half-turn metric. In 2010, Tomas Rokicki, Herbert Kociemba, Morley Davidson, and John Dethridge proved that God's number is 20. Here computation entered as large-scale search through an enormous state space: all 43,252,003,274,489,856,000 positions were handled by symmetry reduction, decomposition into roughly 55.88 billion cosets, and about 35 CPU-years of donated time on Google's infrastructure.

GIMPS and Mersenne primes: The Great Internet Mersenne Prime Search (GIMPS), founded in 1996, illustrates distributed computation in number theory. It searches for primes of the form 2^p - 1 using the Lucas-Lehmer test, with volunteers donating CPU and GPU time. GIMPS has discovered the last 18 known Mersenne primes. The current record is the 52nd known Mersenne prime,; 2^136,279,841 - 1,; discovered on 12 October 2024 by Luke Durant. It has 41,024,320 decimal digits, more than 16 million digits larger than the previous record, and was the first record Mersenne prime found using GPUs, specifically NVIDIA A100 and H100 instances across 24 data centres in 17 countries. By a theorem known to Euclid, every Mersenne prime gives rise to an even perfect number of the form 2^p-1(2^p - 1). It remains unknown whether any odd perfect numbers exist.

Boolean Pythagorean triples problem: This problem illustrates the use of SAT solving, in which a mathematical question is translated into a large Boolean satisfiability instance. In 2016, Marijn Heule, Oliver Kullmann, and Victor Marek showed that the positive integers can be coloured red and blue with no monochromatic Pythagorean triple up to 7,824, but not up to 7,825. The resulting proof certificate was 200 terabytes in size, making it at the time the largest mathematical proof ever produced.

Formal verification: Formal verification represents a different use of computation again. Here the computer is not primarily searching for a result, but checking that every logical step of a proof is valid. A growing number of major theorems have been formally verified in proof assistants such as Coq, Isabelle, HOL Light, and Lean.

Selected formally verified theorems
Theorem	Proof assistant	Year
Four Colour Theorem	Coq	2005
Prime number theorem	Isabelle	2005
Feit-Thompson theorem	Coq	2012
Kepler Conjecture (Flyspeck)	HOL Light and Isabelle	2014
Sphere packing in dimension 8	Lean	2026

In February 2026, Maryna Viazovska's proof that the E₈ lattice gives the densest sphere packing in 8 dimensions was formally verified in Lean, with assistance from the AI auto-formalisation agent Gauss developed by Math, Inc. The 24-dimensional case for the Leech lattice followed two weeks later, with the two projects together amounting to more than 200,000 lines of Lean code.

Other computational evidence

Many famous conjectures have been tested computationally to enormous bounds. Such evidence can be mathematically significant, but it does not by itself constitute proof.

Result	Year	Notes
Catalan's conjecture computations	2000s	Exhaustive verification for small cases preceding Mihailescu's proof
Computation of pi to trillions of digits	Ongoing	Current record exceeds 202 trillion digits; the BBP formula allows extraction of individual hexadecimal digits
Collatz conjecture verification	Ongoing	Verified for all starting values up to roughly 10²⁰
Goldbach's conjecture verification	Ongoing	Verified for all even numbers up to 4 x 10¹⁸
Birch and Swinnerton-Dyer conjecture data	1960s-	Originally formulated through computational study of elliptic curves

High-performance computing

High-performance computing, or HPC, is the use of aggregated computational resources to achieve performance far beyond that of a single workstation. It underpins many of the large calculations described above.

Modern HPC systems exploit parallelism at several levels:

Multi-core and many-core processors: modern CPUs provide dozens of cores, while GPUs may contain thousands of simpler cores.
Clusters and distributed memory: large systems consist of many nodes connected by high-speed interconnects such as InfiniBand; communication is typically handled through MPI.
Accelerators: GPUs, FPGAs, and custom ASICs such as TPUs are used for workloads including linear algebra, FFT, and machine learning.
Volunteer and distributed computing: projects such as GIMPS, BOINC, and Folding@home use the idle time of large numbers of consumer machines.

HPC performance is commonly measured in FLOPS, or floating-point operations per second. As of the exascale era, leading systems such as Frontier have exceeded 10¹⁸ floating-point operations per second. The TOP500 list tracks the world's fastest supercomputers.

Common programming models include MPI for distributed memory, OpenMP for shared memory, and CUDA, OpenCL, and SYCL for GPUs and other accelerators. Higher-level languages such as Chapel and Julia aim to simplify parallel programming.

Hardware foundations

Conventional digital computers reduce computation to operations on bits implemented by logic gates such as AND, OR, NOT, and NAND. A set of gates is said to be functionally complete if it can express any Boolean function; NAND alone suffices.

These gates are physically realised using CMOS transistors. Transistor counts per chip have roughly followed Moore's law, rising from about 2,300 in the Intel 4004 in 1971 to more than 200 billion in the largest modern devices. Performance also depends strongly on the memory hierarchy - registers, caches, main memory, and storage - since memory latency often dominates raw arithmetic speed.

For non-classical models of physical computation, see Quantum Computing.

References

Turing, A. M. (1936). "On Computable Numbers, with an Application to the Entscheidungsproblem". Proceedings of the London Mathematical Society. 2 (42): 230-265.
Rado, T. (1962). "On non-computable functions". Bell System Technical Journal. 41 (3): 877-884.
Appel, K.; Haken, W. (1977). "Every planar map is four colorable". Illinois Journal of Mathematics. 21 (3): 429-567.
Rokicki, T.; Kociemba, H.; Davidson, M.; Dethridge, J. (2014). "The diameter of the Rubik's Cube group is twenty". SIAM Journal on Discrete Mathematics. 27 (2): 1082-1105.
Heule, M. J. H.; Kullmann, O.; Marek, V. W. (2016). "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer". SAT 2016. LNCS 9710: 228-245.

External links