Informath 0.4, July 2026
Pre-release
What's Changed
New formats for symbol table entries, e.g.
"#1 is divisible by #2" | $#2 \mid #1$
where it is also possible to drop arguments and change their order. See more examples in share/profileconstants.dkgf.
New options:
-sampling=<int>, default 2, to prune NLG results before ranking (choose e.g. 20 if too slow)-synonyms=<int>,-symbolics=<int>, to limit the number of symbol table entries for every constant, default no limit; choose 1 to speed up NLG and to force consistent terminology- file format
.dktexto informalize embedded Dedukti code inside begin/end{dedukti} environments
User-definable #SEMANTICS and #NLG rules in symbol tables, see examples; needs more work to be useful.
Normalization of judgements by variable renaming and eta expansion.
New experimental grammars constructed in interaction with an LLM, see doc/vibe/ for documentation and grammars/next/ for code. The new grammars are included in InformathFull.pgf, which thereby has 7 languages (4 written manually).
Proof linearization can now be done in special cases, try make prooftextdemo.
New larger-scale demos: Mizar, HoTT
New Contributors
- @amelieled made their first contribution in #6
Full Changelog: informath-0.3...informath-0.4
What's Changed
- Update baseconstants.dkgf by @amelieled in #6
- Improve the file README.md by @amelieled in #7
- Improve testing hierarchy structure by @amelieled in #8
- Some cleanings and improvements by @amelieled in #9
- Some details by @amelieled in #10
New Contributors
- @amelieled made their first contribution in #6
Full Changelog: informath-0.3...informath-0.4
