著者は、推定の自動検証ツールを改良し、対話型で柔軟な証明支援ツールへと進化させた。Lean風のインターフェースを持ち、Pythonのsympyを利用して線形不等式や漸近推定を処理できる。ユーザーは高レベルの「戦術」を指定し、ツールが計算を行う。今後は関数空間ノルムの評価や不等式の導入も視野に入れており、さらなる拡張が期待される。実装はGitHub上で公開されており、数理解析や論理に関心のある開発者に有用だ。