## Abstract

The paper presents an extension of the proof editor Alfa
with natural-language input and output.
The basis of the new functionality is an automatic translation
to syntactic structures that are closer to natural language
than the type-theoretical syntax of Alfa. These syntactic
structures are mapped into texts in languages such as English, French,
and Swedish. In this way, every theory, definition,
proposition, and proof in Alfa can be translated into a
text in any of these languages. The translation is defined
for incomplete proof objects as well, so that a text with ``holes''
(i.e. metavariables)
in it can be viewed simultaneously with a formal proof constructed.
The mappings into natural language also work in the parsing direction,
so that input can be given to the proof editor in a natural language.

The natural-language interface is implemented using the Grammatical
Framework GF, so that it is possible to change and extend the interface
without recompiling the proof editor. Such extensions can be made on
two dimensions: by adding new target languages, and by adding
theory-specific grammatical annotations to make texts more
idiomatic.