|
|
| Line 1: |
Line 1: |
| '''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|Turing machine]], introduced by [[W:Alan Turing|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|Turing complete]]. Many systems not originally designed for general-purpose computation turn out to be Turing complete, including [[W:Conway's Game of Life|Conway's Game of Life]], [[W:CSS|CSS]] with user interaction, and [[W:Magic: The Gathering|Magic: The Gathering]].
| |
|
| |
| A [[Finite-State Machine|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 Language|regular languages]] and are fundamental in automata theory, compiler construction, network protocols, and digital circuit design. Related models include the [[Pushdown Automaton|pushdown automaton]] and the wider [[Chomsky Hierarchy|Chomsky hierarchy]] of formal languages.
| |
|
| |
| Another foundational model is the [[Lambda Calculus|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|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.
| |
| {| class="wikitable"
| |
| |+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|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 vs NP|P]], [[P vs NP|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 [[P vs NP|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 [[W:Millennium Prize Problems|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, [[W:Kenneth Appel|Kenneth Appel]] and [[W:Wolfgang Haken|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 [[W:Coq|Coq]] by [[W:Georges Gonthier|Georges Gonthier]] in 2005.
| |
|
| |
| ; God's number
| |
| : For the [[W:Rubik's Cube|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 [[W:Google|Google]]'s infrastructure.
| |
|
| |
| ; GIMPS and [[Mersenne Prime|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<sup>p</sup> - 1 using the [[W:Lucas-Lehmer primality test|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<sup>136,279,841</sup> - 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 [[W:Euclid|Euclid]], every Mersenne prime gives rise to an [[Perfect Number|even perfect number]] of the form 2<sup>p-1</sup>(2<sup>p</sup> - 1). It remains unknown whether any odd perfect numbers exist.
| |
|
| |
| ; [[W:Boolean Pythagorean triples problem|Boolean Pythagorean triples problem]]
| |
| : This problem illustrates the use of [[W:SAT solver|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]]
| |
| : 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.
| |
|
| |
| {| class="wikitable"
| |
| |+Selected formally verified theorems
| |
| !Theorem
| |
| !Proof assistant
| |
| !Year
| |
| |-
| |
| |[[Four Colour Theorem]]
| |
| |[[W:Coq|Coq]]
| |
| |2005
| |
| |-
| |
| |[[W:Prime number theorem|Prime number theorem]]
| |
| |[[W:Isabelle (proof assistant)|Isabelle]]
| |
| |2005
| |
| |-
| |
| |[[W:Feit-Thompson theorem|Feit-Thompson theorem]]
| |
| |Coq
| |
| |2012
| |
| |-
| |
| |[[Kepler Conjecture]] (Flyspeck)
| |
| |[[W:HOL Light|HOL Light]] and Isabelle
| |
| |2014
| |
| |-
| |
| |[[W:Sphere packing|Sphere packing in dimension 8]]
| |
| |[[W:Lean (proof assistant)|Lean]]
| |
| |2026
| |
| |}
| |
| In February 2026, Maryna Viazovska's proof that the E<sub>8</sub> lattice gives the densest sphere packing in 8 dimensions was formally verified in [[W:Lean (proof assistant)|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.
| |
| {| class="wikitable"
| |
| !Result
| |
| !Year
| |
| !Notes
| |
| |-
| |
| |[[W:Catalan's conjecture|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 [[W:Bailey-Borwein-Plouffe formula|BBP formula]] allows extraction of individual hexadecimal digits
| |
| |-
| |
| |[[W:Collatz conjecture|Collatz conjecture]] verification
| |
| |Ongoing
| |
| |Verified for all starting values up to roughly 10<sup>20</sup>
| |
| |-
| |
| |[[W:Goldbach's conjecture|Goldbach's conjecture]] verification
| |
| |Ongoing
| |
| |Verified for all even numbers up to 4 x 10<sup>18</sup>
| |
| |-
| |
| |[[W:Birch and Swinnerton-Dyer conjecture|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 [[W:InfiniBand|InfiniBand]]; communication is typically handled through [[W:Message Passing Interface|MPI]].
| |
| * Accelerators: GPUs, [[W:Field-programmable gate array|FPGAs]], and custom ASICs such as TPUs are used for workloads including linear algebra, [[W:Fast Fourier transform|FFT]], and machine learning.
| |
| * Volunteer and distributed computing: projects such as GIMPS, [[W:BOINC|BOINC]], and [[W:Folding@home|Folding@home]] use the idle time of large numbers of consumer machines.
| |
|
| |
| HPC performance is commonly measured in [[W:FLOPS|FLOPS]], or floating-point operations per second. As of the exascale era, leading systems such as [[W:Frontier (supercomputer)|Frontier]] have exceeded 10<sup>18</sup> floating-point operations per second. The [[W:TOP500|TOP500]] list tracks the world's fastest supercomputers.
| |
|
| |
| Common programming models include [[W:Message Passing Interface|MPI]] for distributed memory, [[W:OpenMP|OpenMP]] for shared memory, and [[W:CUDA|CUDA]], [[W:OpenCL|OpenCL]], and [[W:SYCL|SYCL]] for GPUs and other accelerators. Higher-level languages such as [[W:Chapel (programming language)|Chapel]] and [[W:Julia (programming language)|Julia]] aim to simplify parallel programming.
| |
|
| |
| == Hardware foundations ==
| |
| Conventional digital computers reduce computation to operations on [[W:Bit|bits]] implemented by [[W:Logic gate|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 [[W:CMOS|CMOS]] transistors. Transistor counts per chip have roughly followed [[W:Moore's law|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 [[W:Memory hierarchy|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]].
| |
|
| |
| == See also ==
| |
|
| |
| * [[Turing Machine]]
| |
| * [[Turing Complete|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.
| |
|
| |
| == External links ==
| |
|
| |
| * [https://www.mersenne.org/ GIMPS - Great Internet Mersenne Prime Search]
| |
| * [https://cube20.org/ God's Number is 20 - cube20.org]
| |
| * [https://bbchallenge.org/ The Busy Beaver Challenge]
| |
| * [https://www.top500.org/ TOP500 Supercomputer Rankings]
| |
| * [https://leanprover-community.github.io/ Lean Prover Community]
| |
| * [https://www.scottaaronson.com/blog/ Scott Aaronson's Blog - Shtetl-Optimized]
| |
