Initial commit

.gitattributes

@@ -0,0 +1,35 @@
+*.7z filter=lfs diff=lfs merge=lfs -text
+*.arrow filter=lfs diff=lfs merge=lfs -text
+*.bin filter=lfs diff=lfs merge=lfs -text
+*.bz2 filter=lfs diff=lfs merge=lfs -text
+*.ckpt filter=lfs diff=lfs merge=lfs -text
+*.ftz filter=lfs diff=lfs merge=lfs -text
+*.gz filter=lfs diff=lfs merge=lfs -text
+*.h5 filter=lfs diff=lfs merge=lfs -text
+*.joblib filter=lfs diff=lfs merge=lfs -text
+*.lfs.* filter=lfs diff=lfs merge=lfs -text
+*.mlmodel filter=lfs diff=lfs merge=lfs -text
+*.model filter=lfs diff=lfs merge=lfs -text
+*.msgpack filter=lfs diff=lfs merge=lfs -text
+*.npy filter=lfs diff=lfs merge=lfs -text
+*.npz filter=lfs diff=lfs merge=lfs -text
+*.onnx filter=lfs diff=lfs merge=lfs -text
+*.ot filter=lfs diff=lfs merge=lfs -text
+*.parquet filter=lfs diff=lfs merge=lfs -text
+*.pb filter=lfs diff=lfs merge=lfs -text
+*.pickle filter=lfs diff=lfs merge=lfs -text
+*.pkl filter=lfs diff=lfs merge=lfs -text
+*.pt filter=lfs diff=lfs merge=lfs -text
+*.pth filter=lfs diff=lfs merge=lfs -text
+*.rar filter=lfs diff=lfs merge=lfs -text
+*.safetensors filter=lfs diff=lfs merge=lfs -text
+saved_model/**/* filter=lfs diff=lfs merge=lfs -text
+*.tar.* filter=lfs diff=lfs merge=lfs -text
+*.tar filter=lfs diff=lfs merge=lfs -text
+*.tflite filter=lfs diff=lfs merge=lfs -text
+*.tgz filter=lfs diff=lfs merge=lfs -text
+*.wasm filter=lfs diff=lfs merge=lfs -text
+*.xz filter=lfs diff=lfs merge=lfs -text
+*.zip filter=lfs diff=lfs merge=lfs -text
+*.zst filter=lfs diff=lfs merge=lfs -text
+*tfevents* filter=lfs diff=lfs merge=lfs -text

.gitignore

@@ -0,0 +1,10 @@
+.idea/
+.vscode/
+workdir/mathjax-full/
+workdir/res.html
+workdir/pre/mma2sympy_input.txt
+workdir/pre/mma2sympy_output.py
+pre.nb
+*__pycache__*
+test.*
+rename.sh

README.md

@@ -0,0 +1,12 @@
+---
+title: Note that * QED
+emoji: 🤓
+colorFrom: indigo
+colorTo: green
+sdk: gradio
+sdk_version: 5.22.0
+app_file: app.py
+pinned: false
+license: mit
+short_description: Compare sizes by 'Note that' proof
+---

app.py

