I think Fredrik Johansson mentions something similar in this <https://fredrikj.net/blog/2022/04/things-i-would-like-to-see-in-a-computer-algebra-system/#section6> 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 On Sunday, May 4, 2025 at 5:26:14 PM UTC-7 asme...@gmail.com wrote: > 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 > -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/sympy/55be1472-bb92-4870-b90b-4edd1b0b64d1n%40googlegroups.com.
