Pi

A + B * Pi

例如，欲证明

$$ 14885392687-4738167652\pi\gt 0 $$

运行：

solve pi -4738167652 14885392687

输出：

Bounds   : 0, 1
Function : x**23 * (1-x)**23 * (629602886415/653752 + -1184541913/256*x + 116946872953727/20920064*x**2) / (1 + x**2)

即

$$ \int_{0}^{1} \frac{x^{23} \left(x - 1\right)^{23} \left(- 116946872953727 x^{2} + 96799580588447 x - 20147292365280\right)}{20920064 \left(x^{2} + 1\right)} \mathrm{d}x $$

显然积分结果为 $14885392687-4738167652\pi$ 且被积函数在 $[0,1]$ 上恒非负。

A + B * Pi^n

这里 n 为大于 1 的正整数。

欲证明

$$ \pi^{3}-31\gt 0 $$

运行：

solve pi_power_3 1 -31

输出：

Bounds   : 0, 1
Function : x**12 * (1091239949453/83203139250 + -240010278547/83203139250*x**2) * ln(1/x)**2 / (1 + x**2)

即

$$ \int_{0}^{1} \frac{x^{12} \left(1091239949453 - 240010278547 x^{2}\right) \log{\left(\frac{1}{x} \right)}^{2}}{83203139250 \left(x^{2} + 1\right)} \mathrm{d}x $$

欲证明

$$ 5\pi^{2}-49\gt 0 $$

运行：

solve pi_power_2 5 -49

输出：

Bounds   : 0, 1
Function : x**9 * (395/3 + -325/3*x**2) * ln(1/x)**1 / (1 + x**2)

$$ \int_{0}^{1} \frac{5 x^{9} \left(79 - 65 x^{2}\right) \log{\left(\frac{1}{x} \right)}}{3 \left(x^{2} + 1\right)} \mathrm{d}x $$