@@ -0,0 +1,221 @@
+import os
+import gradio as gr
+from solution import solutions
+from sympy.core.numbers import Rational
+
+EN_US = os.getenv("LANG") != "zh_CN.UTF-8"
+ZH2EN = {
+    "# “注意到”证明法比较大小": "# Compare sizes by 'Note that' proof",
+    "比较 e^(m/n) 与 u/v 大小": "Compare e^(m/n) and u/v",
+    "分母不能为 0": "The denominator cannot be 0",
+    "比较 π^n 与 p/q 大小": "Compare π^n and p/q",
+    "比较 e 与 p/q 大小": "Compare e and p/q",
+    "比较 π 与 p/q 大小": "Compare π and p/q",
+    "#### 证明结果": "#### Proof result",
+    "注意到": "Note that",
+    "状态栏": "Status",
+    "证毕!": "QED",
+}
+
+
+def _L(zh_txt: str):
+    return ZH2EN[zh_txt] if EN_US else zh_txt
+
+
+def generate_md(args_dict, name):
+    ans_latex = solutions[name](**args_dict).get_latex_ans()
+    return f"{_L('注意到')} $${ans_latex}$$ {_L('证毕!')}"
+
+
+def float_to_fraction(x):
+    x_str = "{0:.10f}".format(x).rstrip("0").rstrip(".")  # 移除小数点后的无效零
+
+    # 检查是否为整数
+    if "." not in x_str:
+        return Rational(x_str), Rational(1)
+
+    # 分割整数部分和小数部分
+    integer_part, decimal_part = x_str.split(".")
+    decimal_digits = len(decimal_part)
+
+    # 构造分子和分母
+    numerator = int(integer_part + decimal_part)
+    denominator = 10**decimal_digits
+
+    # 简化分数
+    gcd_value = 1
+    a = numerator
+    b = denominator
+    while b != 0:
+        a, b = b, a % b
+        gcd_value = a
+
+    p = Rational(numerator // gcd_value)
+    q = Rational(denominator // gcd_value)
+    return p, q
+
+
+def infer_pi(p, q):
+    status = "Success"
+    proof = None
+    try:
+        if q == 0:
+            raise ValueError(_L("分母不能为 0"))
+
+        p, q = float_to_fraction(p / q)
+        args_dict = {"p": p, "q": q}
+        proof = generate_md(args_dict, "π")
+
+    except Exception as e:
+        status = f"{e}"
+
+    return status, proof
+
+
+def infer_e(p, q):
+    status = "Success"
+    proof = None
+    try:
+        if q == 0:
+            raise ValueError(_L("分母不能为 0"))
+
+        p, q = float_to_fraction(p / q)
+        args_dict = {"p": p, "q": q}
+        proof = generate_md(args_dict, "e")
+
+    except Exception as e:
+        status = f"{e}"
+
+    return status, proof
+
+
+def infer_eq(q1, q2, u, v):
+    status = "Success"
+    proof = None
+    try:
+        if q2 == 0 or v == 0:
+            raise ValueError(_L("分母不能为 0"))
+
+        q1, q2 = float_to_fraction(q1 / q2)
+        u, v = float_to_fraction(u / v)
+        args_dict = {"q1": q1, "q2": q2, "u": u, "v": v}
+        proof = generate_md(args_dict, "e^q")
+
+    except Exception as e:
+        status = f"{e}"
+
+    return status, proof
+
+
+def infer_pin(n: int, p, q):
+    status = "Success"
+    proof = None
+    try:
+        if q == 0:
+            raise ValueError(_L("分母不能为 0"))
+
+        p, q = float_to_fraction(p / q)
+        args_dict = {"n": n, "p": p, "q": q}
+        proof = generate_md(args_dict, "π^n")
+
+    except Exception as e:
+        status = f"{e}"
+
+    return status, proof
+
+
+if __name__ == "__main__":
+    os.chdir(os.path.dirname(__file__))
+    for file_name in os.listdir("solutions"):
+        if not file_name.endswith(".py"):
+            continue
+
+        __import__(f"solutions.{file_name[:-3]}")
+
+    with gr.Blocks() as demo:
+        gr.Markdown(_L("# “注意到”证明法比较大小"))
+        with gr.Tabs():
+            with gr.TabItem("π"):
+                gr.Interface(
+                    fn=infer_pi,
+                    inputs=[
+                        gr.Number(label="p", value=314),
+                        gr.Number(label="q", value=100),
+                    ],
+                    outputs=[
+                        gr.Textbox(label=_L("状态栏"), show_copy_button=True),
+                        gr.Markdown(
+                            value=_L("#### 证明结果"),
+                            show_copy_button=True,
+                            container=True,
+                            min_height=122,
+                        ),
+                    ],
+                    title=_L("比较 π 与 p/q 大小"),
+                    flagging_mode="never",
+                )
+
+            with gr.TabItem("e"):
+                gr.Interface(
+                    fn=infer_e,
+                    inputs=[
+                        gr.Number(label="p", value=2718),
+                        gr.Number(label="q", value=1000),
+                    ],
+                    outputs=[
+                        gr.Textbox(label=_L("状态栏"), show_copy_button=True),
+                        gr.Markdown(
+                            value=_L("#### 证明结果"),
+                            show_copy_button=True,
+                            container=True,
+                            min_height=122,
+                        ),
+                    ],
+                    title=_L("比较 e 与 p/q 大小"),
+                    flagging_mode="never",
+                )
+
+            with gr.TabItem("e^q"):
+                gr.Interface(
+                    fn=infer_eq,
+                    inputs=[
+                        gr.Number(label="m", value=3),
+                        gr.Number(label="n", value=4),
+                        gr.Number(label="u", value=2117),
+                        gr.Number(label="v", value=1000),
+                    ],
+                    outputs=[
+                        gr.Textbox(label=_L("状态栏"), show_copy_button=True),
+                        gr.Markdown(
+                            value=_L("#### 证明结果"),
+                            show_copy_button=True,
+                            container=True,
+                            min_height=122,
+                        ),
+                    ],
+                    title=_L("比较 e^(m/n) 与 u/v 大小"),
+                    flagging_mode="never",
+                )
+
+            with gr.TabItem("π^n"):
+                gr.Interface(
+                    fn=infer_pin,
+                    inputs=[
+                        gr.Number(label="n", value=3, step=1),
+                        gr.Number(label="p", value=31),
+                        gr.Number(label="q", value=1),
+                    ],
+                    outputs=[
+                        gr.Textbox(label=_L("状态栏"), show_copy_button=True),
+                        gr.Markdown(
+                            value=_L("#### 证明结果"),
+                            show_copy_button=True,
+                            container=True,
+                            min_height=122,
+                        ),
+                    ],
+                    title=_L("比较 π^n 与 p/q 大小"),
+                    flagging_mode="never",
+                )
+
+    demo.launch()

output_util.py

@@ -0,0 +1,14 @@
+from sympy import latex
+
+
+def to_latex(expr, is_coeff=False):
+    return "" if is_coeff and expr == 1 else f"{{{latex(expr)}}}"
+
+
+def to_latexes(*args, is_coeff=False):
+    return [to_latex(i, is_coeff=is_coeff) for i in args]
+
+
+sign2cmp = {1: ">", -1: "<"}
+
+sign2cmp_inv = {1: "<", -1: ">"}

requirements.txt

@@ -0,0 +1,3 @@
+sympy~=1.12
+pywebview~=5.3.2
+ttkbootstrap~=1.10.1

sgntools.py

@@ -0,0 +1,34 @@
+def sgns(*args):
+    for i in args:
+        if i < 0:
+            break
+    else:
+        return 1
+
+    for i in args:
+        if i > 0:
+            break
+    else:
+        return -1
+
+    return 0
+
+
+def sq_func_sgn(a, b, c):
+    r"""
+    let f(x) = a+bx+cx^2, x \in [0, 1]
+    :return: f(x)>=0? 1; f(x)<=0? -1; 0
+    """
+    f0 = a
+    f1 = a + b + c
+    fm = 0
+    if c != 0:
+        x_m = -b / (2 * c)
+        if 0 <= x_m <= 1:
+            fm = a + b * x_m + c * x_m**2
+
+    return sgns(f0, f1, fm)
+
+
+def lin_func_sgn(a, b):
+    return sgns(a, a + b)

solution.py

@@ -0,0 +1,132 @@
+from typing import Iterable, Callable
+from sympy import Eq, Expr, Symbol, linsolve, simplify, latex
+
+
+class CannotCalculate(Exception):
+    pass
+
+
+class BadInput(Exception):
+    pass
+
+
+CONSTANT_TERM_KEY = "constant_term"
+
+
+class GetIntegrate:
+    integrate_result_classes: dict[str, Expr | None]
+
+    def integrate_and_separate(
+        self, integrate_formula: Expr, integrate_args: tuple
+    ) -> dict[str, Expr]:
+        """
+        解积分，分离各项
+        """
+        raise NotImplementedError(
+            "该函数已弃用，请使用 GetIntegrateFromData 类。如果想要使用它预处理，见 pre/old_solution.py"
+        )
+
+    def get_integrate_args(self, try_arg):
+        """
+        :return: integrand_function, (independent_variable, lower_limit, upper_limit)
+                被积函数, (自变量, 下限, 上限)
+        """
+        raise NotImplementedError()
+
+    def tries(self, try_arg):
+        """
+        :return: {term_name: coefficient_of_the_term}
+                {该项的名称: 该项系数}
+        """
+        return self.integrate_and_separate(*self.get_integrate_args(try_arg))
+
+    def get_latex(self, try_arg, subs):
+        expr, args = self.get_integrate_args(try_arg)
+        expr = simplify(expr).subs(subs)
+        sym, low, high = args
+        return r"\int_{%s}^{%s} {%s} \mathrm{d} {%s}" % (
+            low,
+            high,
+            latex(simplify(expr)),
+            sym,
+        )
+
+
+class GetIntegrateFromData(GetIntegrate):
+    data: dict[object, dict[str, Expr]]
+
+    def tries(self, try_arg):
+        return self.data[try_arg]
+
+
+class Solution:
+    get_integrate: GetIntegrate
+    # gui: Pattern
+
+    get_tries_args: Callable[[], Iterable[Expr]]
+    """
+    Generate try_arg for each trial
+    生成每一次尝试的 try_arg
+    """
+
+    symbols: tuple[Symbol, ...]
+    """
+    The undetermined variable to solve.
+    要求的待定系数
+    """
+
+    integrate_result_classes_eq: dict[str, Expr]
+    """
+    {term_name: coefficient}
+    The value to which each term's coefficient is equal.
+    每个项系数分别要等于的值
+    """
+
+    check_sgn: Callable
+    """
+    Input: unpacked solution of undetermined variables; 
+    Output: 0 (cannot determine), 1 or -1 (can determine; 1 and -1 are interchangeable for greater or less than).
+    Module sgntools provides lin_func_sgn and sq_func_sgn. Call help() for further details.
+    
+    输入：解包的待定系数的值列表；
+    输出: 0(无法确定), 1或-1(可以确定, 1和-1哪个代表大于、哪个代表小于, 是可以互换的)
+    sgntools 模块提供了 lin_func_sgn 和 sq_func_sgn 函数，详见 help()
+    """
+    # check_sgn: Callable[?, 1 | 0 | -1]
+
+    def get_symbols(self, separate_result):
+        """凑积分结果系数"""
+        system = [
+            Eq(int_term, self.integrate_result_classes_eq[key])
+            for key, int_term in separate_result.items()
+        ]
+        print(f"{system=}")
+        return linsolve(system, *self.symbols)
+
+    def try_times(self) -> tuple[Expr, dict, int] | tuple[None, None, None]:
+        for try_arg in self.get_tries_args():
+            separate = self.get_integrate.tries(try_arg)
+            for symbol_solution in self.get_symbols(separate):
+                if sgn := self.check_sgn(*symbol_solution):
+                    return try_arg, dict(zip(self.symbols, symbol_solution)), sgn
+
+        return None, None, None
+
+    def get_latex_ans(self):
+        """
+        :return: None if it can't be solved; Otherwise, LaTeX (without "$$")
+        """
+        raise NotImplementedError()
+
+
+# 插件注册（历史遗留问题）
+solutions = {}
+solution_sort = []
+
+
+def register(name, solution, top=False):
+    solutions[name] = solution
+    if top:
+        solution_sort.insert(0, name)
+    else:
+        solution_sort.append(name)

solutions/e.py

@@ -0,0 +1,68 @@
+from sympy import *
+from sympy.abc import a, b, x
+from output_util import to_latex, sign2cmp
+from sgntools import lin_func_sgn
+from solution import *
+
+_data = {
+    1: {"constant_term": 3 * a - 8 * b, "e_term": -a + 3 * b},
+    2: {"constant_term": -38 * a + 174 * b, "e_term": 14 * a - 64 * b},
+    3: {"constant_term": 1158 * a - 7584 * b, "e_term": -426 * a + 2790 * b},
+    4: {"constant_term": -65304 * a + 557400 * b, "e_term": 24024 * a - 205056 * b},
+    5: {
+        "constant_term": 5900520 * a - 62118720 * b,
+        "e_term": -2170680 * a + 22852200 * b,
+    },
+    6: {
+        "constant_term": -780827760 * a + 9778048560 * b,
+        "e_term": 287250480 * a - 3597143040 * b,
+    },
+}
+
+
+class EIntegrate(GetIntegrateFromData):
+    # sympy 算力不够，以下由 MMA 算出
+    data = _data
+
+    def get_integrate_args(self, n):
+        return x**n * (1 - x) ** n * (a + b * x) * exp(x), (x, 0, 1)
+
+
+class ESolution(Solution):
+    def __init__(self, p, q):
+        self.p = p
+        self.q = q
+        if self.q == 0:
+            raise BadInput()
+
+        self.get_integrate = EIntegrate()
+        self.symbols = (a, b)
+
+        self.integrate_result_classes_eq = {
+            "e_term": q,
+            CONSTANT_TERM_KEY: -p,
+        }
+        # check
+        self.check_sgn = lin_func_sgn
+
+    @staticmethod
+    def get_tries_args():
+        return EIntegrate.data.keys()
+
+    def get_latex_ans(self):
+        try_arg, symbol_val, sgn = self.try_times()
+        print(f"{(try_arg, symbol_val, sgn)=}")
+        if try_arg is None:
+            return None
+
+        p = to_latex(self.p)
+        q = to_latex(self.q, is_coeff=True)
+        I = self.get_integrate.get_latex(try_arg, symbol_val)
+        return rf"{q}e-{p} = {I} {sign2cmp[sgn]} 0"
+
+
+register("e", ESolution)
+
+
+if __name__ == "__main__":
+    print(ESolution(25, 9))

solutions/eq.py

@@ -0,0 +1,179 @@
+from sympy import *
+from sympy.abc import *
+from output_util import to_latex, sign2cmp, to_latexes
+from sgntools import lin_func_sgn
+from solution import *
+
+_data = {
+    (1,): {
+        "constant_term": a / q**2 + 2 * a / q**3 - 2 * b / q**3 - 6 * b / q**4,
+        "eq_term": a / q**2 - 2 * a / q**3 + b / q**2 - 4 * b / q**3 + 6 * b / q**4,
+    },
+    (2,): {
+        "constant_term": -2 * a / q**3
+        - 12 * a / q**4
+        - 24 * a / q**5
+        + 6 * b / q**4
+        + 48 * b / q**5
+        + 120 * b / q**6,
+        "eq_term": 2 * a / q**3
+        - 12 * a / q**4
+        + 24 * a / q**5
+        + 2 * b / q**3
+        - 18 * b / q**4
+        + 72 * b / q**5
+        - 120 * b / q**6,
+    },
+    (3,): {
+        "constant_term": 6 * a / q**4
+        + 72 * a / q**5
+        + 360 * a / q**6
+        + 720 * a / q**7
+        - 24 * b / q**5
+        - 360 * b / q**6
+        - 2160 * b / q**7
+        - 5040 * b / q**8,
+        "eq_term": 6 * a / q**4
+        - 72 * a / q**5
+        + 360 * a / q**6
+        - 720 * a / q**7
+        + 6 * b / q**4
+        - 96 * b / q**5
+        + 720 * b / q**6
+        - 2880 * b / q**7
+        + 5040 * b / q**8,
+    },
+    (4,): {
+        "constant_term": -24 * a / q**5
+        - 480 * a / q**6
+        - 4320 * a / q**7
+        - 20160 * a / q**8
+        - 40320 * a / q**9
+        + 120 * b / q**6
+        + 2880 * b / q**7
+        + 30240 * b / q**8
+        + 161280 * b / q**9
+        + 362880 * b / q**10,
+        "eq_term": 24 * a / q**5
+        - 480 * a / q**6
+        + 4320 * a / q**7
+        - 20160 * a / q**8
+        + 40320 * a / q**9
+        + 24 * b / q**5
+        - 600 * b / q**6
+        + 7200 * b / q**7
+        - 50400 * b / q**8
+        + 201600 * b / q**9
+        - 362880 * b / q**10,
+    },
+    (5,): {
+        "constant_term": 120 * a / q**6
+        + 3600 * a / q**7
+        + 50400 * a / q**8
+        + 403200 * a / q**9
+        + 1814400 * a / q**10
+        + 3628800 * a / q**11
+        - 720 * b / q**7
+        - 25200 * b / q**8
+        - 403200 * b / q**9
+        - 3628800 * b / q**10
+        - 18144000 * b / q**11
+        - 39916800 * b / q**12,
+        "eq_term": 120 * a / q**6
+        - 3600 * a / q**7
+        + 50400 * a / q**8
+        - 403200 * a / q**9
+        + 1814400 * a / q**10
+        - 3628800 * a / q**11
+        + 120 * b / q**6
+        - 4320 * b / q**7
+        + 75600 * b / q**8
+        - 806400 * b / q**9
+        + 5443200 * b / q**10
+        - 21772800 * b / q**11
+        + 39916800 * b / q**12,
+    },
+    (6,): {
+        "constant_term": -720 * a / q**7
+        - 30240 * a / q**8
+        - 604800 * a / q**9
+        - 7257600 * a / q**10
+        - 54432000 * a / q**11
+        - 239500800 * a / q**12
+        - 479001600 * a / q**13
+        + 5040 * b / q**8
+        + 241920 * b / q**9
+        + 5443200 * b / q**10
+        + 72576000 * b / q**11
+        + 598752000 * b / q**12
+        + 2874009600 * b / q**13
+        + 6227020800 * b / q**14,
+        "eq_term": 720 * a / q**7
+        - 30240 * a / q**8
+        + 604800 * a / q**9
+        - 7257600 * a / q**10
+        + 54432000 * a / q**11
+        - 239500800 * a / q**12
+        + 479001600 * a / q**13
+        + 720 * b / q**7
+        - 35280 * b / q**8
+        + 846720 * b / q**9
+        - 12700800 * b / q**10
+        + 127008000 * b / q**11
+        - 838252800 * b / q**12
+        + 3353011200 * b / q**13
+        - 6227020800 * b / q**14,
+    },
+}
+
+
+class EQIntegrate(GetIntegrateFromData):
+    data = _data
+
+    def get_integrate_args(self, try_arg):
+        n, q = try_arg
+        return x**n * (1 - x) ** n * (a + b * x) * e ** (q * x), (x, 0, 1)
+
+    def tries(self, try_arg):
+        n, q_value = try_arg
+        return {key: expr.subs(q, q_value) for key, expr in self.data[(n,)].items()}
+
+
+class EQSolution(Solution):
+    def __init__(self, q1, q2, u, v):
+        if q2 == 0 or v == 0:
+            raise BadInput()
+
+        self.q = q1 / q2  # 输入都是 Rational 类型的，可以不损失精度相除
+        self.u = u
+        self.v = v
+        self.get_integrate = EQIntegrate()
+        self.symbols = (a, b)
+        self.integrate_result_classes_eq = {
+            "eq_term": v,
+            CONSTANT_TERM_KEY: -u,
+        }
+        # check
+        self.check_sgn = lin_func_sgn
+
+    def get_tries_args(self):
+        for (n,) in EQIntegrate.data.keys():
+            yield n, self.q
+
+    def get_latex_ans(self):
+        try_arg, symbol_val, sgn = self.try_times()
+        print(f"{(try_arg, symbol_val, sgn)=}")
+        if try_arg is None:
+            return None
+
+        u, q = to_latexes(self.u, self.q)
+        v = to_latex(self.v, is_coeff=True)
+        I = self.get_integrate.get_latex(try_arg, symbol_val)
+        return rf"{v}e^{q}-{u} = {I} {sign2cmp[sgn]} 0"
+
+
+register("e^q", EQSolution)
+
+
+if __name__ == "__main__":
+    print(EQSolution(Rational(2), 1, 7, 1).get_latex_ans())

solutions/pi.py

@@ -0,0 +1,136 @@
+from sympy.abc import a, b, c, x
+from output_util import to_latex, sign2cmp
+from sgntools import sq_func_sgn
+from solution import *
+
+
+class PiIntegrate(GetIntegrateFromData):
+    # sympy 算力不够，以下由 MMA 算出
+    # PiIF[n_] :=
+    #  Collect[ Collect[
+    #    PowerExpand[ Expand[
+    #      Integrate[x^n*(1 - x)^n*(a + b x + c x^2)/(x^2 + 1),
+    #                {x, 0, 1}]
+    #    ]],
+    #    Log[2]], Pi]
+    data = {
+        1: {
+            "pi_term": (a - b - c) / 4,
+            "log2_term": (a + b - c) / 2,
+            CONSTANT_TERM_KEY: -a + b / 2 + 7 * c / 6,
+        },
+        2: {
+            "pi_term": -b / 2,
+            "log2_term": a - c,
+            CONSTANT_TERM_KEY: (-2 * a / 3 + 19 * b / 12 + 7 * c / 10),
+        },
+        3: {
+            "pi_term": (-a - b + c) / 2,
+            "log2_term": a - b - c,
+            CONSTANT_TERM_KEY: 53 * a / 60 + 34 * b / 15 - 92 * c / 105,
+        },
+        4: {
+            "pi_term": -a + c,
+            "log2_term": 2 * b,
+            CONSTANT_TERM_KEY: 22 * a / 7 + 233 * b / 168 - 1979 * c / 630,
+        },
+        5: {
+            "pi_term": -a + b + c,
+            "log2_term": 2 * (-a - b + c),
+            CONSTANT_TERM_KEY: 11411 * a / 2520 - 4423 * b / 2520 - 41837 * c / 9240,
+        },
+        6: {
+            "pi_term": 2 * b,
+            "log2_term": -4 * a + 4 * c,
+            CONSTANT_TERM_KEY: (38429 * a) / 13860
+            - (174169 * b) / 27720
+            - (35683 * c) / 12870,
+        },
+        7: {
+            "pi_term": 2 * (a + b - c),
+            "log2_term": 4 * (-a + b + c),
+            CONSTANT_TERM_KEY: -((421691 * a) / 120120)
+            - (407917 * b) / 45045
+            + (31627 * c) / 9009,
+        },
+        8: {
+            "pi_term": 4 * (a - c),
+            "log2_term": 8 * b,
+            CONSTANT_TERM_KEY: -(188684 * a) / 15015
+            - (1332173 * b) / 240240
+            + (3849155 * c) / 306306,
+        },
+        9: {
+            "pi_term": 4 * (a - b - c),
+            "log2_term": 8 * (-c + a + b),
+            CONSTANT_TERM_KEY: -((17069771 * a) / 942480)
+            + (86025349 * b) / 12252240
+            + (4216233689 * c) / 232792560,
+        },
+        10: {
+            "pi_term": -8 * b,
+            "log2_term": 16 * (a - c),
+            CONSTANT_TERM_KEY: -((1290876029 * a) / 116396280)
+            + (325039733 * b) / 12932920
+            + (117352369 * c) / 10581480,
+        },
+        11: {
+            "pi_term": 8 * (-a - b + c),
+            "log2_term": 16 * (a - b - c),
+            CONSTANT_TERM_KEY: (817240769 * a) / 58198140
+            + (4216233641 * b) / 116396280
+            - (37593075209 * c) / 2677114440,
+        },
+        12: {
+            "pi_term": -16 * a + 16 * c,
+            "log2_term": -32 * b,
+            CONSTANT_TERM_KEY: (431302721 * a) / 8580495
+            + (9135430531 * b) / 411863760
+            - (5902037233 * c) / 117417300,
+        },
+    }
+
+    def get_integrate_args(self, n):
+        return x**n * (1 - x) ** n * (a + b * x + c * x**2) / (1 + x**2), (x, 0, 1)
+
+
+class PiSolution(Solution):
+    def __init__(self, p, q):
+        self.p = p
+        self.q = q
+        if self.q == 0:
+            raise BadInput()
+
+        self.get_integrate = PiIntegrate()
+        self.symbols = (a, b, c)
+        self.integrate_result_classes_eq = {
+            "pi_term": q,
+            "log2_term": 0,
+            CONSTANT_TERM_KEY: -p,
+        }
+        # check
+        self.check_sgn = sq_func_sgn
+
+    @staticmethod
+    def get_tries_args():
+        return PiIntegrate.data.keys()
+
+    def get_latex_ans(self):
+        try_arg, symbol_val, sgn = self.try_times()
+        print(f"{(try_arg, symbol_val, sgn)=}")
+        if try_arg is None:
+            return None
+
+        p = to_latex(self.p)
+        q = to_latex(self.q, is_coeff=True)
+        I = self.get_integrate.get_latex(try_arg, symbol_val)
+        return rf"{q}\pi-{p} = {I} {sign2cmp[sgn]} 0"
+
+
+register("π", PiSolution, top=True)
+
+if __name__ == "__main__":
+    while True:
+        p = int(input(">>> "))
+        q = int(input("  / "))
+        print(PiSolution(p, q).get_latex_ans())

solutions/pin.py

@@ -0,0 +1,188 @@
+from sympy import *
+from sympy.abc import a, b, x
+from output_util import to_latex, sign2cmp, to_latexes
+from sgntools import lin_func_sgn
+from solution import *
+
+_data = {
+    (1, 2): {"constant_term": a - 2 * b / 3, "pin_term": -a / 4 + b / 4},
+    (1, 4): {"constant_term": -2 * a / 3 + 13 * b / 15, "pin_term": a / 4 - b / 4},
+    (1, 6): {"constant_term": 13 * a / 15 - 76 * b / 105, "pin_term": -a / 4 + b / 4},
+    (1, 8): {"constant_term": -76 * a / 105 + 263 * b / 315, "pin_term": a / 4 - b / 4},
+    (1, 10): {
+        "constant_term": 263 * a / 315 - 2578 * b / 3465,
+        "pin_term": -a / 4 + b / 4,
+    },
+    (1, 12): {
+        "constant_term": -2578 * a / 3465 + 36979 * b / 45045,
+        "pin_term": a / 4 - b / 4,
+    },
+    (2, 3): {"constant_term": a / 4 - 3 * b / 16, "pin_term": -a / 48 + b / 48},
+    (2, 5): {"constant_term": -3 * a / 16 + 31 * b / 144, "pin_term": a / 48 - b / 48},
+    (2, 7): {
+        "constant_term": 31 * a / 144 - 115 * b / 576,
+        "pin_term": -a / 48 + b / 48,
+    },
+    (2, 9): {
+        "constant_term": -115 * a / 576 + 3019 * b / 14400,
+        "pin_term": a / 48 - b / 48,
+    },
+    (2, 11): {
+        "constant_term": 3019 * a / 14400 - 973 * b / 4800,
+        "pin_term": -a / 48 + b / 48,
+    },
+    (2, 13): {
+        "constant_term": -973 * a / 4800 + 48877 * b / 235200,
+        "pin_term": a / 48 - b / 48,
+    },
+    (3, 2): {"constant_term": 2 * a - 52 * b / 27, "pin_term": -a / 16 + b / 16},
+    (3, 4): {
+        "constant_term": -52 * a / 27 + 6554 * b / 3375,
+        "pin_term": a / 16 - b / 16,
+    },
+    (3, 6): {
+        "constant_term": 6554 * a / 3375 - 2241272 * b / 1157625,
+        "pin_term": -a / 16 + b / 16,
+    },
+    (3, 8): {
+        "constant_term": -2241272 * a / 1157625 + 60600094 * b / 31255875,
+        "pin_term": a / 16 - b / 16,
+    },
+    (3, 10): {
+        "constant_term": 60600094 * a / 31255875 - 80596213364 * b / 41601569625,
+        "pin_term": -a / 16 + b / 16,
+    },
+    (3, 12): {
+        "constant_term": -80596213364 * a / 41601569625
+        + 177153083899958 * b / 91398648466125,
+        "pin_term": a / 16 - b / 16,
+    },
+    (4, 3): {
+        "constant_term": 3 * a / 8 - 45 * b / 128,
+        "pin_term": -7 * a / 1920 + 7 * b / 1920,
+    },
+    (4, 5): {
+        "constant_term": -45 * a / 128 + 1231 * b / 3456,
+        "pin_term": 7 * a / 1920 - 7 * b / 1920,
+    },
+    (4, 7): {
+        "constant_term": 1231 * a / 3456 - 19615 * b / 55296,
+        "pin_term": -7 * a / 1920 + 7 * b / 1920,
+    },
+    (4, 9): {
+        "constant_term": -19615 * a / 55296 + 12280111 * b / 34560000,
+        "pin_term": 7 * a / 1920 - 7 * b / 1920,
+    },
+    (4, 11): {
+        "constant_term": 12280111 * a / 34560000 - 4090037 * b / 11520000,
+        "pin_term": -7 * a / 1920 + 7 * b / 1920,
+    },
+    (4, 13): {
+        "constant_term": -4090037 * a / 11520000 + 9824498837 * b / 27659520000,
+        "pin_term": 7 * a / 1920 - 7 * b / 1920,
+    },
+    (5, 2): {
+        "constant_term": 24 * a - 1936 * b / 81,
+        "pin_term": -5 * a / 64 + 5 * b / 64,
+    },
+    (5, 4): {
+        "constant_term": -1936 * a / 81 + 6051944 * b / 253125,
+        "pin_term": 5 * a / 64 - 5 * b / 64,
+    },
+    (5, 6): {
+        "constant_term": 6051944 * a / 253125 - 101708947808 * b / 4254271875,
+        "pin_term": -5 * a / 64 + 5 * b / 64,
+    },
+    (5, 8): {
+        "constant_term": -101708947808 * a / 4254271875
+        + 24715694492344 * b / 1033788065625,
+        "pin_term": 5 * a / 64 - 5 * b / 64,
+    },
+    (5, 10): {
+        "constant_term": 24715694492344 * a / 1033788065625
+        - 3980462502772918544 * b / 166492601756971875,
+        "pin_term": -5 * a / 64 + 5 * b / 64,
+    },
+    (5, 12): {
+        "constant_term": -3980462502772918544 * a / 166492601756971875
+        + 1477921859864507412282392 * b / 61817537584151358384375,
+        "pin_term": 5 * a / 64 - 5 * b / 64,
+    },
+    (6, 3): {
+        "constant_term": 15 * a / 8 - 945 * b / 512,
+        "pin_term": -31 * a / 16128 + 31 * b / 16128,
+    },
+    (6, 5): {
+        "constant_term": -945 * a / 512 + 229955 * b / 124416,
+        "pin_term": 31 * a / 16128 - 31 * b / 16128,
+    },
+    (6, 7): {
+        "constant_term": 229955 * a / 124416 - 14713475 * b / 7962624,
+        "pin_term": -31 * a / 16128 + 31 * b / 16128,
+    },
+    (6, 9): {
+        "constant_term": -14713475 * a / 7962624 + 45982595359 * b / 24883200000,
+        "pin_term": 31 * a / 16128 - 31 * b / 16128,
+    },
+    (6, 11): {
+        "constant_term": 45982595359 * a / 24883200000 - 5109066151 * b / 2764800000,
+        "pin_term": -31 * a / 16128 + 31 * b / 16128,
+    },
+    (6, 13): {
+        "constant_term": -5109066151 * a / 2764800000
+        + 601081707598999 * b / 325275955200000,
+        "pin_term": 31 * a / 16128 - 31 * b / 16128,
+    },
+}
+
+
+class PiNIntegrate(GetIntegrateFromData):
+    data = _data
+
+    def get_integrate_args(self, args):
+        n, m = args
+        return x**m * (a + b * x**2) * (log(1 / x)) ** (n - 1) / (1 + x**2), (x, 0, 1)
+
+
+class PiNSolution(Solution):
+    def __init__(self, n, p, q):
+        if n < 0:
+            n = -n
+            p, q = q, p
+        self.n = n
+        self.p = p
+        self.q = q
+        if self.q == 0:
+            raise BadInput()
+
+        self.get_integrate = PiNIntegrate()
+        self.symbols = (a, b)
+        self.integrate_result_classes_eq = {
+            "pin_term": q,
+            CONSTANT_TERM_KEY: -p,
+        }
+        # check
+        self.check_sgn = lin_func_sgn
+
+    def get_tries_args(self):
+        for n, m in PiNIntegrate.data.keys():
+            if n == self.n:
+                yield n, m
+
+    def get_latex_ans(self):
+        try_arg, symbol_val, sgn = self.try_times()
+        print(f"{(try_arg, symbol_val, sgn)=}")
+        if try_arg is None:
+            return None
+
+        p, n = to_latexes(self.p, self.n)
+        q = to_latex(self.q, is_coeff=True)
+        I = self.get_integrate.get_latex(try_arg, symbol_val)
+        return rf"{q}\pi^{n}-{p} = {I} {sign2cmp[sgn]} 0"
+
+
+register("π^n", PiNSolution)
+
+
+if __name__ == "__main__":
+    print(PiNSolution(3, 31, 1).get_latex_ans())