Symbolic Informalization: Fluent, Productive, Multilingual
2026-06-15 • Artificial Intelligence
Artificial IntelligenceComputation and LanguageLogic in Computer Science
AI summaryⓘ
The authors describe a project called Informath that helps turn precise formal math proofs into clear, natural language text without losing accuracy. They use a system where Dedukti acts as a bridge between different formal proof systems, and Grammatical Framework ensures the natural language is correct and varied. This approach aims to make machine-generated proofs easier for humans to understand and works with multiple languages and proof tools. Essentially, the authors show a way to explain complex formal math in a way people can read naturally.
symbolic informalizationformal mathematicsnatural language generationDeduktiGrammatical Frameworkproof systemsAgdaLeanRocqautoformalization
Authors
Aarne Ranta
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.