Проект Informath демонстрирует символическую неформализацию для преобразования формальной математики в естественный, гладкий и точный язык. В проекте используется Dedukti как центральная система доказательств и Grammatical Framework для обеспечения лингвистической корректности на нескольких языках, что позволяет получать человеко-читаемые выводы из доказательств, сгенерированных ИИ.