Quotes on formalized mathematics and automatic mathematical assistants

To expand on point (a), our approach to user language is also based on a combination of, rather than a compromise between, ease of use and efficiency. We want to make it possible for the user to use notation natural to his problem, although we must restrict him somewhat to the framework of notations we have chosen for our user-computer interface. On the other hand, we are willing to make substantial transformations on the input in computing the internal form of an expression.

It is clear that the system we are trying to create is a very ambitious one. Nevertheless, we think it is appropriate because it focuses our thinking and efforts on the important computer science questions of the day.

R.A. de Millo, R.J. Lipton and A.J. Perlis, Social processes and proofs of theorems and programs Communications of the ACM 22 (1979), 271-280.

(p.272, quoting N. Bourbaki) ``Indeed every mathematician knows that a proof has not been "understood" if one has done nothing more than verify step by step the correctness of the deductions of which it is composed and has not tried to gain a clear insight into the ideas which have led to the construction of this particular chain of deductions in preference to every other one.''

(p.273) In view of these uncertainties over what constitutes an acceptable proof, which is after all a fairly basic element of the mathematical process, how is it that mathematics has survived and been so successful? If proofs bear little resemblance to formal deductive reasoning, if they can stand for generations and then fall, if they can contain flaws that defy detection, if they can express only the probability of truth within certain error bounds--if they are, in fact, not able to prove theorems in the sense of guaranteeing them beyond probability and, if necessary, beyond insight, well, then, how does mathematics work? How does it succeed in developing theorems that are significant and that compel belief?

First of all, the proof of a theorem is a message. A proof is not a beautiful abstract object with an independent existence. No mathematician grasps a proof, sits back, and sighs happily at the knowledge that he can now be certain of the truth of his theorem. He runs out into the hall and looks for someone to listen to it. He bursts into a colleague's office and commandeers the blackboard. He throws aside his scheduled topic and regales a seminar with his new idea. He drags his graduate students away from their dissertations to listen. He gets onto the phone and tells his colleagues in Texas and Toronto. In its first incarnation, a proof is a spoken message, or at most a sketch on a chalkboard or a paper napkin.

That spoken stage is the first filter for a proof. If it generates no excitement or belief among his friends, the wise mathematician reconsiders it. But if they fred it tolerably interesting and believable, he writes it up. After it has circulated in draft for a while, if it still seems plausible, he does a polished version and submits it for publication. If the referees also fred it attractive and convincing, it gets published so that it can be read by a wider audience. If enough members of that larger audience believe it and like it, then after a suitable coolingoff period the reviewing publications take a more leisurely look, to see whether the proof is really as pleasing as it first appeared and whether, on calm consideration, they really believe it.

And what happens to a proof when it is believed? The most immediate process is probably an internalization of the result. That is, the mathematician who reads and believes a proof will attempt to paraphrase it, to put it in his own terms, to fit it into his own personal view of mathematical knowledge. No two mathematicians are likely to internalize a mathematical concept in exactly the same way, so this process leads usually to multiple versions of the same theorem, each reinforcing belief, each adding to the feeling of the mathematical community that the original statement is likely to be true. Gauss, for example, obtained at least half a dozen independent proofs of his "law of quadratic reciprocity"; to date over fifty proofs of this law are known.

(p.275) Once an idea has met the criterion of simplicity, other standards help determine its place among the ideas that make mathematicians gaze off abstractedly into the distance. Yuri Manin has put it best: A good proof is one that makes us wiser.

(p.278) We often use "Let us assume, without loss of generality ..." or "Therefore, by renumbering, if necessary ..." to replace enormous amounts of formal detail. To insist on the formal detail would be a silly waste of resources. Both symbolic and material structures must be engineered with a very cautious eye. Resources are limited; time is limited; energy is limited. Not even the computer can change the finite nature of the universe.

Mathematical Problems by David Hilbert (1900)

From the Introduction:

As long as a branch of science offers an abundance of problems, so long is it alive; a lack of problems foreshadows extinction or the cessation of independent development. Just as every human undertaking pursues certain objects, so also mathematical research requires its problems. It is by the solution of problems that the investigator tests the temper of his steel; he finds new methods and new outlooks, and gains a wider and freer horizon.

It is difficult and often impossible to judge the value of a problem correctly in advance; for the final award depends upon the gain which science obtains from the problem. Nevertheless we can ask whether there are general criteria which mark a good mathematical problem. An old French mathematician said: "A mathematical theory is not to be considered complete until you have made it so clear that you can explain it to the first man whom you meet on the street." This clearness and ease of comprehension, here insisted on for a mathematical theory, I should still more demand for a mathematical problem if it is to be perfect; for what is clear and easily comprehended attracts, the complicated repels us.

Moreover a mathematical problem should be difficult in order to entice us, yet not completely inaccessible, lest it mock at our efforts. It should be to us a guide post on the mazy paths to hidden truths, and ultimately a reminder of our pleasure in the successful solution.

