It should be noted that this is a PR piece for a "math" startup. The result doesn't look particularly interesting, from either a mathematical or Lean code standpoint, as far as I can see.