Logic List Mailing Archive

PhD student position in formal mathematics at RU Nijmegen (Netherlands; deadline July 1, 2005)

Subject: PhD position in formal mathematics at RU Nijmegen

In informal calculus, and therefore also in computer algebra
of the Maple/Mathematica kind, one encounters formulas that
only have a "fuzzy" mathematical meaning, like:

	ln(0) = -infinity
	integral(1/x,x) = ln(x) + C
	ln(1+x) = x + O(x^2)
	ln(z) = 2.3025850929... log(z)
	Ln(z) = ln(z) + 2 k pi i, with k in Z

In particular it is not clear at all what the "=" signs in these formulas
mean.  The "lack of semantics" for this kind of formulas is a real source
of problems in computer algebra systems.  It regularly causes the formula
manipulation algorithms in those programs to get confused and give wrong
or meaningless answers.

The F.E.A.R. project ("Formalizing Elementary Analysis Rigorously") has
been started to address this problem.  The core activity of this project
will be the formalization of a section of Abramowitz & Stegun using the
proof assistant HOL. The _proofs_ of the statements from that section will
_not_ be formalized, but all the definitions that are needed to phrase
those statements will be provided in full detail. The main aim of the
project is to find formal versions of those statements that are similar in
"look and feel" to their informal counterparts as much as possible.

The intended outcome of the F.E.A.R. project will be a term language that
(i) will enable users of proof assistants to formalize calculus in a way
that is much closer to informal calculus than it is today (and the aim is
to have the approach be abstract enough to be usable in all proof
assistants and not only in HOL), and that (ii) will allow a term-rewriting
based implementation of calculus in computer algebra that combines
usefulness with a rigorous semantics.

For the details of the F.E.A.R. project, see
<http://www.cs.ru.nl/~freek/notes/oc2004.ps.gz> or
<http://www.cs.ru.nl/~freek/notes/oc2004.pdf>.

For an approach for dealing with infinity in the formulas
of informal calculus, see
<http://www.cs.ru.nl/~freek/notes/limits1.ps.gz> or
<http://www.cs.ru.nl/~freek/notes/limits1.pdf>.  The research
of the F.E.A.R. project can be seen as a extension of the
topic of that paper.

WE ARE LOOKING FOR
a student with a completed Master's degree in mathematics
or computer science (preferably with a thorough knowledge of
complex function theory), who combines a strong mathematical
ability with an active interest in the computerization of
mathematics.  Experience with a proof assistant or with the
application of computer algebra to calculus will be a bonus.

WE ARE OFFERING
employment as a PhD student for four years in the group
of Henk Barendregt and Herman Geuvers (see the web page at
<http://www.cs.ru.nl/fnds/>), which is one of the foremost
research groups in formal mathematics in the world.  We have
a very enthusiastic and international team and participate
in various national and international research projects
(like Types, Calculemus, MoWGLI, MKM and Diamant.)  The PhD
position will be combined with an educational program,
and has a salary that is standard for PhD students in the
Netherlands (starting at 2,179 euro/month before taxes,
and growing to 2,517 euro/month max.)

For more information contact Freek Wiedijk <freek@cs.ru.nl>.
Reactions should be sent before July 1st, 2005.