It remains to discuss briefly what general requirements may be justly laid down for the solution of a mathematical problem. I should say first of all, this: that it shall be possible to establish the correctness of the solution by means of a finite number of steps based upon a finite number of hypotheses which are implied in the statement of the problem and which must always be exactly formulated. This requirement of logical deduction by means of a finite number of processes is simply the requirement of rigor in reasoning. Indeed the requirement of rigor, which has become proverbial in mathematics, corresponds to a universal philosophical necessity of our understanding; and, on the other hand, only by satisfying this requirement do the thought content and the suggestiveness of the problem attain their full effect. A new problem, especially when it comes from the world of outer experience, is like a young twig, which thrives and bears fruit only when it is grafted carefully and in accordance with strict horticultural rules upon the old stem, the established achievements of our mathematical science.

Besides it is an error to believe that rigor in the proof is the enemy of simplicity. On the contrary we find it confirmed by numerous examples that the rigorous method is at the same time the simpler and the more easily comprehended. The very effort for rigor forces us to find out simpler methods of proof. It also frequently leads the way to methods which are more capable of development than the old methods of less rigor.

While insisting on rigor in the proof as a requirement for a perfect solution of a problem, I should like, on the other hand, to oppose the opinion that only the concepts of analysis, or even those of arithmetic alone, are susceptible of a fully rigorous treatment. This opinion, occasionally advocated by eminent men, I consider entirely erroneous. Such a one-sided interpretation of the requirement of rigor would soon lead to the ignoring of all concepts arising from geometry, mechanics and physics, to a stoppage of the flow of new material from the outside world, and finally, indeed, as a last consequence, to the rejection of the ideas of the continuum and of the irrational number. But what an important nerve, vital to mathematical science, would be cut by the extirpation of geometry and mathematical physics! On the contrary I think that wherever, from the side of the theory of knowledge or in geometry, or from the theories of natural or physical science, mathematical ideas come up, the problem arises for mathematical science to investigate the principles underlying these ideas and so to establish them upon a simple and complete system of axioms, that the exactness of the new ideas and their applicability to deduction shall be in no respect inferior to those of the old arithmetical concepts.

If we do not succeed in solving a mathematical problem, the reason frequently consists in our failure to recognize the more general standpoint from which the problem before us appears only as a single link in a chain of related problems. After finding this standpoint, not only is this problem frequently more accessible to our investigation, but at the same time we come into possession of a method which is applicable also to related problems. The introduction of complex paths of integration by Cauchy and of the notion of the IDEALS in number theory by Kummer may serve as examples. This way for finding general methods is certainly the most practicable and the most certain; for he who seeks for methods without having a definite problem in mind seeks for the most part in vain.

In dealing with mathematical problems, specialization plays, as I believe, a still more important part than generalization. Perhaps in most cases where we seek in vain the answer to a question, the cause of the failure lies in the fact that problems simpler and easier than the one in hand have been either not at all or incompletely solved. All depends, then, on finding out these easier problems, and on solving them by means of devices as perfect as possible and of concepts capable of generalization. This rule is one of the most important levers for overcoming mathematical difficulties and it seems to me that it is used almost always, though perhaps unconsciously.

Occasionally it happens that we seek the solution under insufficient hypotheses or in an incorrect sense, and for this reason do not succeed. The problem then arises: to show the impossibility of the solution under the given hypotheses, or in the sense contemplated. Such proofs of impossibility were effected by the ancients, for instance when they showed that the ratio of the hypotenuse to the side of an isosceles right triangle is irrational. In later mathematics, the question as to the impossibility of certain solutions plays a preeminent part, and we perceive in this way that old and difficult problems, such as the proof of the axiom of parallels, the squaring of the circle, or the solution of equations of the fifth degree by radicals have finally found fully satisfactory and rigorous solutions, although in another sense than that originally intended. It is probably this important fact along with other philosophical reasons that gives rise to the conviction (which every mathematician shares, but which no one has as yet supported by a proof) that every definite mathematical problem must necessarily be susceptible of an exact settlement, either in the form of an actual answer to the question asked, or by the proof of the impossibility of its solution and therewith the necessary failure of all attempts.

This conviction of the solvability of every mathematical problem is a powerful incentive to the worker. We hear within us the perpetual call: There is the problem. Seek its solution. You can find it by pure reason, for in mathematics there is no ignorabimus.

Rhetoric and mathematics (by Davis and Hersh, 1987)
as quoted by Karlis Podnieks

In the real world of mathematics, a mathematical paper does two things. It testifies that the author has convinced himself and his friends that certain "results" are true, and presents a part of the evidence on which this conviction is based.

The myth of totally rigorous, totally formalized mathematics is indeed a myth.

The QED Manifesto (1994)

(Section 1) QED is the very tentative title of a project to build a computer system that effectively represents all important mathematical knowledge and techniques. The QED system will conform to the highest standards of mathematical rigor, including the use of strict formality in the internal representation of knowledge and the use of mechanical methods to check proofs of the correctness of all entries in the system.

The QED project will be a major scientific undertaking requiring the cooperation and effort of hundreds of deep mathematical minds, considerable ingenuity by many computer scientists, and broad support and leadership from research agencies. In the interest of enlisting a wide community of collaborators and supporters, we now offer reasons that the QED project should be undertaken.

