目前初等數學的研究, 主要還是依賴於人工手算。 由於人受到記憶力、 計算能力等多方面的限制, 以致每次研究的問題不能太複雜, 包括問題的數量要少、 涉及變數個數不能太多、 變數次數不能太高等。 而這些問題借助資訊技術, 是有可能改變的。

我們已經進入了大資料時代, 數學建模和數據分析是中學數學需要培養的核心素養。 能否針對要研究的初等數學問題建立數學模型, 並借助電腦進行資料計算和分析, 批次處理一類問題？ 技術的飛速發展, 使得農業、 工業等都進入了機械化, 初等數學的研究能否機械化？ 我們近幾年做了大量的實踐, 發現這完全是可能的。 本文將以三元算幾不等式的隔離為例, 分享我們的探索思路和研究成果。

一、建立模型

三元算幾不等式是初等數學研究的一個重要內容。 除了其代數特徵之外, 由於三角形有三條邊, 三元算幾不等式也常與三角形不等式混在一起出題, 在各種競賽中頻繁出現。 三元算幾不等式基本形式是 $\dfrac{a+b+c}{3}\ge {\root 3 \of {abc}}$ (只考慮正數範圍, 下同), 由於根式書寫和計算都不太方便, 因此考慮等價形式 $a^3+b^3+c^3\ge 3abc$。 兩個不等的量若存在大小關係, 則可在中間插入新的量 $T$, 使得 $a^3+b^3+c^3\ge T\ge 3abc$, 此稱之為不等式的隔離或加強。

由於隔離可無止盡地做下去, 有必要對 $T$ 從形式上和研究範圍做進一步的限制, 以便操作。 這也是建立模型的過程。設 $T=f(a,b,c)+f(b,c,a)+f(c,a,b)$, 其中

\begin{align*} f(a,b,c)=\,&\frac{k_1a^{k_2}b^{k_3}c^{k_4}\big((1-k_6)a^{k_5}+k_6b^{k_5}+k_6c^{k_5}\big)} {(1-k_7)a^{k_2+k_3+k_4+k_5-3}+k_7b^{k_2+k_3+k_4+k_5-3}+k_7c^{k_2+k_3+k_4+k_5-3}},\\ &\ k_1\in S_1,\ k_2\in S_2,\ k_3\in S_2,\ k_4\in S_2,\ k_5\in S_2,\ k_6\in S_3,\ k_7\in S_3,\\ &\ S_1=\{1,2,3,4\},\ S_2=\{-2,-1,0,1,2,3,4,5\},\ S_3=\Big\{0,\frac 12, 1\Big\}. \end{align*}

$f(a,b,c)$ 的分母中出現指數 $k_2+k_3+k_4+k_5-3$, 是為了確保 $T$ 是三次式。 確定 $T$ 的形式後, 因為變數實在太多, 不太可能直接解不等式 $a^3+b^3+c^3\ge T\ge 3abc$。 我們不解不等式, 而是搜索驗證給定範圍內符合要求的 $T$。 根據乘法原理, $T$ 的可能取值有 $4\times 8\times 8\times 8\times 8\times 3\times 3=147456$ 種。 這遠遠超過人工所能處理的範圍。 下面將借助符號計算軟體 Mathematica 來進行處理。

二、數據分析

對於可能的 147456 個 $T$, 每一個 $T$ 都對應著不等式 $a^3+b^3+c^3\ge T\ge 3abc$。 這其中絕大多數 $T$ 不符合要求。 要排除這些不符合要求的 $T$, 最直接的方式就是舉反例。

篩選數據： 電腦隨機生成一組正數, 賦值給 $a,b,c$, 並對 147456 個不等式 $a^3+b^3+c^3\ge T\ge 3abc$ 進行驗證, 可以排除相當部分 $T$。 對這一操作重複執行 1000 次, 能通過數值驗算的 $T$ 只有幾百個。

數據去重： 幾百個 $T$ 中有重複, 如

$$\frac{2a^2b^2}{a+b}+\frac{2b^2c^2}{b+c}+\frac{2c^2a^2}{c+a}\quad \hbox{與}\quad \frac{2ab}{\dfrac 1a+\dfrac 1b}+\frac{2bc}{\dfrac 1b+\dfrac 1c}+\frac{2ca}{\dfrac 1c+\dfrac 1a} $$

