Symbolic Informalization: Fluent, Productive, Multilingual
यह शोध पत्र इन्फॉर्मथ (Informath) प्रोजेक्ट का परिचय देता है, जो एक डेडक्टी हब (Dedukti hub) और ग्रामैटिकल फ्रेमवर्क (Grammatical Framework) पर निर्मित एक प्रतीकात्मक अनौपचारिककरण ढांचे (symbolic informalization framework) का उपयोग करता है ताकि एगडा (Agda), लीन (Lean) और रॉक (Rocq) जैसे सिस्टम के औपचारिक प्रमाणों को प्रवाहपूर्ण, सटीक और बहुभाषी प्राकृतिक भाषा में विश्वसनीय रूप से परिवर्तित किया जा सके।