First, the increase of mathematical knowledge during the last two hundred years has made the knowledge, let alone understanding, of all, or even of the most important, mathematical results something beyond the capacity of any human. For example, few mathematicians, if any, will ever understand the entirety of the recently settled structure of simple finite groups or the proof of the four color theorem. Remarkably, however, the creation of mathematical logic and the advance of computing technology have also provided the means for building a computing system that represents all important mathematical knowledge in an entirely rigorous and mechanically usable fashion. The QED system we imagine will provide a means by which mathematicians and scientists can scan the entirety of mathematical knowledge for relevant results and, using tools of the QED system, build upon such results with reliability and confidence but without the need for minute comprehension of the details or even the ultimate foundations of the parts of the system upon which they build. Note that the approach will almost surely be an incremental one: the most important and applicable results will likely become available before the more obscure and purely theoretical ones are tackled, thus leading to a useful system in the relatively near term.

Second, the development of high technology is an endeavor of fabulously increasing mathematical complexity. The internal documentation of the next generation of microprocessor chips may run, we have heard, to thousands of pages. The specification of a major new industrial system, such as a fly-by-wire airliner or an autonomous undersea mining operation, is likely to be even an order of magnitude greater in complexity, not the least reason being that such a system would perhaps include dozens of microprocessors. We believe that an industrial designer will be able to take parts of the QED system and use them to build reliable formal mathematical models of not only a new industrial system but even the interaction of that system with a formalization of the external world. We believe that such large mathematical models will provide a key principle for the construction of systems substantially more complex than those of today, with no loss but rather an increase in reliability. As such models become increasingly complex, it will be a major benefit to have them available in stable, rigorous, public form for use by many. The QED system will be a key component of systems for verifying and even synthesizing computing systems, both hardware and software.

The third motivation for the QED project is education. Nothing is more important than mathematics education to the creation of infrastructure for technology-based economic growth. The development of mathematical ability is notoriously dependent upon "doing" rather than upon "being told" or "remembering". The QED system will provide, via such techniques as interactive proof checking algorithms and an endless variety of mathematical results at all levels, an opportunity for the one-on-one presenting, checking, and debugging of mathematical technique, which it is so expensive to provide by the method of one trained mathematician in dialogue with one student. QED can provide an engaging and non-threatening framework for the carrying out of proofs by students, in the same spirit as a long-standing program of Suppes at Stanford for example. Students will be able to get a deeper understanding of mathematics by seeing better the role that lemmas play in proofs and by seeing which kinds of manipulations are valid in which kinds of structures. Today few students get a grasp of mathematics at a detailed level, but via experimentation with a computerized laboratory, that number will increase. In fact, students can be used (eagerly, we think) to contribute to the development of the body of definitions and proved theorems in QED. Let also us make the observation that the relationship of QED to education may be seen in the following broad context: with increasing technology available, governments will look not only to cut costs of education but will increasingly turn to make education and its delivery more cost-effective and beneficial for the state and the individual.

Fourth, although it is not a practical motivation, nevertheless perhaps the foremost motivation for the QED project is cultural. Mathematics is arguably the foremost creation of the human mind. The QED system will be an object of significant cultural character, demonstrably and physically expressing the staggering depth and power of mathematics. Like the great pyramids, the effort required (especially early on) may be great; but the rewards can be even more staggering than this effort. Mathematics is one of the most basic things that unites all people, and helps illuminate some of the most fundamental truths of nature, even of being itself. In the last one hundred years, many traditional cultural values of our civilization have taken a severe beating, and the advance of science has received no small blame for this beating. The QED system will provide a beautiful and compelling monument to the fundamental reality of truth. It will thus provide some antidote to the degenerative effects of cultural relativism and nihilism. In providing motivations for things, one runs the danger of an infinite regression. In the end, we take some things as inherently valuable in themselves. We believe that the construction, use, and even contemplation of the QED system will be one of these, over and above the practical values of such a system. In support of this line of thought, let us cite Aristotle, the Philosopher, the Father of Logic, "That which is proper to each thing is by nature best and most pleasant for each thing; for man, therefore, the life according to reason is best and pleasantest, since reason more than anything else is man." We speculate that this cultural motivation may be the foremost motivation for the QED project. Sheer aesthetic beauty is a major, perhaps the major, force in the motivation of mathematicians, so it may be that such a cultural, aesthetic motivation will be the key motivation inciting mathematicians to participate.

Fifth, the QED system may help preserve mathematics from corruption. We must remember that mathematics essentially disappeared from Western civilization once, during the dark ages. Could it happen again? We must also remember how unprecedented in the history of mathematics is the clarity, even perfection, that developed in this century in regard to the idea of formal proof, and the foundation of essentially the entirety of known mathematics upon set theory. One can easily imagine corrupting forces that could undermine these achievements. For example, one might suspect that there is already a trend towards believing some recent "theorems" in physics because they offer some predictive power rather than that they have any meaning, much less rigorous proof, with a possible erosion in established standards of rigor. The QED system could offer an antidote to any such tendency. The standard, impartial answer to the question "Has it been proved?" could become "Has it been checked by the QED system?". Such a mechanical proof checker could provide answers immune to pressures of emotion, fashion, and politics.