形式不同, 實則恒等。 需要對幾百個 $T$ 進行兩兩對比, 若恒等, 只保留其中形式較簡單的。 最後保留得到 89 個 $T$。 限於篇幅, 此處僅列出如下 17 個。

$(t_1)$ $2abc\Big(\dfrac{c}{a+b}+\dfrac{a}{b+c}+\dfrac{b}{c+a}\Big)$,

$(t_2)$ $\dfrac{2a^2b^2}{a+b}+\dfrac{2b^2c^2}{b+c}+\dfrac{2c^2a^2}{c+a}$,

$(t_3)$ $\dfrac12 a^2(b+c)+\dfrac12 b^2(c+a)+\dfrac12 c^2(a+b)$,

$(t_4)$ $2abc\Big(\dfrac{c^2}{a^2+b^2}+\dfrac{a^2}{b^2+c^2}+\dfrac{b^2}{c^2+a^2}\Big)$,

$(t_5)$ $\dfrac{c^2(a^2+b^2)}{a+b}+\dfrac{a^2(b^2+c^2)}{b+c}+\dfrac{b^2(c^2+a^2)}{c+a}$,

$(t_6)$ $\dfrac{ab(a^2+b^2)}{a+b}+\dfrac{bc(b^2+c^2)}{b+c}+\dfrac{ca(c^2+a^2)}{c+a}$,

$(t_7)$ $a(b^2-bc+c^2)+b(c^2-ca+a^2)+c(a^2-ab+b^2)$,

$(t_8)$ $\dfrac{c^2(a^3+b^3)}{a^2+b^2}+\dfrac{a^2(b^3+c^3)}{b^2+c^2}+\dfrac{b^2(c^3+a^3)}{c^2+a^2}$,

$(t_9)$ $\dfrac{ab(a^3+b^3)}{a^2+b^2}+\dfrac{bc(b^3+c^3)}{b^2+c^2}+\dfrac{ca(c^3+a^3)}{c^2+a^2}$,

$(t_{10})$ $\dfrac{3(a^2b^2+b^2c^2+c^2a^2)}{a+b+c}$,

$(t_{11})$ $\dfrac{(a^2+b^2+c^2)^2}{a+b+c}$,

$(t_{12})$ $\dfrac{(ab+bc+ca)(a^3+b^3+c^3)}{a^2+b^2+c^2}$,

$(t_{13})$ $\dfrac{3(a^3b+b^3c+c^3a)}{a+b+c}$,

$(t_{14})$ $\dfrac{(ab+bc+ca)(a^2+b^2+c^2)}{a+b+c}$,

$(t_{15})$ $\dfrac13 (a+b+c)(ab+bc+ca)$,

$(t_{16})$ $a^2b+b^2c+c^2a$,

$(t_{17})$ $\dfrac{ab(a^4+b^4)}{(a+b)(a^2-ab+b^2)}+\dfrac{bc(b^4+c^4)}{(b+c)(b^2-bc+c^2)}+\dfrac{ca(c^4+a^4)}{(c+a)(c^2-ca+a^2)}$.

三、證明檢驗

數值檢驗法的好處是運算速度快, 經過上千次的檢驗, 錯誤的可能性極低。 因此所得的 89 個 $T$, 大概率保證是符合要求的。為進一步檢驗這些不等式的正確性, 我們使用了數學家楊路教授開發的 Bottema 軟體, 其中的降維演算法能高效證明不等式, 其原理詳見《不等式機器證明與自動發現》。 譬如輸入求證命令：

$$xprove\Big[a^3+b^3+c^3\ge 2abc\Big(\frac{c^2}{a^2+b^2}+\frac{a^2}{b^2+c^2}+\frac{b^2}{c^2+a^2}\Big)\Big];$$

Bottema 軟體輸出： The inequality holds, 意味著該不等式成立。

Bottema 軟體能在理論上保證不等式成立, 但其過程涉及相當複雜的多項式運算, 難以被初等數學研究者接受, 有必要研究其他證明方法。 配方法是一種相當經典巧妙的方法。配方法的思路很多, 最簡單的是使用待定係數法。 此處我們使用在 Groebner Basis 演算法基礎上改進得到的配方法, 參看《Ideals,Varieties and Algorithms》, 於是電腦生成恒等式：

