Symbolic Informalization: Fluent, Productive, Multilingual

Aarne Ranta
6/15/2026
cs.AIcs.CLcs.LO

No confident code implementation found for this paper.

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs

85% match1 repo72023

Towards a Common Framework for Autoformalization

84% match2025

FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

83% match1 repo12026

(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs

83% match2026

Trustworthy Formal Natural Language Specifications

83% match2023

Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure

82% match2025

Cite this paper

@article{ranta2026symbolic,
  title  = {Symbolic Informalization: Fluent, Productive, Multilingual},
  author = {Aarne Ranta},
  year   = {2026},
  eprint = {2606.16893},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2606.16893v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2606.16893.svg)](https://codeofpaper.com/paper/2606.16893)

Discussion