Re: Incentive to write proofs

• Mail folder: QED
• Next message: mthayer@BIX.com: "Boyer's Constant"
• Previous message: Zdzislaw Meglicki: "Re: Boyer's Hypothesis"
• Maybe in reply to: John Harrison: "Incentive to write proofs"

Message-id: <gfqoQ82KmlE2IUS25Z@arp>
Date: Mon, 26 Apr 1993 12:20:56 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Re: Incentive to write proofs
Sender: qed-owner
Precedence: bulk

In <9304251907.AA08125@maui.cs.ucla.edu> chou@CS.UCLA.EDU writes:

> I guess everyone who's done machine-assisted theorem proving would agree
> with John Harrison and Josh Guttman on its educational value. But, is
> there any funding agency which is willing to fund such a grand proposal
> as QED just because of its "educational value"?

Few areas of science are as important to intellectual development of the
society as a whole and to its industrial and technological prowess as
mathematics. Societies which neglect or just dump mathematics very
quickly begin to lag behind other more mathematically aware societies
and cultures. After all it was the developments in mathematics, physics,
chemistry and engineering that gave the Europeans the technological edge
which provided them with the means to colonize other cultures and
countries in XVIII and XIX centuries. This point was made very
succinctly by Abdus Salam (Nobel prize for electroweak interactions
together with Weinberg and Glashow) in his conversation with Zhou En
Lai. But even without delving into past ages the importance of
mathematics and the high cost of its neglect can be easily ascertained
by observing what has happened in some Western societies over the last
30 years. The cultural revolution of the 60s and 70s resulted in
diminished emphasis on mathematics and other so called "hard sciences"
in primary and secondary schools in many countries. Almost all of them
paid for this with faltering economies and diminished technological
innovation in comparison with countries in which the "Hippie cultural
revolution" did not have such a devastating effect (e.g., Japan, France,
Germany, Italy, Singapore). For such reasons it may be far easier to
obtain funding for QED than Chou's note would suggest. There are many
people in high technology industries and in management of those
industries who may see such a project as a worthwhile long term
investment in the future of their own industries and their
competitiveness. The governments may be equally interested in fostering
mathematical culture. I don't see this as a hopeless dream. 

   Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
   Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS,
   The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, 
   Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158