Terry Tao estimates package

[Aaron Meurer]

Terry Tao has posted a proof-of-concept Python tool that can be used
to prove asymptotic inequalities. See
https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/
and https://github.com/teorth/estimates.

There was some discussion on the blog post about whether it would make
sense for his tool to be using SymPy (it most likely should), and he
also expressed some interest in possibly integrating his tool into
SymPy.

The thing that isn't yet clear to me is whether a tool that proves
asymptotic inequalities would be useful for SymPy. I know that we
definitely need better support in the assumptions system for making
use of *inequalities*, but, for instance, would knowing that X = O(Y)
(X is bounded by a constant times Y) be useful?

I'm posting about this here so that people are aware of it, but you
should probably comment on Terry Tao's blog post if you want to
discuss the project with him.

Aaron Meurer

[Tilo RC]

I think Fredrik Johansson mentions something similar in this blog post but I could be wrong:

> Good for inequalities
> This is a rather specific feature request. Any CAS will let me compute some terms of Stirling's series for Γ(z). How come I can't get a truncation of Stirling's series with an explicit error term? Analysis-oriented CASes are generally good at manipulating equalities and limits, but strangely poor at manipulating inequalities. This is bizarre since inequalities are at least as important as equalities in analysis!

This is the same sort of thing Terry Tao's blog post is about, right?

Tilo Reneau-Cardoso