De Bruijn Factor

Last updated

The de Bruijn Factor is a measure of how much harder it is to write a formal mathematical proof instead of an informal one. It was created by the Dutch computer-proof pioneer Nicolaas Govert de Bruijn.

De Bruijn computed it as the size of the formal proof over the size of the informal proof. [1]

Freek Wiedijk refined the definition to use the compressed size of the formal proof over the compressed size of the informal proof. He called this the "intrinsic de Bruijin Factor". The compression removes the effect that the length of identifiers in the proofs might have. [2]

Related Research Articles

A fallacy is the use of invalid or otherwise faulty reasoning, or "wrong moves", in the construction of an argument, which may appear stronger than it really is if the fallacy is not spotted. Some fallacies are committed intentionally to manipulate or persuade by deception, while others are committed unintentionally due to carelessness or ignorance. The soundness of legal arguments depends on the context in which the arguments are made.

Informal economy Economic activity unregulated by government

An informal economy is the part of any economy that is neither taxed nor monitored by any form of government.

Mathematical proof Concept in mathematics

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 proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation". Presenting many cases in which the statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases. An proposition that has not been proved but is believed to be true is known as a conjecture, or a hypothesis if frequently used as an assumption for further mathematical work.

Mizar system

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec.

The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically.

Picks theorem Formula for area of a grid polygon

In geometry, Pick's theorem provides a formula for the area of a simple polygon with integer vertex coordinates, in terms of the number of integer points within it and on its boundary. The result was first described by Georg Alexander Pick in 1899. It was popularized in English by Hugo Steinhaus in the 1950 edition of his book Mathematical Snapshots. It has multiple proofs, and can be generalized to formulas for certain kinds of non-simple polygons.

Radboud University Nijmegen University in the Netherlands

Radboud University (abbreviated as RU, Dutch: Radboud Universiteit, formerly Katholieke Universiteit Nijmegen) is a public research university located in Nijmegen, Netherlands. The university bears the name of Saint Radboud, a 9th century Dutch bishop who was known for his intellect and support of the underprivileged.

In logic and mathematics, a formal proof or derivation is a finite sequence of sentences, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.

Proof assistant software tool to assist with the development of formal proofs by human-machine collaboration

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 editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

Nicolaas Govert de Bruijn Dutch mathematician

Nicolaas Govert (Dick) de Bruijn was a Dutch mathematician, noted for his many contributions in the fields of analysis, number theory, combinatorics and logic.

Dickman function

In analytic number theory, the Dickman function or Dickman–de Bruijn functionρ is a special function used to estimate the proportion of smooth numbers up to a given bound. It was first studied by actuary Karl Dickman, who defined it in his only mathematical publication, and later studied by the Dutch mathematician Nicolaas Govert de Bruijn.

Automath is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.

In graph theory, the De Bruijn–Erdős theorem relates graph coloring of an infinite graph to the same problem on its finite subgraphs. It states that, when all finite subgraphs can be colored with colors, the same is true for the whole graph. The theorem was proved by Nicolaas Govert de Bruijn and Paul Erdős (1951), after whom it is named.

De Bruijns theorem On packing congruent rectangular bricks (of any dimension) into larger rectangular boxes

In a 1969 paper, Dutch mathematician Nicolaas Govert de Bruijn proved several results about packing congruent rectangular bricks into larger rectangular boxes, in such a way that no space is left over. One of these results is now known as de Bruijn's theorem. According to this theorem, a "harmonic brick" can only be packed into a box whose dimensions are multiples of the brick's dimensions.

In incidence geometry, the De Bruijn–Erdős theorem, originally published by Nicolaas Govert de Bruijn and Paul Erdős (1948), states a lower bound on the number of lines determined by n points in a projective plane. By duality, this is also a bound on the number of intersection points determined by a configuration of lines.

Ingrid van Engelshoven Dutch politician

Ingrid Katharina van Engelshoven is a Dutch politician who served as Minister of Education, Culture and Science in the Third Rutte cabinet from 26 October 2017 until 10 January 2022.

The Euclid–Euler theorem is a theorem in number theory that relates perfect numbers to Mersenne primes. It states that an even number is perfect if and only if it has the form 2p−1(2p − 1), where 2p − 1 is a prime number. The theorem is named after mathematicians Euclid and Leonhard Euler, who respectively proved the "if" and "only if" aspects of the theorem.

Logic Study of correct reasoning

Logic is the study of correct reasoning or good arguments. It is often defined in a more narrow sense as the science of deductively valid inferences or of logical truths. In this sense, it is equivalent to formal logic and constitutes a formal science investigating how conclusions follow from premises in a topic-neutral way or which propositions are true only in virtue of the logical vocabulary they contain. When used as a countable noun, the term "a logic" refers to a logical formal system. Formal logic contrasts with informal logic, which is also part of logic when understood in the widest sense. There is no general agreement on how the two are to be distinguished. One prominent approach associates their difference with the study of arguments expressed in formal or informal languages. Another characterizes informal logic as the study of ampliative inferences, in contrast to the deductive inferences studied by formal logic. But it is also common to link their difference to the distinction between formal and informal fallacies.

Tom de Bruijn Dutch diplomat and politician

Thomas Justinus Arnout Marie de Bruijn is a Dutch diplomat, civil servant and politician who served as Minister for Foreign Trade and Development Cooperation in the third Rutte cabinet from 10 August 2021 to 10 January 2022. He is a member of the social-liberal Democrats 66 (D66) party.

References

  1. Wiedijk, Freek. "De Bruijn Factor". Radboud University. Retrieved 11 January 2022.
  2. Wiedikj, Freek. "The De Bruijn Factor" (PDF). Radboud University. Retrieved 11 January 2022.