[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Math rigor in the electronic age
Even if the information given by Greg is not exact - Imean about the
Mizar proof of the Jordan Theorem, you might be
interested in it:
<!--X-From: Bill Richter <richter@math.nwu.edu> -->
****************************************************************
* archive: <A HREF="http://math.albany.edu:8800/hm/emj/";>http://math.albany.edu:8800/hm/emj/</A> *
* glimpse index: <A HREF="http://nyjm.albany.edu:8000/SF/emjsearch.html";>http://nyjm.albany.edu:8000/SF/emjsearch.html</A> *
****************************************************************
Greg Kuperberg on Wed, 1 Sep 1999 23:35:52 -0700)
Subject: Re: Math rigor in the electronic age
FCC: ~/Mail/outahere
References: <<A HREF="msg00256.html"><A HREF="msg00256.html">199909020635.XAA23854@manifold.math.ucdavis.edu</A></A>>
--text follows this line--
> You want to decouple publication/dissemination from peer review /
> refereeing?
Yes, exactly!
> Maybe that's a good idea. But what will be the new mechanism for
> refereeing? Unless a powerful new structure is created, I think
> we'll have even less refereeing in your new electronic age than
> we have now.
Right! Apart from the fact that I and many other people want it to
happen, distribution *is* decoupling from peer review.
Greg, that's because of technology is obseleting the old system? I'll
accept that. So the decoupling doesn't require your intervention.
The challenge for the old guard, especially math journals, is to
adapt to the transition. That is exactly the reason that I keep
stoking this discussion in the EMJ mailing list. I do not know the
new mechanism either, but I know that none of us will find it
unless we try.
I think the unknown mechanism is the place to stoke the discussion.
People will stick to the old lousy mechanism until a new mechanism is
worked out. I think that's Kuhn's theory of paradigm shifts -- we can
poke all the holes we want in the old paradigm, but the shift doesn't
take place until the new paradigm is worked out well enough to take
it's place (so e.g. the old grants can get "shifted" to new grants).
The old system even has some advantages. As Mark Steinberger argued,
a submitted and then published paper is fixed target. Maybe moving
targets are harder to review.
> I'm not sure I understand. Just & Weese claim that all of modern
> mathematics (logic & set theory aside, which aren't considered
> real mathematics) consists of deductions of the ZFC axioms in
> their book "Basic Set Theory I".
The most that they can reasonably mean is that most of modern
mathematics would consist of deductions of the ZFC axioms *if* it
were translated to formal logic.
Yeah.
But this translation is not (yet?) humanly possible, even with the
aid of high-level languages that are compiled into low-level formal
ZFC. One such high-level language, called MIZAR, is being
developed by my uncle, Andrzej Trybulec. To give you an idea of
how far his team has gotten, they are still working on the
piecewise linear Jordan curve theorem. (I.e., every polygon
separates the plane.) That's after building up "lemma libraries"
for 20 years with the aid of numerous assistants and collaborators.
That's cool!
This doesn't have much to do with electronic communication in
mathematics, except for the following point: While Quinn et al may
worry about losing rigor in the arXiv transition, mathematicians
have always been far away from the theoretical limit of rigor
anyway. Quinn's "electronic roadkill" thesis is a little like Wall
Street worrying that on-line trading will lead to corruption.
Hadn't heard about e-roadkill. I guess there was plenny corruption in
off-line trading already 8^0
My connection with e-communication is the analogy of proofs = source
code. Proofs in ZFC (especially MIZAR) actually are source code.
========================
Andrzej Trybulec
Institute of Computer Science
University of Bialystok
ul. Akademicka 2
Bialystok, Poland