# [2021.06.11] JSONEncoder

One of the main problems of contemporary automated theorem provers is
their monolith architecture. For example, they all can parse problem
files in different formats, but there is no library for parsing TPTP,
SMTLib, Isar, Mizar, or anything else into a universal
language-independent format like JSON (or whatever you want). That's
a bit strange given that there exists such a format since nearly all
these provers use the standard first-order language with predicates,
functional symbols, and variables. I see in that the lack of sharing
culture in the academy. It might sound unbelievable, but researchers
don't seem to like sharing their research building blocks. Because
usually, there are none since this presumes reproducibility. But even
when the results are reproducible, it doesn't mean that they are
reusable. The result of any research is hardly ever a tool, not to
mention code libraries.