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. In mathematics and theoretical computer science, computation may be studied both as an abstract notion of effective procedure and as a physical process carried out by machines. Computation also plays an important role in practice, where large-scale search, symbolic manipulation, numerical methods, visualization, 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. To do this, mathematicians and computer scientists use formal models of computation: simplified abstract systems that capture what it means to follow a procedure mechanically.

The best-known model is the Turing machine, introduced by Alan Turing in 1936. A Turing machine consists of a tape, a read/write head, and a finite set of states governed by a transition function. Despite its simplicity, it can simulate any algorithm that is ordinarily regarded as effective, and so it became the standard model of general computation. Other equivalent formalisms were developed at about the same time, including the lambda calculus and recursive-function formalisms. The broad agreement among these formalisms underlies the Church-Turing thesis, according to which every effectively calculable procedure can be captured by one of these equivalent models.

A system or language that can simulate an arbitrary Turing machine is called Turing complete. Many systems not originally designed for general-purpose programming turn out to be Turing complete, such as Conway's Game of Life.

Not all models are equally powerful. A finite-state machine is a weaker model with only finitely many states and no unbounded external memory. Finite-state machines recognize exactly the regular languages and are fundamental in automata theory, compiler construction, network protocols, and digital circuit design. More powerful models, such as the pushdown automaton, recognize larger classes of languages and form part of the Chomsky hierarchy. More generally, computation has been studied through state-based models such as automata and Turing machines, functional models such as the lambda calculus, logical models, and concurrent models.

Computability and its limits

Once computation is formalized, 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 $\mathrm{B}\mathrm{B}(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 $\mathrm{B}\mathrm{B}(n)$

$n$	$\mathrm{B}\mathrm{B}(n)$	Year determined
1	1	1962
2	4	1962
3	6	1965
4	13	1983
5	4098	2024
6	unknown	lower bounds only

In 2024 the five-state, two-symbol case was settled completely by the bbchallenge collaboration. In the related step-count version of the problem, the corresponding value is $S(5)=47,176,870$. For 6 states, only enormous lower bounds are known.

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 optimization, cryptography, logic, and algorithm design.

Mathematical practice

These abstract notions of computability and complexity also shape how computation is used in actual mathematical work. Computation is used to test conjectures, search large finite spaces, generate data, visualize structure, verify exceptional cases, and check formal proofs.

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

Roles of computation 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 proved that every planar map can be colored with four colors by combining a general mathematical argument with discharging and a large computer check of thousands of reducible 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 formalized in Coq by Georges Gonthier in 2005.

God's number for the Rubik's Cube

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 cube positions were handled by symmetry reduction, decomposition into 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 compute 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 and was the first record Mersenne prime found using GPUs. 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 colored 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.

Fractals and visualization

Computation can also serve as a tool of visualization. Objects such as the Mandelbrot set are defined by simple iterative rules, but their structure is explored by computing many iterations across a grid of points and rendering the result graphically. In such cases computation does not merely check a theorem or search a space; it reveals patterns, self-similarity, and parameter dependence that are difficult to grasp from formulas alone.

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 formalized 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 dimensions 8 and 24	Lean	2026

In 2026, the sphere-packing results in dimensions 8 and 24 were formalized in Lean in a project that grew to about 200,000 lines of code, with AI tools assisting the process.

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
Computation of pi to 314 trillion digits	2025	A record-sized numerical computation that also serves as a stress test for algorithms, storage, and hardware
Collatz conjecture verification	2025	Verified for all starting values up to $2^{71}$
Goldbach's conjecture verification	2014	Verified for all even numbers up to $4\times 10^{18}$
Birch and Swinnerton-Dyer conjecture data	1960s-	Originally formulated through computational study of elliptic curves

Hardware foundations

Conventional digital computers represent information in binary, encoding data as bits with values 0 and 1. At this level, computation is described by Boolean algebra, in which operations such as AND, OR, and NOT correspond to logical combination and negation. These operations are implemented physically by logic gates. A set of gates is said to be functionally complete if every Boolean function can be built from it; NAND alone suffices, and so does NOR alone. This connection between symbolic logic and circuit design is one of the central links between abstract computation and physical machinery.

Logic gates are combined into larger circuits such as adders, multiplexers, registers, and memory cells. Arithmetic, control flow, and storage are all built from compositions of these elementary Boolean operations. In modern computers these circuits are realized using transistors, typically in CMOS technology, and organized into processors, memory systems, and input/output devices.

Performance depends not only on raw logic speed but also on the movement of data through the memory hierarchy - registers, caches, main memory, and storage. In many practical computations, waiting for data costs more than carrying out the arithmetic itself. For non-classical models of physical computation, see Quantum Computing.

Parallel and large-scale computation

Many important computations exceed the capacity of a single processor or even a single machine. They are made feasible by parallelism, in which a problem is divided so that many operations can be carried out simultaneously.

Parallel computation appears in several forms. A task may be split among many cores in one machine, across many machines in a distributed system, or across large numbers of independent volunteer computers. Some workloads are especially well suited to performing the same operation repeatedly on many data items at once, while others require large search spaces to be divided into many smaller cases that can be checked independently.

At this scale the limiting question is often not just speed but scope: how many cases can be checked, how large a state space can be searched, how many terms or digits can be computed, or how large a numerical range can be tested. This is why large-scale computation is central to exhaustive proofs, record prime searches, simulation, and numerical experimentation.

Performance is often measured in FLOPS (floating-point operations per second). By 2025, the TOP500 list included three exascale systems, each capable of exceeding $10^{18}$ floating-point operations per second. In practice, however, successful large-scale computation depends as much on decomposition, communication, and memory access as on peak arithmetic throughput.

See also

• Turing Machine
• Church-Turing thesis
• Turing completeness
• Finite-State Machine
• Lambda Calculus
• Busy Beaver
• Halting Problem
• Computational Complexity
• P vs NP
• Formal Verification
• Mersenne Prime
• Chomsky Hierarchy
• 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.
• Oliveira e Silva, T.; Herzog, S.; Pardi, S. (2014). "Empirical Verification of the Even Goldbach Conjecture and Computation of Prime Gaps up to 4 x 10¹⁸". Mathematics of Computation. 83 (288): 2033-2060.
• Barina, D. (2025). "Improved verification limit for the convergence of the Collatz conjecture". The Journal of Supercomputing.
• Great Internet Mersenne Prime Search (2024). "52nd Known Mersenne Prime Discovered".
• Formalising Sphere Packing in Lean / EPFL / Math, Inc. (2026).

External links

• GIMPS - Great Internet Mersenne Prime Search
• God's Number is 20 - cube20.org
• The Busy Beaver Challenge
• TOP500 Supercomputer Rankings
• Formalising Sphere Packing in Lean
• Lean Prover Community