**Mail folder:**QED**Next message:**jt@linus.mitre.org: "Re: from idea to project "**Previous message:**victor yodaiken: "Re: How many false theorems are there?"**Reply:**jt@linus.mitre.org: "Re: from idea to project "**Reply:**Zdzislaw Meglicki: "Re: from idea to project"

Date: Tue, 03 Aug 1993 04:00:34 -0400 (EDT) From: LYBRHED@delphi.com Subject: from idea to project To: qed@mcs.anl.gov Message-id: <01H1AMQV4V0O90NYL7@delphi.com> X-Vms-To: INTERNET"qed@mcs.anl.gov" Mime-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Content-Transfer-Encoding: 7BIT Sender: qed-owner

I have been reading "NeXTSTEP Programming: Step One," by Garfinkel and Mahoney. The two main projects in the book are... calculators! First you build a little four-function calculator, then a more elaborate one that can graph functions. I am struck by the fact that NeXTSTEP seems to be designed as a construction kit for making calculators. And the idea of a "calculator" can be taken to whatever level of sophistication you want. Steve Jobs's original vision of the NeXT Cube could be described as "a platform for QED." The original Cube came with Mathematica, Allegro Common Lisp, and a built-in searchable digital library, at least in skeleton form. It was a Pythagorean computer designed for mathematicians. But so far the only mathematicians who have taken him up on it are the quants on Wall Street and the cryptographers at the CIA. I don't think this was what Steve had in mind. In my last letter I said there should be a demo of QED, or actually a series of demos with increasing functionality. Why not take the NeXT Cube as a prototype of QED? Of course it fell far short of the ideal. It was concerned with numerical calculations rather than proofs. But it could be taken as a demo of Version 0 of QED. It was a first approximation to "a computer system that contains all of mathematics." It is the only computer that even aspires to be QED-like, and it actually exists, so it gives us a tangible starting point. If the Cube is Version 0, then Version 1 would be a 486 computer running NeXTSTEP 3.x. It will have a built-in proof constructor, to go with its built-in librarian and built-in calculation engine. By "proof constructor" I mean a mathematician's workbench, something like the combination of editor, compiler, and debugger that programmers use. It could be used to "compile" a proof into Machine Math and to connect it with other theorems in a "hypermath" network. It would also be able to animate a proof, like the programs that animate sorting algorithms. Version 1 will also have at least the beginning of a mathematical library. The Digital Librarian is already there in NeXTSTEP as a capability, but there is no actual content in the library; at least no mathematical content. The original Cube came with the works of Shakespeare on an optical disk. Shakespeare was the whole library! There is more in Heaven and Earth, Horatio, than is dreamt of in your philosophy! This was where Steve's vision wavered. This was one of his first strategic mistakes. You have to give him credit for conceiving the idea of a computer with a built- in library, but instead of Shakespeare he should have bundled a library of mathematical theorems, methods, and ideas. Version 1 of QED will have at least a token library, enough to see what it would look like. First it will be necessary to create the tools needed to write the proof constructor. NeXTSTEP comes with "kits" for constructing various kinds of applications: the Music Kit, the DB Kit, and so forth. What we need is a Math Kit. This could be an actual project as soon as school starts in the fall. All we need to do is find some students who think working on Version 1 would be a good way to learn computer science and math at the same time, and at least one professor willing to teach them.