User:Math634/sandbox

Early Life

De Bruijn was born in The Hague, Netherlands on July 9 , 1918. De Bruijn's father owned a paint shop and his family had eight children. He attended an elementary school in The Hague, Netherlands from 1924 to 1930. He then went on to a secondary school called hogere burgerschool, HBS where he studied four years there after graduating in 1934. He finished the 5 year program in HBS in just 4 years. After completing his examinations to finish secondary school, De bruijn failed to get a job or a scholarship due to his young age. He also couldn't find a appropriate job due to the Great Depression in the 1930's. He then took two years to learn mathematics on his own in which he received two mathematical teaching certificates.

College Career

De bruijn received a scholarship to study mathematics at the Leiden University due to his teaching certificate he achieved at the age of 18. During his time at Leiden, De Bruijn was a full-time assistant in the Mathematics Department in Technological University of Delft from 1939 to 1944. De Bruijn was particularly inspired by a lecturer H.D. Kloosterman at Leiden University. De Bruijn remembered the lectures Kloosterman gave on Lebesgue integrals, linear operators in Hilbert spaces, Group Theory, and Number Theory. Kloosterman gave lectures on these subjects from scratch which pleased De Bruijn because he was able to learn them from the ground up. Klossterman stated he hardly ever seen a student like De Bruijn who formulated so precisely during De Bruijn's time at Leiden University. De Bruijn stated in his In Memoriam for Kloosterman "... from Kloosterman I inherited his love for precision and his love for correct mathematical language. Things not to be vague in order to be interesting. It was his style to be careful, precise, clear, patient, right to the goal, never a superfluous word". Right after De Buijn took his doctorate exams in 1940, classes were suspended by the German occupiers because of the student protests over the discharge of Jewish Professors. Leiden University stopped awarding degrees during that time.

Mathematical Career

Across from his parent's home in the Hague was a shop that had a large sign that said Philips. De Bruijn stated that was on the first words he learned to read. Right after De Bruijn got his Ph.D, he took a research job at Philips NatLab research center in Eindhoven from 1944-1946. He felt rescued by this offer from Philips Natlab because he was still an assistant at Delft earning one hundred and twenty guilders a month while still living in his parents home. But at Natlab he got paid three hundred guilders and for him it felt like a royal salary. When he got his job offer at NatLab and moved to Eindhoven in 1944, De Bruijn got married to his wife Elizabeth De Groot in 1944. Together they had four children together; Jorina Aleida born 19 January 1947, Frans Willem born 13 April 1948, Elisabeth born 24 November 1950, and Judith Elizabeth born 31 March 1963. In 1946, he returned back to University of Technology at Delft as a Professor. Then in 1952 he was appointed as a professor at University of Amsterdam. Despite the prestige of University of Amsterdam, which had been the center for Dutch Mathematics for decades, J.J.Seidel managed to lure De Bruijn to the Technische Hogeschool Eindhoven (Eindhoven University of Technology) in 1960. Seidel, De Bruijn’s former fellow student and friend at Leiden University, had organized a new mathematics department there. In this fresh and expanding environment, De Bruijn had great freedom in his research topics. The mathematics department grew in eminence; by 1972, four of the ten KNAW (Royal Netherlands Academy of Arts and Sciences) members in mathematics worked in that department. De Bruijn was one of the members and the other three members were C. J. Bouwkamp,E. W. Dijkstra, and J. H. van Lint. De Bruijn stayed at Eindhoven University of Technology until he retired on 1 August 1984. He was made Professor Emeritus when he retired.

Death

De Bruijn was a respected mathematician throughout his career, with almost 200 articles in journals and several books. Nicolaas Govert de Bruijn died on February 17, 2012 in Nuenen, Netherlands. He was 93 years of age when he died. De Bruijn contributed a lot to the global mathematical community. De Bruijn’s name has been attached to several mathematical notions, such as de Bruijn cycles and de Bruijn graphs, de Bruijn-Newman constant, one Erdo¨s-de Bruijn theorem, de Bruijn indices and de Bruijn notation, and the de Bruijn criterion. All which are in different fields of mathematics varying from graph theory, type lamda calculus, finite geometry, type theory and etc.