Sixth, the "noise level" of published mathematics is too high. It has been estimated that something between 50 and 100 thousand mathematical papers are published per year. Nobody knows for sure how many contain errors or how many are repetitions, but some pessimists claim the number of both is high. QED can help to reduce the level of noise, both by helping to find errors and by helping to support computer searches for duplication.

Seventh, QED can help to make mathematics more coherent. There are similar techniques used in various fields of mathematics, a fact that category theory has exploited very well. It is quite natural for formalizers to generalize definitions and propositions because it can make their work much easier.

Eighth, by its insistence upon formalization, the QED project will add to the body of explicitly formulated mathematics. There is mathematical knowledge that is neither taught in classes nor published in monographs. It is below what mathematicians call "folklore," which is explicitly formulated. Let us call this lower level of unformulated knowledge "mathlore". In formalization efforts, we must formalize everything, and that includes mathlore lemmas.

Ninth, the QED project will help improve the low level of self-consciousness in mathematics. Good mathematicians understand trends and connections in their field. The QED project will enable mathematicians to analyze, perhaps statistically, the whole structure of the mathematics, to discover new trends, to forecast developments and so on.

The QED Workshop II, Warsaw, 1995

QED is too big a task to be achieved by a single group. Therefore it will demand the cooperation of different groups which have developed up to now their specific systems for their specific purposes. QED has to use the skills and achievements of these groups.

Cooperation in Proof Exchange. In this approach provers supply lemmas that can be loaded by other provers before starting a proof search. Here the provers can be run completely independent at different times and at different locations connected by a network that gives access to a library of theorems. This is likely to be the most important form of cooperation.

In ILF the user can communicate with the automated provers through a uniform graphical user interface. The integrated systems remain completely independent and no change in their code is required. The user does not have to know theorem provers or logical calculi.

Experiments in ILF in the field of lattice ordered groups show that by the use of automated provers it suffices that the user enters about 10\% of the proof interactively to have it formally verified.

Support the author, the reviewer and the user of a theorem against false theorems as well as against false proofs.

Proving mathematical theorems is a social process. The verification of mathematical arguments is a key activity in mathematics and hence very sensitive for the development of mathematics. Therefore it is not a good idea to try to replace this process by checking proofs in QED.

While correctness and proof presentation may not be the main gains mathematicians can draw from QED they may be very interested in using a large data base of definitions and theorems when it is wellorganized and easy to use.

QED eventually has to enable a human user to develop a machine-checked proof at least as easily as to do that on paper.

A main practical argument for mathematicians to use QED could be the speed of publications. If the article is formally written in QED cumbersome proof reading can be done mechanically and the referees can concentrate on the relevance of the paper rather than on the correctness.

I. Weiss, The QED Manifesto after Two Decades ï¾ Version 2.0 J. Software 11 (2016), 803-815.

However, none of the systems today [2016] can be said to have realized the vision presented in the Manifesto. In current systems of automated proof checking, for instance Coq, HOL, Isabelle, and Mizar, the conversion of a typical proof to the formal system requires a considerable amount of work and typically results in a proof four times longer than what one started with.

Proofs and Fundamentals (2000, by Ethan Bloch)

(from p.57:)
What does a rigorous proof consist of? The word ''proof'' has a different meaning in different intellectual pursuits. A ''proof''in biology might consist of experimental data confirming a certain hypothesis; a ''proof'' in sociology or psychology might consist of the results of a survey. What is common to all forms of proof is that they are arguments that convince experienced practitioners of the given field. So too for mathematical proofs. Such proofs are, ultimately, convincing arguments that show that the desired conclusions follow logically from the given hypotheses.

There is no formal definition of proof that mathematicians use (except for mathematical logicians, when they develop formal theories of proof, but these theories are distinct from the way mathematicians go about their daily business).

Mathematicians who are not logicians virtually never write proofs as strings of logical symbols and rules of inference, for a number of reasons: proofs are often much too long and complicated to be broken down into the two-column (statement-justification) approach; the mathematics is the major issue, so we don't even mention the logical rules of inference used, but rather mention the mathematical justification of each step; we often have to refer to previous theorems, which would need to be brought into the proper logical format; many mathematical proofs are so complicated, and involve so many definitions and symbols, that bringing everything into the logicians' format would be extremely cumbersome; we want proofs to focus on the conceptual difficulties, not the logical ones; non-logicians, which means most mathematicians, find long strings of logical symbols at minimum unpleasant, not to mention confusing. (One look at the difference between the mathematicians' version of [a] proof and the logicians' version, in terms of both length and complexity, should suffice to convince you why mathematicians do things as they do.)

The verifying compiler: A grand challenge for computing research (2003, by Tony Hoare)