\begin{align*} &a^3+b^3+c^3-\Big(\frac{c^2(a^2+b^2)}{a+b}+\frac{a^2(b^2+c^2)}{b+c}+\frac{b^2(c^2+a^2)}{c+a}\Big)\\ &\quad =\frac{(a+b+c)\big(ab(a+b)(a-b)^2+bc(b+c)(b-c)^2+ca(c+a)(c-a)^2\big)}{(a+b)(b+c)(c+a)};\\ &\frac{c^2(a^2+b^2)}{a+b}+\frac{a^2(b^2+c^2)}{b+c}+\frac{b^2(c^2+a^2)}{c+a}-3abc\\ &\quad =\frac{(a+b+c)\big(a^2(b+c)(b-c)^2+b^2(c+a)(c-a)^2+c^2(a+b)(a-b)^2\big)}{(a+b)(b+c)(c+a)}; \end{align*}

因此 $a^3+b^3+c^3\ge \dfrac{c^2(a^2+b^2)}{a+b}+ \dfrac{a^2(b^2+c^2)}{b+c}+ \dfrac{b^2(c^2+a^2)}{c+a}\ge 3abc$ 得證。

\begin{align*} &a^3+b^3+c^3-2abc\Big(\frac{c}{a+b}+\frac a{b+c}+\frac b{c+a}\Big)\\ &\quad =\frac{c(a-b)^2(a^2+b^2+ab+bc+ca)}{(a+c)(b+c)}+\frac{a(b-c)^2(b^2+c^2+ab+bc+ca)}{(b+a)(c+a)}\\ &\qquad +\frac{b(c-a)^2(c^2+a^2+ab+bc+ca)}{(c+b)(a+b)};\\ &2abc\Big(\frac{c}{a+b}+\frac a{b+c}+\frac b{c+a}\Big)-3abc\\ &\quad =\frac{abc(a-b)^2}{(a+c)(b+c)}+\frac{abc(b-c)^2}{(b+a)(c+a)}+\frac{abc(c-a)^2}{(c+b)(a+b)}; \end{align*}

因此 $a^3+b^3+c^3\ge 2abc\Big(\dfrac{c}{a+b}+ \dfrac{b}{a+c}+\dfrac{a}{b+c}\Big)\ge 3abc$ 得證。 順便得到經典不等式 $\dfrac{c}{a+b}+ \dfrac{b}{a+c}+\dfrac{a}{b+c}\ge \dfrac 32$。

限於我們的水準, 還難以對所發現的這些不等式全部給出漂亮的恒等式證明。這有待進一步努力。 也歡迎讀者給出人工證明。

另外, 關於 89 個 $T$ 之間也得到一些恒等式。 如：

\begin{align*} &\frac{(a^2+b^2+c^2)^2}{a+b+c}-\frac 13 (a+b+c)(ab+ac+bc)\\ &\quad =\frac{\big((a-b)^2+(b-c)^2+(c-a)^2\big)(3a^2+3b^2+3c^2+2ab+2bc+2ca)}{6(a+b+c)};\\ &a(b^2-bc+c^2)+b(c^2-ca+a^2)+c(a^2-ab+b^2)-\Big(\frac{2a^2b^2}{a+b}+\frac{2b^2c^2}{b+c}+\frac{2c^2a^2}{c+a}\Big)\\ &\quad =\frac{(ab+bc+ca)\big((c^2+ab)(a-b)^2+(a^2+bc)(b-c)^2+(b^2+ca)(c-a)^2\big)}{(a+b)(b+c)(c+a)};\\ &a(b^2-bc+c^2)+b(c^2-ca+a^2)+c(a^2-ab+b^2)\\ &\qquad -\Big(\frac{a^2(b^2+c^2)}{b+c}+\frac{b^2(a^2+c^2)}{c+a}+\frac{c^2(a^2+b^2)}{a+b}\Big)\\ &\quad =\frac{abc\Big(a\big((a-b)^2+(a-c)^2\big)+b\big((b-c)^2+(b-a)^2\big)+c\big((c-a)^2+(c-b)^2\big)\Big)}{(a+b)(b+c)(c+a)}; \end{align*}

上述恒等式分別說明： $t_{15}\le t_{11}$, $t_2\le t_7$, $t_5\le t_7$。

這提醒我們, 還有一個工作需要完成, 即89個 $T$ 之間的相互比較, 譬如 $t_2$和$t_5$ 孰大孰小？

四、直觀顯示