History

AutoMath was a project first thought up by Nicolaas Govert De Bruijn. De Bruijn first attempt of a formal language for mathematics was published in 1967. This publication was called the Primitive Automatic Language (PAL). A book in PAL was formed by lines of text organized in nested blocks. Lines could be either axioms, type declarations for variables, or definitions. Surprisingly, with this simple structure one can represent real pieces of mathematics: basically everything that does not exploit the modern notion of function. The publication of PAL set the foundation of the AutoMath project. The basic Automath which was later renamed as AUT-68 was published as a 63 page paper in 1973. Charles G Morgan explains that the purpose of the paper is "... to present a formal language called AUTOMATH. The rules for writing the language are precise enough that a computer may be used to check a body of text for (grammatical) correctness. The author claims that the language is sufficient to express significant portions of mathematics, including meta-theoretical notions concerning inference rules and proofs. The language is so designed that it is incorrect to state a theorem without first "constructing" a proof of the theorem. Thus a computer verification of a body of text translated into AUTOMATH provides automated proof checking. ... The presentation is relatively informal and primarily by example." The research stimulated by the design of the Automath language and some of its variants became what is known as the Automath project, in which a number of researchers collaborated to work on.

The purpose of the Automath Project was to be able to design a mathematical language in which a computer can decipher mathematical theories and verify its correctness.The Automath Project was a predecessor of later Automated Proof Checkers that were later to be established. The Automath project was initiated and was led by De Bruijn in Eindhoven from 1967 until the early 1980s. Readers who were interested in a more complete historical and scientific account of the project are referred to the collection Selected Papers on Automath and to the Automath Archive. Both include several retrospective articles by De Bruijn and others involved in the project. Some recent workshops containing historical reviews are Thirty Five Years of Automating Mathematics and Mathematics, Logic and Computation

De Bruijn had an interest in Computers at a young age and wanted to see how he can use this evolving technology of computers during the late 1960's to the 1980's in Mathematics. De Bruijn’s central aim with the Automath project was the design of a formal language in which any piece of mathematics can be straight forwardly expressed, with the property that a computer can check the correctness of the text. The use of the system should be close to mathematical practice. De Bruijn didn't want the project just showing that such a thing was theoretically possible. De Bruijn wanted to aim higher than that, he was convinced it was actually feasible, even with the computers of that time in the late 1960's and he was anxious to prove it. De Bruijn's goal was that within one or two decades from the start of the Automath project that mathematicians would have a proof checker on their desk and that they would actually use for verifying and archiving results. The goal of the program was to not only verify existing mathematical proofs but allowed the program the ability to which it can possibly also assist mathematicians in proving new results. These goals were quite different from other projects in the emerging field of reasoning with computers, as De Bruijn himself noticed at the conference on Automatic Deduction at Versailles, France in 1968. The Automath project has made lasting contributions, such as:

• Independence of logic: it suffices (and is also advantageous) to design a logical framework suited to different kinds of logical systems.

• Venturing ‘‘beyond Gödel’’: computers can be useful for mathematics, even if they cannot solve all mathematical problems by themselves.

• Enhanced reliability: the feature that all obtained formal expressions can be checked by one fixed and relatively easy algorithm, which can be validated beforehand once and for all.

The Automath project in 1994 had accumulated a collection of papers called the Selected Papers on Automath which is currently the standard reference on Automath. But there are other publications on Automath that are not part of this collection. Even though De Bruijn demonstrated that automatic verification of mathematics was feasible, even with the computer technology of the early 1970s, the achievements of the project were not appreciated at the time. Only two decades later, De Bruijn’s work was picked up by a new generation of researchers. With technological advancements aiding the Mathematics community they recognized the valuable insights underlying the Automath project. Thenew generation of researchers that adopted the concept of Automath started to use Automath in their own research. De Bruijn’s pioneering ventures with Automath are nowadays widely appreciated, in particular in the community of applied logicians working in type theory and in verification of mathematical theories and computer programs. The University of Technology in Eindhoven where De Bruijn was a Professor at digitally archived all his articles on Automath as well as other articles which are widely available online.