Symbolic Informalization: Fluent, Productive, Multilingual
Aarne Ranta
cs.AI
Jun 15, 2026 · v2
cs.CL cs.LO
TL;DR
Informalizes Lean code, along with Agda and Rocq code, after third-party translation to Dedukti, producing multilingual natural-language text with Grammatical Framework.
Abstract
Symbolic informalization enables a reliable conversion of formal mathematics to natural language. It has the potential to make machine-checked content human-readable without loss of precision. In a traditional proof system usage, symbolic informalization generalizes the limited mechanisms of syntactic sugar into the ordinary language of mathematics. In a setting where proofs are constructed by artificial intelligence and autoformalization, symbolic informalization can explain what precisely has been constructed. This paper outlines the project Informath, which aims to show how symbolic informalization can produce fluent text with a reasonable development effort and address multiple formal and natural languages. Informath is based on an interlingual architecture, where Dedukti works as a hub between different proof systems (Agda, Lean, Rocq) and Grammatical Framework (GF) takes care of linguistic correctness and variation in different natural languages.
Problem
Machine-checked mathematics, including AI-generated formalizations, is hard for humans to read and check against the intended statements. LLM-based informalization can hallucinate, so a precise, reliable formal-to-informal translation is needed.
Approach
Informath uses an interlingual architecture with Dedukti as a hub. Proof systems such as Agda, Lean and Rocq are converted to Dedukti by third-party tools. Grammatical Framework grammars, split into a minimal MathCore CNL and the richer MathExtensions, produce fluent text in multiple natural languages. Users adapt the system to new concepts through low-code symbol tables that map Dedukti constants to a large multilingual lexicon.
Results
The grammar is semantically complete with respect to Dedukti and has a lexicon of about 4000 words covering four languages. It has been tested on undergraduate mathematics and a subset of the '100 theorems'. Informalizing Lean, Agda and Rocq code via Dedukti works, but output is less fluent than for native Dedukti code because the conversions blow up in size and complexity.
