← All papers
Symbolic Informalization: Fluent, Productive, Multilingual
cs.AI
Jun 15, 2026 · v1
cs.CL cs.LO
TL;DR
Treats Lean as one source proof system in an interlingual formal-to-natural-language informalization pipeline built on Dedukti.
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 formal mathematics is hard for humans to read. Informalization, the inverse of formalization, needs to produce fluent text across multiple formal and natural languages with reasonable effort.
Approach
The paper outlines Informath, which generalizes syntactic sugar into ordinary mathematical language. It uses an interlingual architecture with Dedukti as a hub between proof systems (Agda, Lean, Rocq) and Grammatical Framework handling linguistic correctness and variation across natural languages.
Results
First results include a multilingual mathematics lexicon (about 5300 terms drawn from Wikidata and MathGloss) and a controlled-natural-language grammar that generates fluent multilingual text.