Anyone knows a software that compiles formally well-defined algebraic equations to validate their correctness?
For example, I insert a statemente in latex like that:
\forall S_i \in S \to \exists! R_i \mid R_i \subset S \land S_i \notin R_i \land |Ri| = k
It looks like ...
$$\forall S_i \in S \to \exists! R_i \mid R_i \subset S \land S_i \notin R_i \land |Ri| = k $$
and before compilation the software tells what errors encounter or if it is ok.