[FOM] paper announcement

[Jeremy Avigad]

Dear friends and colleagues,

I have recently posted three items that may be of interest to FOM readers.
They are on my web page:

  http://www.andrew.cmu.edu/~avigad

First, under "Research," there is a draft of a paper called "Mathematical
method and proof." Over the years a number of postings have dealt with the
fact that, from a foundational standpoint, one may be interested in a number
of value judgments that come up in mathematics. In particular, it seems
clear that we get a lot more out of proofs than just the knowledge that the
resulting theorem is true. In this paper, I begin to develop a framework
that may help us understand how this works.

Second, under "Surveys," there is a translation of Dedekind's 1871 version
of ideal theory, to which I have added some introductory notes. Dedekind
published four versions of his theory of ideals between 1871 and 1894, and
in these developments one finds early examples of styles of reasoning
(set-theoretic, algebraic, structural, infinitary, nonconstructive, etc.)
that are taken to be hallmarks of modern mathematics. Studying these
developments is therefore helpful towards understanding how modern
mathematics came to be the way it is. 

Finally, under "Research" again, there is a preliminary version of a paper
(written with Kevin Donnelly) on the formalization of asymptotic "big O"
notation with the Isabelle proof assistant. With the help of some students
at Carnegie Mellon, I have been working on a formal proof of the prime
number theorem, and I am hopeful that it will be completed by the end of the
summer. (Since Isabelle does not yet have a complex analysis library, we are
relying on Selberg's elementary proof.) This paper describes part of that
work; there is also a project page,

  http://www.andrew.cmu.edu/~avigad/isabelle

with more details. 

Comments, corrections, and suggestions are welcome.

Jeremy Avigad