Informath: Informalization and Autoformalization of Formal Mathematics

LATEST NEWS

24 July 2026: New binary release, entitled Informath-0.4.

22 July 2026: also verbal constants can now be defined with # variables, which enables permutations, as well as drops without the #DROP directive. See the alternative symbol table for examples.

10 July 2026: an experiment on porting the Informath grammar to new languages (Finnish and Czech) by help from Claude code. The process is documented in the vibe directory. NOTICE: these grammars are not yet an "official" part of Informath but need checking for known and still unknown bugs.

22 June 2026: macros in symbol tables now directly possible in entries of form $...$ , e.g. $#1 \mid #2$ , from which a macro is generated automatically; see test/profiletest.dkgf

15 June 2026: a lengthy paper on Informath in arXiv: Symbolic Informalization: Fluent, Productive, Multilingual. At the moment, this is the most up-to-date description on some features of Informath.

9 June 2026: moved experimental and/or deprecated code to a separate repository, called informath-experiments.

6 May 2026: New binary release, entitled Informath-0.3.

15 April 2026: Generalized production of synonyms, regulated by new flags -synonyms=<int> and -symbolics=<int>. Value 1 is reasonable for both of them: it means that just one verbal and one symbolic synonym is taken from the symbol table. Otherwise, the number of variations can now grow very large. Even without the -variations flag, this can make generation slow. In many demos accessible by Makefile, these flag values are used, but they can be overridden.

4 March 2026: Binary release, entitled Informath-0.2.

Older news

Documentation

Symbolic Informalization: Fluent, Productive, Multilingual. As of June 2026, the most up-to-date description on some features of Informath.

The Informath Deployment stack slides from workshops in Gothenburg and Nancy, May and June 2026. They give examples of using Informath on different levels of adaptation, starting with just the command line and the existing binary.

This README: using Informath with ready-made binaries and grammars.

The vibe directory containing LLM-generated documentation on LLM-generated experimental grammars.

Informath Under the Hood. Recommended if you want to change the GF grammar and not just the symbol table. However, not completely up to date as of 2026-07-24.

Informalization of Advanced Mathematics: A Case Study with Homotopy Type Theory. Presentation by May Ohlsson and Aarne Ranta in Types 2026.

Video from MCLP conference at Institut Pascal, Paris Saclay, September 2025

Updated slides shown in Saclay, Prague, and some other places in 2025

InformathAPI haddock-generated documentation

Symbolic Informalization: Fluent, Productive, Multilingual (by A. Ranta, AITP-2025, extended abstract)

Multilingual Autoformalization via Fine-tuning Large Language Models with Symbolically Generated Data, by Pei Huang, Nicholas Smallbone and Aarne Ranta, SCML Vol. 1, 2025.

The Informath project

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:

formal to informal (informalization)
informal to formal (autoformalization)
informal to informal (translation, via formal)
formal to formal (works in special cases)

The formal languages included are Agda, Rocq (formerly Coq), Dedukti, and Lean. The informal languages are English, French, German, and Swedish.

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.

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)))).
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)

English: Prop110. Let