Nice. Is the lean used to formalize formulas?

Sort of. The formulas for each line live in the form YAML I described above. The formulas are built out of a set of primitive operations that are defined in lean, with their properties proved there (non-negativity, monotonicity, etc.). There's also a lean evaluator that's run on compiled form data and cross checked with the typescript evaluator. (There's a lot more detail in the README.)