Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.math
Subject: Secret Sauce of Dana Scott and Raymond Smullyan
Date: Sat, 18 Jan 2025 01:16:00 +0100
Message-ID: <vmers0$41rn$3@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 18 Jan 2025 00:16:00 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="132983"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.20
Cancel-Lock: sha1:slmZpCwvg5AJvC4FPdLhn8+vt5w=
X-User-ID: eJwFwQkRwEAIBDBLhYXlkMMz+JfQxEHhhNFpfn70rnlysZXbKpN63dByYwPBb6uQXDexm+iSvIeoybUT/GkdFe0=
X-Mozilla-News-Host: news://news.solani.org:119
Bytes: 2954
Lines: 47

Hi,

How it started:

Computers Still Can't Do Beautiful Mathematics - by Gina Kolata
-----------------------------------------------------------------
Mathematicians often say that their craft is as much an art
as a science.  But as more and more researchers are using
computers to prove their theorems, some worry that the magic
is in danger of fading away.

How its going:

Computers Do Produce Beautiful Mathematics - Dr. Larry Wos
-----------------------------------------------------------------
In addition to exhibiting logical reasoning of the type
found in mathematics, reasoning programs produce results
that are startling and elegant.  Dr. J. Lukasiewicz was well
recognized for his contributions to areas of logic,

and yet the program OTTER recently found a proof far shorter and
more elegant than that produced by this eminent researcher,
and the program used the same notation and style of
reasoning.  Mathematicians and logicians find elegance in
shorter proofs.

In August of 1990, Dr. Dana Scott of Carnegie Mellon
University attended a workshop at Argonne National
Laboratory.  There he learned of OTTER and some of its uses
and successes.  Upon returning to his university, Dr.
Scott's curiosity prompted him to suggest (via electronic
mail) 68 theorems for consideration by the computer.

His curiosity was almost immediately satisfied, for the sought-
after 68 proofs were returned with the comment that all were
obtained in a single computer run with the program--and in
less than 16 CPU minutes on a Sun 4 workstation.  Dr. Scott
now uses his own copy of OTTER on his Macintosh.

Dr. R. Smullyan of the University of Indiana showed
great pleasure and surprise at learning of some of the
successes achieved by an automated reasoning program.  As
evidence of his interest, he posed a number of questions,
receiving in turn the answers to all but one of them--a
question that is still open.
https://theory.stanford.edu/~uribe/mail/qed.messages/91.html

Bye