對 89 個 $T$ 兩兩比較, 有 $C^{89}_2=3916$ 種可能, 但並不表示能生成 3916 個不等式。 因為存在兩個運算式無法比較的情況。譬如

當 $a=1$, $b=1$, $c=3$ 時,

$$2abc\Big(\frac{c}{a+b}+\frac a{b+c}+\frac b{c+a}\Big)=12\gt10=\frac{2a^2b^2}{a+b}+\frac{2b^2c^2}{b+c}+\frac{2c^2a^2}{c+a}；$$

當 $a=1$, $b=1$, $c=\dfrac 12$ 時,

$$2abc\Big(\frac{c}{a+b}+\frac a{b+c}+\frac b{c+a}\Big)=\dfrac{19}{12}\lt\frac 53=\frac{2a^2b^2}{a+b}+\frac{2b^2c^2}{b+c}+\frac{2c^2a^2}{c+a}；$$

所以 $2abc\Big(\dfrac{c}{a+b}+\dfrac a{b+c}+\dfrac b{c+a}\Big)\cdots\cdots(t_1)$ 和 $\dfrac{2a^2b^2}{a+b}+\dfrac{2b^2c^2}{b+c}+\dfrac{2c^2a^2}{c+a}\cdots\cdots(t_2)$ 之間不可比較。

我們仍然採用數值檢驗方法。 從 $T$ 中任選兩項 $t_i$ 和 $t_j$, 計算得到 $t_i-t_j$ 的正負號, 隨機對 $a,b,c$ 賦值, 重複執行 1000 次。 若 1000 次結果都為非負, 輸出 $t_i\ge t_j$； 若 1000 次結果都為非正, 輸出 $t_i\le t_j$； 其餘情況, 則不輸出。

如果將所得的不等式全部列出, 篇幅龐大, 且不能直觀顯示不等式之間的大小關係。 限於篇幅, 只考慮上文所列的 17 個 $T$。 為了更直觀地顯示, 此處借助圖論中有向圖的概念, 將一個 $T$ 看成一個點, 若 $t_i\le t_j$, 則 $t_i\to t_j$, 即生成一條有向邊, 不等式中較小的項指向較大的項, 於是可得到一個不等式的關係圖 (圖1)。 為使得圖形簡潔, 需刪除一些邊。如 $t_1\to t_{13}$, $t_{13}\to t_{11}$, 那麼刪除 $t_1\to t_{11}$ 這條邊並不會丟失資訊。 通過圖 1, 容易得到不等式鏈條, 如 $3abc\le t_{15}\le t_3\le t_{14}\le t_6\le t_{12}\le t_{11}\le a^3+b^3+c^3$。

至此, 我們通過建立模型、 分析資料、 證明檢驗、 直觀顯示四個步驟, 探索了三元算幾不等式的隔離, 研究所得的幾百個不等式結論可以為教學、 考試、 研究等提供素材。 從我們的實踐來看, 上述步驟可認為是借助電腦自動生成初等數學結論的一般方法。 同時本文也可以看作是中學數學建模的一個案例。 因為中學生知識水準、 投入精力等多方面的限制, 讓他們研究一些現實問題可能比較困難, 去研究初等數學內部的一些問題可能更具有可操作性。 考慮到中學生的實際水準, 建議只完成基於數值檢驗法尋找 $T$, 而這可以使用 Excel 完成。

本文研究看似涉及上萬條訊息, 動輒測試上千次, 實際上這樣的運算量對於電腦來說不值一提。 如果我們考慮成熟, 在建立合適的模型以及編寫好程式之後, 電腦輸出 89 個 $T$ 以及圖 1, 總共無需 2 分鐘。 而這一探索靠人工來完成, 所花費的時間精力難以想像。 農業生產已經告別了刀耕火種的時代, 但現在多數的初等數學研究者還是依賴紙筆在做研究, 沒有充分利用資訊技術帶來的便利。 最後抄錄吳文俊先生的話結束本文。 吳先生認為, 工業時代主要是體力勞動的機械化, 現在是電腦時代, 腦力勞動機械化可以提到議事日程上來, 數學研究機械化是腦力勞動機械化的起點, 因為數學表達非常精確嚴密, 敘述簡明, 我們要打開這個局面。

參考文獻

本文作者彭翕成任職中國華中師範大學國家數位化學習工程技術研究中心, 曹洪洋任職中國常州九章教育科技有限公司