[FOM] PhD position in formal mathematics at RU Nijmegen

[Freek Wiedijk]

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 at cs.ru.nl>.
Reactions should be sent before July 1st, 2005.