(c) Aarne Ranta 2025
Updated slides shown in Saclay, Prague, and some other places in 2025
The Informath project addresses the problem of translating between formal and informal languages for mathematics. It aims to translate between multiple formal and informal languages in all directions. The formal languages included are Agda, Rocq (formerly Coq), Dedukti, and Lean. The informal languages are English, French, German, and Swedish. More languages will be added later. Also the scope of language structures is at the moment theorem statements and definitions; proofs are included for the sake of completeness, but will require more work to enable more natural verbalizations.
Informath started in 2024, but it has a background of a long tradition of translating between formal and informal languages by using GF, Grammatical Framework. New relevance for this task has been created by recent attempts to "teach mathematics" to Artificial Intelligence (AI) systems. These contemporary systems, such as Google's AlphaProof, combine machine learning (e.g. large language models) with formal proof systems, to guarantee the correctness of results. In this context,
- autoformalization is automatic translation from informal to formal language
- informalization is (automatic) translation from formal to informal language
An insight that has guided GF from the beginning is that informalization is easier than autoformalization, because it goes from a restricted, semantically explicit formal notation to an open-ended, semantically often implicit natural language. Recent developments in AI have suggested something similar: one can "train" language models to formalize by providing them data generated by automatic informalization. Informath intends to become a useful source of such data. But this is so far seen as a by-product: the primary purpose of Informath is to help the users of formal proof systems to create and document formal code.
The software included in this directory supports the translation of text and code files in batch mode. For a quick start, you can just do
$ make
to build RunInformath and all its dependencies. After that, you can do
$ make demo
which illustrates different functionalities: translating between Dedukti and natural languages, as well as from Dedukti to Agda, Rocq, and Lean. Building the system requires some more software, as discribed below in Requirements.
Requirements: you need
- GF == 3.12 (both as executable and as the PGF library)
- BNFC >= 2.9 (executable)
- GHC >= 9.6 (executable, with some common libraries)
- alex (executable, tested with 3.5.4)
- happy (executable)
to do this.
For those who are interested just in the generation of synthetic data, the following commands (after building Informath with make) can do it: assuming that you have a .dk file available, build a .jsonl file with all conversions of each Dedukti judgement:
$ ./RunInformath -parallel <file>.dk > <file>.jsonl
After that, select the desired formal and informal languages to generate a new .jsonl data with just those pairs:
$ python3 test/jsonltest.py <file.jsonl> <formal> <informal>
The currently available values of <formal> and <informal> are the keys in <file>.jsonl - for example, agda and InformathEng, respectively.
The src directory contains
- Haskell and other sources
- a BNFC grammar with generated parser and printer for the proof system Dedukti
- partial BNFC grammars of Agda, Rocq, and Lean in typetheory with generated parsers and printers
- a translator from MathCore to Dedukti and vice-versa
- translations between MathCore and Informath
- BaseConstants.dk of logical and numeric operations assumed in the translations, and correspoonding files for Agda, Rocq, and Lean
- base_constant_data.dkgf, a symbol table for converting Dedukti constants to GF abstract syntax functions (read from this file by the conversion program)
- some test material and scripts in test/.
The grammars directory contains
- MathCore, a minimal CNL for mathematics
- MathCoreEng, Fre, Swe - concrete syntaxes of MathCore in grammars.
- Informath, an extension of MathCore with alternative expressions
The structure of the project is shown in the following picture:
(to be updated with Rocq and German). Here is an example statement involving all of the currently available languages. The Dedukti statement has been used as the source of all the other formats. Both MathCore and Informath could also be used as source, by parsing them and converting to Dedukti.
Dedukti: prop110 : (a : Elem Int) -> (c : Elem Int) ->
Proof (and (odd a) (odd c)) ->
Proof (forall Int (b => even (plus (times a b) (times b c)))).
MathCoreEng: Prop110. Let
InformathEng: Let
MathCoreFre: Prop110. Soient
InformathFre: Prop110. Soient
MathCoreSwe: Prop110. Låt
InformathSwe: Prop110. Låt
Agda: postulate prop110 : (a : Int) -> (c : Int) ->
and (odd a) (odd c) ->
all Int (\ b -> even (plus (times a b) (times b c)))
Rocq: Axiom prop110 : forall a : Int, forall c : Int,
(odd a /\ odd c -> forall b : Int, even (a * b + b * c)) .
Lean: axiom prop110 (a c : Int) (x : odd a ∧ odd c) :
∀ b : Int, even (a * b + b * c)
MathCore renderings are designed to be unique for each Dedukti judgement. But the full Informath language recognizes several variations. Here are some of them for English, as generated by the system; other languages have equivalents of each of them:
- Prop110. For all integers
$a$ and$c$ , if$a$ is odd and$c$ is odd, then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a$ and$c$ be integers. Then if$a$ is odd and$c$ is odd, then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a , c \in Z$ . then if$a$ is odd and$c$ is odd, then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a$ and$c$ be integers. Assume that$a$ is odd and$c$ is odd. Then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a , c \in Z$ . assume that$a$ is odd and$c$ is odd. Then for all integers$b$ ,$a b + b c$ is even. - Prop110. For all integers
$a$ and$c$ , if both$a$ and$c$ are odd, then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a$ and$c$ be integers. Then if both$a$ and$c$ are odd, then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a , c \in Z$ . then if both$a$ and$c$ are odd, then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a$ and$c$ be integers. Assume that both$a$ and$c$ are odd. Then for all integers$b$ ,$a b + b c$ is even. - Prop110. Let
$a , c \in Z$ . assume that both$a$ and$c$ are odd. Then for all integers$b$ ,$a b + b c$ is even. Prop110. Let$a , c \in Z$ . assume that both$a$ and$c$ are odd. Then$a b + b c$ is even for all integers$b$ .
Dedukti is a minimalistic logical framework aimed as an interlingua between different proof systems such as Agda, Rocq (formerly Rocq), Isabelle, and Lean. Its purpose is to help share formalizations between these systems. Dedukti comes with an efficient proof checker and evaluator. Translations from many other proof system to Dedukti have been built, and this work is ongoing.
Technically, Dedukti is described as an implementation of Lambda-Pi-calculus with rewrite rules. It is similar to Martin-Löf's logical framework from the 1980's, except for a more liberal syntax of rewrite rules. Thereby, it is also similar to the ALF system of 1990's and to the abstract syntax of GF, Grammatical Framework.
Due to its simplicity and expressivity, together with an existing implementation and conversions, we have chosen Dedukti as the interlingua for other proof systems.
Agda, Rocq, and Lean are type-theoretical proof systems just like Dedukti. But all of them have a richer syntax than Dedukti, because they are intended to be hand-written by mathematicians and programmers, whereas Dedukti has an austere syntax suitable for automatic generation for code.
Translators from each of Agda, Rocq, and Lean to Dedukti are available, and we have no plans to write our own ones. However, translators from Dedukti to these formalisms are included in the current directory. They are very partial, because they only have to target fragments of the Agda, Rocq, and Lean. This is all we need for the purpose of autoformalization, if the generated code is just to be machine-checked and not to be read by humans.
However, if Informath is to be used as an input tool by Agda, Rocq, and Lean users, nice-looking syntax is desirable. In the case of Rocq and Lean, we have tried to include some syntactic sugar, such as infix notations. In Agda, this has not yet been done, partly because the syntactic sugar is not as standardized as in Rocq and Lean.
Another caveat is that Dedukti is, by design, more liberal than the other systems. Type checking of code generated from type-correct Dedukti code can therefore fail in them. This can sometimes be repaired by inserting extra code such as coercions, but this is still mostly future work.
The MathCore language is meant to be the "core abstract syntax" in Informath. Technically, it is actually a subset of Informath: Informath is implemented as an extension of MathCore.
As shown in the picture above, informalization and autoformalization are in the first place defined between Dedukti and MathCore. On the type theory side, this is composed with translations between other frameworks and Dedukti. On the natural language side, mappings between MathCore and the full Informath are defined on the abstract syntax level of these languages. Input and output of actual natural languages is performed by generation and parsing with concrete syntaxes of each language.
Following Informath Version 2, we first investigated was to keep MathCore and "extensions" as two separate languages, where the extensions are provided by the ForTheL-based grammar in this project. However, the long distance between the abstract syntaxes of MathCore and ForTheL soon made us change our mind and replace ForTheL by a proper extension (in the technical sense of GF) of MathCore, subsequently called Informath.
While being inspired by ForTheL and covering a similar fragment of English, the Informath grammar differs from the original ForTheL in several ways:
- Grammaticality: Informath follows the agreement rules of English (and other languages) instead of allowing free variation of e.g. singular and plural forms; this makes it better usable as the target of informalization.
- Ambiguity: ForTheL prevents syntactic ambiguities by means of devices such as brackets. Informath tries to capture all syntactic ambiguities that exist in natural language, and delegates it to the logical framework to resolve them by semantic clues. This is in line with the findings in The language of Mathematics by Mohan Ganesalingam.
- LaTeX: The original ForTheL is plain text, whereas Informath (like some other later versions of ForTheL) allows the full use of LaTeX similar to usual mathematical documents; this is one of the
- Extensions: Informath is open for extensions with new forms of expression when encountered in mathematical text. In ForTheL, new concepts can be defined, but the overall syntax is fixed. Because of the design of Informath, every extension should be equipped with a new semantic rule that converts it to MathCore.
- Omissions: Informath is not guaranteed to cover all of the original ForTheL. In particular, constructs that differ from grammatical English are usually omitted.
- Multilinguality: Informath will have several concrete syntaxes sharing a common abstract syntax, reusing the ForTheL grammars in v2.
The MathCore language shares some features with Informath: grammaticality, LaTeX support, and extensibility (with a lexicon). But the other features are delegated to Informath via the NLG function.
MathCore is a minimalistic grammar for mathematical English, with other languages added via a functor on GF Resource Grammar Library. It is based on the following principles:
- Completeness: all Dedukti code can be translated to MathCore.
- Non-ambiguity: all MathCore text has a unique parse tree and a unique translation to Dedukti.
- Losslessness: Core is a lossless representation of Dedukti; that is, all Dedukti code translated to MathCore can be translated back to the same Dedukti code (modulo some differences yet to be specified).
- Traceability: Dedukti code and MathCore text can be aligned part by part.
- Grammaticality: MathCore text is grammatically correct natural language (with mathematical symbols and some mark-up to prevent ambiguity).
- Naturalness: MathCore supports natural expressions for mathematical concepts using nouns, adjectives, verbs, and other structures conventionally used in mathematical text.
- Minimality: MathCore is defined to have exactly one way to express each Dedukti judgement. Alternative ways are provided in Informath via NLG. Typically, the unique way is the most straightforward one. For example, complex mathematical expressions are given in their verbal forms ("the sum of x and y") rather than formulas ("x + y"), because formulas are not available when any of the constituents if not formal ("x + the successor of y").
- Extensibility: MathCore can be extended with lexical information assigning natural language verbalizations to Dedukti identifiers.
- Multilinguality: MathCore has been implemented by GF RGL and is therefore ready for concrete syntax in other languages than English. French and Swedish are already included.
The following propertes are, however, not expected:
- Type correctness: MathCore text can be semantically invalid, leading to syntactically correct Dedukti code that is rejected by Dedukti's type checker.
- Fluency: MathCore text can be repetitive and even hard to read; making it better is delegated to the Informath grammar via the NLG component.
- Compositionality: The translation between Dedukti and MathCore is not compositional in the strict sense of GF, as the two languages have different abstract syntaxes. For example, Core supports the aggregation of conjuncts and function argument lists, without which it would be even less readable; and the basic type system is richer than in Dedukti, for instance distinguishing between expressions that represent kinds, objects, and propositions.
- Easy natural language input: while the grammar of MathCore is reversible, it is tedious to write MathCore. It is intended to be produced indirectly: by conversion from Dedukti on one hand and Informath on the other.
The rationale of this design is modularity and an optimal use of existing resources:
- Type checking is delegated to Dedukti.
- Conversions to different frameworks are also delegated to Dedukti.
- Variation of natural language input and output is delegated to Informath.
The following programming languages have been used so far in Informath:
- GF: Grammatical Framework used for implementing MathCore and Informath, maximally using its Resource Grammar Library (RGL). You need to install both gf-core and gf-rgl.
- Haskell: used for writing conversions between formal and informal, via embedded GF grammars in the GADT format (Generalized Algebraic Datatypes) supporting almost compositional functions in NLG.
- BNFC: BNF Converter, used for implementing Dedukti. The implementation includes a parser, a printer, and an abstract syntax in Haskell, all generated from this BNF grammar. Also used for the fragments of Agda and Lean addressed in the project.
If you want to check the formal code in any of the proof systems, you must also install them. Informath itself does not require them, but at least Dedukti is useful to have so that you can check the input and output Dedukti code.
In order for this to work, you need to compile the formal (Dedukti, Agda, Rocq, Lean) and the Informath grammars:
$ make
An example of a readily available demo case is
$ make demo
Consult the Makefile to see what these commands exactly do.
It is too early to document the usage of this software, because its user interface has not yet stabilized.
The emerging interface is in the file RunInformath.hs. Its two modes are interactive shell and conversion of files.
Write
$ ./RunInformath -help
to see the currently available functionalities.
Under construction, not guaranteed always to work like this
The lexicon part part of the GF grammar (files grammars/BaseConstants*, UserConstants*) give verbalizations to defined constants in .dk files. The UseConstants* files can be dynamically generated with the command
$ ./RunInformath <file>.dkgf
which with the default lang=Eng generates at least two files:
- UserConstants.gf
- UserConstantsEng.gf and similarly for other languages addressed in the .dkgf file
after which
$ make Informath.pgf
and compiles Informath.pgf with them. The format of .dkgf files is a list of lines with data about constants, where user-defined ones have the forms
<dkid> NEW <project> <gfcat> <gffun> <int>* =
#LIN <lang> <gffun> = <word>+
This generates new entries in the two UserConstants*.gf files (abstract and concrete) and also instructs RunInformath how to handle the constant in translations to and from GF.
The label can be chosen freely by the user; it is appended to each generated GF abstract rule as a comment that can be grepped with.
The * part is a space-separated list of integers telling which arguments (numbered from 0) are sent to GF and in what order. It provides a way to deal with hidden arguments. Leaving it out means that all arguments are sent.
Users can also map their Dedukti identifiers to already existing ones in BaseConstants.dk. This is performed with a simpler form of lines in .dkgf files,
<dkid> ALIAS <project> <dkid> <int>*
stating that the former dkid should be treated in the same way as the latter one in GF.
In addition to information for GF, .dkgf files can contain information about conversions of constants from Dedukti to the other type theories, whenever the constant names or their argument lists need to be changed; see below.
The following categories of new constants are currently supported by the grammar and can appear in the field of .dkgf files:
-- GF cat usage example
—-------------------------------------------------------------------
Noun ; -- Kind -- set
Fam ; -- Kind -> Kind -- list of integers
Adj ; -- Exp -> Prop -- even
Verb ; -- Exp -> Exp -- converge
Reladj ; -- Exp -> Exp -> Prop -- divisible by
Relverb ; -- Exp -> Exp -> Prop -- divide
Relnoun ; -- Exp -> Exp -> Prop -- root of
Name ; -- Exp -- contradiction
Fun ; -- [Exp] -> Exp -- radius of
Label ; -- Exp -- theorem 1
Set ; -- Kind | Term -- integer, Z
Const ; -- Exp | Term -- the empty set, Ø
Oper ; -- Exp -> Exp -> Exp | Term -- the sum of, +
Compar ; -- Exp -> Exp -> Prop | Formula -- greater than, >
Comparnoun ; -- Exp -> Exp -> Prop | Formula -- a subset of, \sub
Pred3 ; -- Exp -> Exp -> Exp -> Prop -- congruent to y modulo m
The type checking is based on the file BaseConstants.dk, which is meant to be extended as the project grows. This file type checks in Dedukti with the command
$ dk check BaseConstants.dk
The example file test/exx.dk assumes this file. As shown in make demo, it must at the moment be appended to the base file to type check:
$ cat BaseConstants.dk test/exx.dk >bexx.dk
$ dk check bexx.dk
Since this is cumbersome, we will need to implement something more automatic in the future. We also plan to use Dedukti for type selecting among ambiguous parse results by type checking, and Lambdapi (a syntactically richer version of Dedukti with implicit arguments) to restore implicit arguments.
Each of Agda, Rocq, and Lean will be described below. A common feature to all of them are the conversion rules of constants stored in BaseConstants.dk, with the format as in
#CONV Agda forall all
#CONV Rocq forall All
#CONV Lean forall All
The purpose of these conversions is to
- avoid clashes of the target systems' reserved words
- map Dedukti to standard libraries of these systems
- comply to the identifier syntax of each system
The last purpose might be better served by a generic conversion, but that remains to be done.
There a simple generation of Agda from Dedukti. At the moment, it is only reliable for generating Agda "postulates". The usage is
$ ./RunInformath -to-agda <file>
where the file can be either a .dk or a text file.
As shown by make demo, this process can produce valid Agda code:
$ ./RunInformath -to-agda test/exx.dk >exx.agda
$ agda --prop exx.agda
The base file BaseConstants.agda is imported automatically.
Generation from Dedukti is similar to Agda, but type checking requires at the moment concatenation with BaseConstants.v:
$ ./RunInformath -to-coq test/exx.dk >exx.v
$ cat BaseConstants.v exx.v >bexx.v
$ coqc bexx.lean
This should be made less cumbersome in the future.
Just like in Rocq, type checking requires at the moment concatenation with BaseConstants.lean:
$ ./RunInformath -to-lean test/exx.dk >exx.lean
$ cat BaseConstants.lean exx.lean >bexx.lean
$ lean bexx.lean
This should be made less cumbersome in the future.
- improve conversions from Dedukti to other proof systems in particular to preserve type correctness
- extend the MathCore-Informath conversion
- investigate the possibility of a declarative, user-defined extension of MathCore-Informath conversion
- improve the concrete syntaxes of different languages by functor exceptions
- add concrete syntaxes to yet other natural languages
- extend the Informath language, in particular, with
- proofs, in addition to theorems and definitions to proofs (complete in theory, but very rudimentary now)
- wider coverage of BaseConstants.dk and the multilingual lexicon of math terms