HOME

TheInfoList



OR:

A computer-assisted proof is a
mathematical proof A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every pr ...
that has been at least partially generated by
computer A computer is a machine that can be programmed to carry out sequences of arithmetic or logical operations ( computation) automatically. Modern digital electronic computers can perform generic sets of operations known as programs. These prog ...
. Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical
theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of t ...
. The idea is to use a computer program to perform lengthy computations, and to provide a proof that the result of these computations implies the given theorem. In 1976, the
four color theorem In mathematics, the four color theorem, or the four color map theorem, states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. ''Adjacent'' means that two regions sha ...
was the first major theorem to be verified using a
computer program A computer program is a sequence or set of instructions in a programming language for a computer to Execution (computing), execute. Computer programs are one component of software, which also includes software documentation, documentation and oth ...
. Attempts have also been made in the area of
artificial intelligence Artificial intelligence (AI) is intelligence—perceiving, synthesizing, and inferring information—demonstrated by machines, as opposed to intelligence displayed by animals and humans. Example tasks in which this is done include speech ...
research to create smaller, explicit, new proofs of mathematical theorems from the bottom up using
automated reasoning In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer prog ...
techniques such as
heuristic A heuristic (; ), or heuristic technique, is any approach to problem solving or self-discovery that employs a practical method that is not guaranteed to be optimal, perfect, or rational, but is nevertheless sufficient for reaching an immediate ...
search. Such
automated theorem prover Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a m ...
s have proved a number of new results and found new proofs for known theorems. Additionally, interactive
proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof edi ...
s allow mathematicians to develop human-readable proofs which are nonetheless formally verified for correctness. Since these proofs are generally human-surveyable (albeit with difficulty, as with the proof of the Robbins conjecture) they do not share the controversial implications of computer-aided proofs-by-exhaustion.


Methods

One method for using computers in mathematical proofs is by means of so-called
validated numerics Validated numerics, or rigorous computation, verified computation, reliable computation, numerical verification (german: Zuverlässiges Rechnen) is numerics including mathematically strict error (rounding error, truncation error, discretization er ...
or rigorous numerics. This means computing numerically yet with mathematical rigour. One uses set-valued arithmetic and in order to ensure that the set-valued output of a numerical program encloses the solution of the original mathematical problem. This is done by controlling, enclosing and propagating round-off and truncation errors using for example
interval arithmetic Interval arithmetic (also known as interval mathematics, interval analysis, or interval computation) is a mathematical technique used to put bounds on rounding errors and measurement errors in mathematical computation. Numerical methods using ...
. More precisely, one reduces the computation to a sequence of elementary operations, say (+, -, \times, /). In a computer, the result of each elementary operation is rounded off by the computer precision. However, one can construct an interval provided by upper and lower bounds on the result of an elementary operation. Then one proceeds by replacing numbers with intervals and performing elementary operations between such intervals of representable numbers.


Philosophical objections

Computer-assisted proofs are the subject of some controversy in the mathematical world, with
Thomas Tymoczko A. Thomas Tymoczko (September 1, 1943August 8, 1996) was a philosopher specializing in logic and the philosophy of mathematics. He taught at Smith College in Northampton, Massachusetts from 1971 until his death from stomach cancer in 1996, aged 52. ...
first to articulate objections. Those who adhere to Tymoczko's arguments believe that lengthy computer-assisted proofs are not, in some sense, 'real'
mathematical proof A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every pr ...
s because they involve so many logical steps that they are not practically verifiable by human beings, and that mathematicians are effectively being asked to replace logical deduction from assumed axioms with trust in an empirical computational process, which is potentially affected by errors in the computer program, as well as defects in the runtime environment and hardware.. Other mathematicians believe that lengthy computer-assisted proofs should be regarded as ''calculations'', rather than ''proofs'': the proof algorithm itself should be proved valid, so that its use can then be regarded as a mere "verification". Arguments that computer-assisted proofs are subject to errors in their source programs, compilers, and hardware can be resolved by providing a formal proof of correctness for the computer program (an approach which was successfully applied to the four-color theorem in 2005) as well as replicating the result using different programming languages, different compilers, and different computer hardware. Another possible way of verifying computer-aided proofs is to generate their reasoning steps in a machine-readable form, and then use a proof checker program to demonstrate their correctness. Since validating a given proof is much easier than finding a proof, the checker program is simpler than the original assistant program, and it is correspondingly easier to gain confidence into its correctness. However, this approach of using a computer program to prove the output of another program correct does not appeal to computer proof skeptics, who see it as adding another layer of complexity without addressing the perceived need for human understanding. Another argument against computer-aided proofs is that they lack mathematical elegance—that they provide no insights or new and useful concepts. In fact, this is an argument that could be advanced against any lengthy proof by exhaustion. An additional philosophical issue raised by computer-aided proofs is whether they make mathematics into a quasi-empirical science, where the
scientific method The scientific method is an empirical method for acquiring knowledge that has characterized the development of science since at least the 17th century (with notable practitioners in previous centuries; see the article history of scientifi ...
becomes more important than the application of pure reason in the area of abstract mathematical concepts. This directly relates to the argument within mathematics as to whether mathematics is based on ideas, or "merely" an
exercise Exercise is a body activity that enhances or maintains physical fitness and overall health and wellness. It is performed for various reasons, to aid growth and improve strength, develop muscles and the cardiovascular system, hone athletic ...
in formal symbol manipulation. It also raises the question whether, if according to the
Platonist Platonism is the philosophy of Plato and philosophical systems closely derived from it, though contemporary platonists do not necessarily accept all of the doctrines of Plato. Platonism had a profound effect on Western thought. Platonism at l ...
view, all possible mathematical objects in some sense "already exist", whether computer-aided mathematics is an observational science like astronomy, rather than an experimental one like physics or chemistry. This controversy within mathematics is occurring at the same time as questions are being asked in the physics community about whether twenty-first century
theoretical physics Theoretical physics is a branch of physics that employs mathematical models and abstractions of physical objects and systems to rationalize, explain and predict natural phenomena. This is in contrast to experimental physics, which uses experim ...
is becoming too mathematical, and leaving behind its experimental roots. The emerging field of experimental mathematics is confronting this debate head-on by focusing on numerical experiments as its main tool for mathematical exploration.


Applications


Theorems proved with the help of computer programs

Inclusion in this list does not imply that a formal computer-checked proof exists, but rather, that a computer program has been involved in some way. See the main articles for details.


Theorems for sale

In 2010, academics at The
University of Edinburgh The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 1 ...
offered people the chance to "buy their own theorem" created through a computer-assisted proof. This new theorem would be named after the purchaser. This service now appears to no longer be available.


See also


References


Further reading

* * *


External links

* * * * {{Numerical PDE Argument technology Automated theorem proving Computer-assisted proofs Formal methods Numerical analysis Philosophy of mathematics