I propose a set of criteria which distinguish a grand challenge in science or engineering from the many other kinds of short-term or long-term research problems that engage the interest of scientists and engineers.

In the following list, the earlier criteria emphasize the significance of the goals, and the later criteria relate to the feasibility of the project, and the maturity of the state of the art.

A Grand Challenge for Computing Research: a mathematical assistant (2003, by Toby Walsh)

Scientists, engineers and students would all benefit greatly from the help of a mathematical assistant. Such an assistant should be rigorous and indefatigable, and have vast amounts of mathematical knowledge at her fingertips. Since these are precisely the qualities we appreciate most in computers, computers ought to make excellent mathematical assistants. Indeed, in specialized domains, computers already are useful mathematical assistants. For example:

The challenge then is to develop an automated mathematical assistant with both breadth and depth of mathematical expertise. The assistant should cooperatively help users solve their mathematical problems, adapting and learning over time. Such an assistant would be able to:

Such an assistant will require research in a wide number of areas. These include:

It is certainly a challenge since we could fail. AI has had success in narrow domains (witness expert systems) but broad expertise, like that proposed here, is a much more challenging and uncertain goal. What about the other criteria identified in the call for submissions to the workshop? This challenge arises from curiosity about the limits of how much mathematics we can automate. It aims to build something never seen before. It ought to be obvious when the challenge is met since we will stop asking our mathematical colleagues for help. It will be useful to the whole scientific community so should gain their support. It is of a scale that will require international participation. It will be comprehensible to the general public. It was formulated long ago (at least as far back as Leibniz's desire to reduce all mathematics to calculation). It will take us way beyond the domain specific mathematical tools available today. It will require planned co-operation between many different research projects. Even partial success will improve the mathematical tools available. Finally, given the scale and ambition of the challenge, it is unlikely to happen through the evolution of existing commercial products.

The Status of the Classification of the Finite Simple Groups (by Michael Aschbacher, 2004)

Common wisdom has it that the theorem classifying the finite simple groups was proved around 1980. However, the proof of the Classification is not an ordinary proof because of its length and complexity, and even in the eighties it was a bit controversial. [...] However, [...] over the last twenty years gaps have been discovered in the original proof of the Classification. Most of these gaps were quickly eliminated, but one presented serious difficulties. The serious gap has recently been closed, so it is perhaps a good time to review the status of the Classification.

Highly complex proofs and implications of such proofs (by Michael Aschbacher, 2005)

Conventional wisdom says the ideal proof should be short, simple, and elegant. However there are now examples of very long, complicated proofs, and as mathematics continues to mature, more examples are likely to appear. Such proofs raise various issues. For example it is impossible to write out a very long and complicated argument without error, so is such a 'proof' really a proof? What conditions make complex proofs necessary, possible, and of interest? Is the mathematics involved in dealing with information rich problems qualitatively different from more traditional mathematics?

And so on... Reasoning with infinte diagrams (by Solomon Feferman, 2008)

A proof must convince us of the truth of the statement being proved. ''Truth'' is taken in its prima facie sense, i.e. we are supposed to understand the meanings of the notions in that statement. To be convinced of a proof, one must follow the argument and check the steps using also background knowledge. So to follow a proof we must also understand the meanings of the notions used in the proof and from background knowledge. Even given that, it is possible to go through the steps of a proof and not ''really understand'' the proof itself.

Really Understanding Proofs - When we~re led to say, ''Oh, I see!'' - It~s a special kind of insight into how and why the proof works. - That kind of understanding of proofs is necessary in order to be a fullfledged consumer and producer of mathematics.

Understanding of both meanings and proofs is essential to higher mathematical activity, and that is in no way reflected in the formal model.

Social Epistemology (from the Stanford Encyclopedia of Philosophy)

Classical epistemology has been concerned with the pursuit of truth. How can an individual engage in cognitive activity so as to arrive at true belief and avoid false belief? This was the task René Descartes set for himself in his Discourse on the Method of Rightly Conducting the Reason and Seeking for Truth in the Sciences (1637/1955) and in his Meditations on First Philosophy (1641/1955). Classical epistemology has equally been concerned with rationality or epistemic justification, as suggested by part of the title of the Discourse. A person might rightly conduct her reason in the search for truth but not succeed in getting the truth. However, as long as she forms a belief by a proper use of reason - and perhaps by proper use of other faculties like perception and memory - then her belief is rationally warranted or justified.

Many researchers in the social studies of knowledge reject or ignore such classical concerns of epistemology as truth, justification, and rationality. It is acknowledged, of course, that various communities and cultures speak the language of truth, justification, or rationality, but the researchers in question do not find such concepts legitimate or useful for their own purposes. They seek to describe and understand a selected community's norms of rationality, like anthropologists describing the norms or mores of an alien culture. But they reject the notion that there are any universal or "objective" norms of rationality, or criteria of truth, that they themselves could appropriately invoke. As Barry Barnes and David Bloor put it, "there are no context-free or super-cultural norms of rationality" (1982: 27). So they are not prepared to decree that certain practices are more rational or more truth-conducive than others.

They are, nonetheless, clearly interested in belief-forming practices. If we use the term "knowledge" for any sort of belief (or at least for "institutionalized" belief), whether true or false, justified or unjustified, then they can be said to be investigators of knowledge.

The Social Dimensions of Scientific Knowledge (from the Stanford Encyclopedia of Philosophy)

Each member or subgroup participating in such a project is required because each has a crucial bit of expertise not possessed by any other member or subgroup. This may be knowledge of a part of the instrumentation, the ability to perform a certain kind of calculation, the ability to make a certain kind of measurement or observation. The other members are not in a position to evaluate the results of other members' work, and hence, all must take one anothers' results on trust. The consequence is an experimental result, (for example, the measurement of a property such as the decay rate or spin of a given particle) the evidence for which is not fully understood by any single participant in the experiment. This leads Hardwig to ask two questions, one about the evidential status of testimony, and one about the nature of the knowing subject in these cases. With respect to the latter, Hardwig says that either the group as a whole, but no single member, knows or it is possible to know vicariously. Neither of these is palatable to him. Talking about the group or the community knowing smacks of superorganisms and transcendent entities and Hardwig shrinks from that solution. Vicarious knowledge, knowing without oneself possessing the evidence for the truth of what one knows, requires, according to Hardwig, too much of a departure from our ordinary concepts of knowledge.

The first question is, as Hardwig notes, part of a more general discussion about the epistemic value of testimony. Much of what passes for common knowledge is acquired from others. We depend on experts to tell us what is wrong with our appliances, our cars, our bodies. Indeed, much of what we later come to know depends on what we previously learned as children from our parents. We acquire knowledge of the world through the institutions of education, journalism, and scientific inquiry. Philosophers disagree about the status of beliefs acquired in this way.

B does not know simply on the basis of A's testimony. While this result is consistent with traditional philosophical empiricism and rationalism, which emphasized the individual's sense experience or rational apprehension as foundations of knowledge, it does have the consequence that we do not know most of what we think we know.

Formal mathematics in natural language? (Aarne Ranta)

How relevant natural language is in a math wiki depends largely on whom one wants to use it. If the wiki is meant just for experts who want to exchange their formal proofs, then it may be adequate to use just the type theoretical formalisms; it is well known that formal proof experts are more comfortable with formal than natural languages, as it comes to expressing mathematics. To motivate the use of natural language, two new kinds of users should be targeted:

In the setting of a European proposal, one could point out that non-expert users should not be underestimated:

making the results accessible to a wide audience can be an important part of the dissemination plan. One should also bear in mind that most working mathematicians are non-experts in formal proofs, and might become users of the wiki more easily if they did not need to learn a new language.

• ordinary mathematical language uses symbolism for some singular terms and predicates, natural language for the overall logical structure and text structure; as a third ingredient, diagrams can be used for presenting sometimes very complex structures
• therefore, to create the "look" of ordinary mathematics, we should present the overall structure in natural languages
• this has been shown feasible as regards definitions and statements of theorems, and also problems and exercises (WebALT): we can translate them mechanically from formal representations to readable natural language
• translating proofs is only feasible if the proofs are structured on high enough level; the main problem in rendering proofs in natural language is largely the same as making them readable as formal proofs (this is a problem especially if the starting point is proofs found by automatic theorem provers)
• from nicely structured proofs, readable natural language can be genererated, as shown by Wikicoqweb and Mizar
• the problem is largely language independent: with a grammar library such as used in WebALT, a solution can be ported to new languages by mainly porting a domain lexicon

Platonism, intuition and the nature of mathematics (by Karlis Podnieks)

The process of idealization ended in stable, fixed, self-contained concepts of numbers, points, lines etc. These concepts ceased to change and were commonly acknowledged in the community of mathematicians. And all that was achieved already in the V century BC. Since that time our concepts of natural numbers, points, lines etc. have changed very little. The stabilization of concepts is an evidence of their detachment from real objects that have led people to these concepts and that are continuing their independent life and contain an immense variety of changing details. When working in geometry, a mathematician does not investigate the relations of things of the human practice (the "real world" of materialists) directly, he investigates some stable notion of these relations - an idealized, fantastic "world" of points, lines etc. And during the investigation this notion is treated (subjectively) as the "last reality", without any "more fundamental" reality behind it. If during the process of reasoning mathematicians had to remember permanently the peculiarities of real things (their degree of smoothness etc.), then instead of a science (efficient geometrical methods) we would have an art - simple, specific algorithms obtained by means of trial and error or on behalf of some elementary intuition. Mathematics of Ancient Orient stopped at this level. Greeks went further.

Studying mathematics Plato came to his surprising philosophy of two worlds: the "world of ideas" (as perfect as the "world" of geometry) and the "world of things". According to Plato, each thing is only an imprecise, imperfect implementation of its "idea" (which does exist independently of the thing itself in the world of ideas). Surprising and completely fantastic was Plato's notion of the nature of mathematical investigation: before a mathematician is born, his soul is living in the world of ideas, and afterwards, doing mathematics, he simply remembers what his soul has learned in the world of ideas.

LogiWeb (LaTeX based, by Klaus Grue)

Logiweb was designed and implemented 1996-2006 to meet the following objectives:

Accumulation of knowledge: Once a machine formalized development was published on Logiweb, the publication should remain accessible in unchanged form forever. This simply mimics what publishing houses and libraries provide for ordinary mathematics.

Standing on the shoulders of predecessors: When proving a theorem, users should be able to draw upon theorems proved by others. This simply mimics the way any mathematician works.

Notational freedom: Each user should be free to use any notation. That freedom should come without restricting the notational freedom of others. And differences in notation should be no obstacle when using the results of others.

Foundational freedom: Each user should be free to choose what mathematical foundation to work upon. Import of results from one foundation to another should be possible (but not neccessarily trivial).

Distribution: Access to the work of others should happen transparently via the Internet.

Readibility: Users should be able to publish articles on Logiweb which are as readable as any mathematics book one can pick from any library.

Accommodation: Users should be able to publish anything from short notes to multi-volume works that span thousands of pages.

Scalability: The system should allow an arbitrary number of submissions and should run smoothly up to 10^18 papers.

Simplicity: The system should be so simple that its core could be implemented by a single person. And so simple that once it was implemented, a graduate computer science student could re-implement it in one year.

Extensibility: Once the core was implemented, users should be able to adapt the system without changing the core and should be able to publish adaptations on Logiweb itself to make the adaptations available to other users.

Verification: Logiweb should be able to tell whether or not a publication is correct. In the spirit of accumulation, correctness should be time independent such that a publication which is deemed correct at one time should remain correct forever.

Ninth International Conference on Mathematical Knowledge Management 10-12 July 2009 Grand Bend, Ontario (Canada)

Mathematical Knowledge Management is the field at the intersection of mathematics, computer science, library science, and scientific publishing. Its development is driven by on the one hand new technological possibilities which computer science, the Internet, and intelligent knowledge processing offer, and on the other hand the increasing demand by engineers and scientists for new techniques for producing, transmitting, consuming, and managing sophisticated mathematical knowledge. The conference is concerned with all aspects of mathematical knowledge management. Topics covered include, but are not limited to:

• Representations of mathematical knowledge
• Repositories of formalized mathematics
• Mathematical digital libraries
• Diagrammatic representations
• Multi-modal representations
• Mathematical OCR
• Mathematical search and retrieval
• Deduction systems
• Math assistants, tutoring and assessment systems
• Authoring languages and tools
• MathML, OpenMath, and other mathematical content standards
• Web presentation of mathematics
• Data mining, discovery, theory exploration
• Computer Algebra Systems
• Collaboration tools for mathematics
• Challenges and Solutions for Mathematical workflows

Formalizing Mathematics (by Herman Geuvers)

The concrete aim is to make formalizing of known mathematics of the same degree of easiness as writing it up in LaTeX. In addition, we want the formalized mathematics to be available in an active form, that represents also the semantics. So, we want to be able to

• browse and search libraries of formalized mathematics, (so it should both be readable, like a mathematics book and searchable like a database),
• use the stored formalized mathematics, e.g. by computing with it or proving with it (so it should be possible to actively use the mathematics in a computer algebra system or a theorem prover),
• extend the corpus of formalized mathematics. For example by extending the formalized theory or by adding an illuminating example. Extending should be as easy as writing it up in, say, LaTeX.

How? We perform and study concrete (large) formalizations of mathematics in mathematical assistants. Presently there are two types of system in which mathematics can be presented in some kind of semantical form: Theorem Provers (TPs) and Computer Algebra Systems (CAs). The first have the advantage that a lot of mathematical concepts can be represented (defined) very precisely and hence completely formalized proofs can be given. The second have the advantage that it is much simpler to represent mathematics (if it falls within the expressive scope of the CA) and its computation capabilities are much larger.

At present, TPs are the only systems in which one can really formalize a large piece of mathematics, so we focus on those. We are mainly users of Coq and we have experimented (and we presently still are) with some larger developments in Coq. We also develop specific tools for supporting and automating the proof-process. Other systems that we look into are Mizar and HOL-light (but this list may vary from time to time). We have also done some experiments with combining TPs and CAs, to let the TP profit from the computing facilities of the CA. Another topic that we study is the presentation of formalized mathematics. Ideally this should be done via an (interactive) document that can be read roughly as an ordinary mathematics book.

The language of proofs (Naproche, 2007)
TeXmacs based

(p.12) From a linguistic perspective, the Language of Mathematics is distinguished by the fact that its core mathematical meaning can be fully captured by an intelligent translation into rst-order predicate logic.

The project NAPROCHE aims at constructing a system which accepts a controlled but rich subset of ordinary mathematical language including TeX-style typeset formulas and transforms them into formal statements. We adapt linguistic techniques to allow for common grammatical constructs and to extract mathematically relevant implicit information about hypotheses and conclusions. Combined with proof checking software we obtain NAtural language PROof CHEckers which are prototypically used to teach mathematical proving.

It has been experimentally used in a first-year undergraduate course Mathematics for computer scientists.

Generating Proof Representation Structures in the Project Naproche (by Nickolay Kolev)

(p.6) [The project] aims at providing a system within which mathematical texts written in a controlled natural language can be automatically checked for integrity and correctness. The project is intended as an aid to both authors, who wish to check their work before submitting it, and to reviewers who wish to automatically check work submitted to them. The prototypical users of the system are students of mathematics and related fields such as computer science and physics, who need to turn in mathematical proofs as assignments, and teachers and teaching assistants who need to check large numbers of such proofs.

Buchberger's preface of MKM2001 Conference

I believe that mathematical knowledge management will turn out to be one of the most exciting future topics of mathematics and will lead to a new understanding of the fundamentals of mathematics in the same way as the foundational problems of mathematics in the early 20th century lead to a new, and much deeper, understanding of mathematics and to a whole wave of new directions, techniques and results. The impacts of advances in mathematical knowledge management on all of science and technology will be dramatic both because of the role of mathematics as the universal "thinking technology" of all science and technology and because techniques to be worked out for mathematical knowledge management will be applicable also for other, less structured, disciplines.

Mathematical Knowledge Management

The realm of mathematical information looks as the best candidate for testing innovative theoretical and technological solutions for content-based systems, interoperability, management of machine understandable information, and the Semantic Web.

MOWGLI

Semantical search for mathematical concepts (rather than keywords).

Classification: given a concrete mathematical structure, is there a general theory for it?

All modern sciences have a strongly mathematicised core, and will benefit.

The real market and application area for the techniques developed in this project, apart from the obvious realm of education, lies with high-tech and engineering corporations that rely on huge formula databases.

Logosphere (uses Twelf as the common intermediate language)

The quantity of mathematical knowledge is growing faster than our ability to formalize and organize it. The proposed research focuses on developing a Formal Digital Library called Logosphere, a common and open infrastructure for managing and sharing mathematical knowledge and formal proof. Central to this work is the design of a logical framework as a representation language for logical formalisms, individual theories, and proofs, with an interface to theorem proving systems such as PVS or HOL, that have been effective in industrial practice. Logoshpere emphasizes interoperability between theorem proving systems, and the exchange and reusability of mathematical facts across different systems.

Constructive Coq Repository at Nijmegen

a good computer-representation of mathematics will enable the following.

Mathematical Components Manifesto (Georges Gonthier)

The object of this project is to demonstrate that formalized mathematical theories can, like modern software, be built out of components. By components we mean modules that comprise both the static (objects and facts) and dynamic (proof and computation methods) contents of theories.

The lack of good mathematical libraries is due to the difficulty of creating and using them. The most commonly cited causes for this difficulty are rather superficial, such as poor input and display notation, poor lookup and retrieval, insufficient automation of deduction. It is our thesis that the ''library'' concept itself is at fault, more precisely the notion that a mathematical library consists of a set of symbols and a collection of first-order theorems for using these symbols. For to use such a library one must adhere exactly to its conventions and this all but rules out the ''abuses of notation that make mathematics tractable'' (Bourbaki).

The final target would be the Feit-Thompson (or Odd Order) theorem, which gives the structure of all finite groups with an odd number of elements, and whose textbook proof is over 250 pages, on top of 300 pages of prerequisites.

slawekk's weblog

1/0 = 0, really!
(my paraphrase)
Undefined function values are the empty set in ZF, and hence equal 0. This is very unnatural, and shows that ZF is not the correct foundation of math

more-113
In mathematics proofs have also another role to fulfill: proofs convey knowledge. People study proofs not only to check if they do not contain mistakes, but also to find out why the assertion is true.

mathwiki-conference
To me software for doing formalized mathematics becomes interesting when:

1. it supports ZF set theory or something similar (really, now, not potentially),

2. some work has been done on formalizing a bit more than foundations so that I can evaluate how readable the proofs can be made and how easy they are to write.

Theorem provers are typically created at computing science departments. No wonder that so few provers (Isabelle and Mizar) support ZFC.

Another reason support for ZFC is rare is that funding for formalized mathematics projects is often obtained by promising something like ''the production of mathematically proved programs'' (Cornell, NuPrl, grant from the Office of Naval Research). Once your stated goal is formally verified software, ZFC is gone from the picture, together with a chance for a larger participation of people with standard mathematical education.

I am a mathematician by training and I have tried to use Isabelle/HOL. It was weird and I felt like I was writing software rather than mathematics. I could do it, but it was not fun. Isabelle/ZF, on the other hand was easy and natural.

by ''readable proof'' I mean one that uses standard mathematical notation and terminology and anyone with some mathematical education is able to follow it without having to learn a new language with words like ''constdefs'' and ''assms''.

Just like a standard math paper needs more than just definitions, theorems and proofs, formalized math text needs some informal text to dilute content, explain motivation, mention other people's work or simply provide keywords to make searching easier. However, this should not be the main ingredient. The approach that reduces formalized text to an optional comment on the informal content misses the point.

Some of My Other Pages

my home page (http://arnold-neumaier.at/)