這是一套用於透過和平方（SOS）分解證明多項式不等式的 Lean4 策略集合，並由 Python 後端驅動。你可以透過 Python 或 Lean 使用這些策略。

這些策略比 nlinarith 和 positivity 更強大，也就是說，它們能證明那些傳統方法無法證明的不等式。理論上，它們可以用來證明以下類型的陳述。

更多運作細節可參考部落格文章。完整文件位於本 README 結尾，歡迎將你的程式代理指向該文件。

請參考 Sostactic/Examples.lean 以獲得更多有趣範例！

如果你的專案使用 lakefile.toml 或 lakefile.lean，請依說明設定。

注意：Sostactic 追蹤 Mathlib v4.29.0-rc8 版本。如果你的專案使用不同版本，可能需要對齊。新建專案時，預設 Mathlib 版本應相符。

在專案根目錄建立虛擬環境並安裝相依套件即可使用。Sostactic 會自動尋找專案根目錄下的 .venv/bin/python3。

建議將 .venv/ 加入 .gitignore。

若 Python 執行檔位置不同，可設定環境變數 SOSTACTIC_PYTHON。

此套件有三種使用方式：Python API、Python CLI 及 Lean 套件。Lean 策略會呼叫 Python CLI 產生證書，然後在 Lean 中檢查該證書。Python 程式使用 cvxpy 凸優化求解器，因為 SOS 多項式與半正定規劃（SDP）有良好對應關係。問題在於 SDP 解是數值解，我們透過有理化與投影步驟及其他數值技巧，取得精確解，並在 Lean 中驗證。

但由於數值問題，精確化可能失敗，原因多樣。互動式定理證明器精神下，求解器會提供如何修正解的建議，透過額外參數傳入。

理論與演算法詳情請參考部落格文章。

以下介紹 Python API、Python CLI 及 Lean 策略。

整個 Python 程式包含於 python/sos.py，測試在 python/test_sos.py。主要有五個函數：

1. 證明多項式 p 全域非負，透過尋找精確 SOS 證書。

denom_degree_bound=0（預設）時，尋找純 SOS 分解：p = w₁s₁² + w₂s₂² + ...

denom_degree_bound > 0 時，尋找 SOS 多項式 d 和 n，使 d·p = n，處理像 Motzkin 多項式這類非負但非 SOS 的多項式。

也可傳入 denom_template 作為含自由參數的 sympy 表達式（例如 a*x**2 + b*y**2 + c*z**2）。

失敗時，result["diagnostics"] 含秩資訊，result["suggestion"] 提示下一步嘗試。

2. 使用 Putinar 的 Positivstellensatz 證明目標函數在半代數集合 {x : g₁(x) ≥ 0, ..., gₘ(x) ≥ 0} 上非負。

順序為全域鬆弛階數 r。每個乘子 h 對應區塊被截斷為 deg(h * sigma) ≤ 2r，sigma 使用的單項式度數最多為 floor((2r - deg(h)) / 2)。

3. 與 putinar 類似，但使用 Schmüdgen 的 Positivstellensatz，乘子為所有約束子集的乘積。此方法比 Putinar 更強大（適用於任意緊集），但 SDP 規模隨約束數指數成長。

4. 證明集合 {x : g₁(x) ≥ 0, ..., gₘ(x) ≥ 0} 為空集，相當於 putinar(-1, constraints, order=order)。

5. 與 putinar_empty 類似，使用 Schmüdgen 的 Positivstellensatz。

所有函數回傳至少包含：

成功時，結果含精確證書資料（SOS 項、Gram 矩陣、證書區塊）。失敗時，"diagnostics" 或 "block_diagnostics" 含每區塊精確化診斷，有助調整 basis_overrides。後端亦回傳啟發式 basis_override_suggestion 與頂層 "suggestion" 字串，可直接貼入 CLI 或 Lean 策略。建議來自失敗的數值解，無額外隱藏 SDP 求解。

CLI 提供相同三個指令（sos_decomp、putinar、schmudgen），輸出 JSON 證書。

成功 sos_decomp 範例輸出表示 x² + y² = 1·y² + 1·x²。Positivstellensatz 證書包含 exact_certificate_blocks，列出每個約束區塊的乘子/SOS 配對。

失敗時輸出含診斷與建議。

證明多項式 f 全域非負，透過 SOS 分解，選擇性使用分母將其分解為 SOS 多項式比率。根據 Artin 定理，任一全域非負多項式皆可如此分解。

目標可為 0 ≤ f、f ≥ 0、a ≤ b 或 a ≥ b。

根據多項式不等式假設，使用 Putinar 或 Schmüdgen Positivstellensatz 證明 0 ≤ f。假設可為 0 ≤ g、g ≥ 0、a ≤ b 或 a ≥ b。

證明矛盾假設導致 False，顯示可行集合為空。

SDP 求解器對大型問題可能較慢。可預先產生證書並從 JSON 檔案載入，避免每次檔案重載時重新求解。

Lean 仍獨立驗證證書，JSON 檔案不被信任。

若子目標無法自動完成，策略會保留為命名目標，供使用者互動完成。sos_decomp 與 Positivstellensatz 分解策略的子目標包括：

對帶分母的 sos_decomp，子目標為 hD_ne、hmul、hD_nonneg、hN_nonneg。

SDP 求解器對大型多項式可能較慢。可用 Python CLI 先生成證書（例如夜間運行），存成 JSON，再在 Lean 載入，避免重複求解。

後端失敗原因可能為鬆弛階數過低（SDP 不可行）或數值 SDP 解無法精確化。兩種情況皆回傳診斷與建議。

建議包括：

- 提高鬆弛階數，若求解器回傳不可行，可能截斷過小。

- 使用分母，對非 SOS 但非負多項式（如 Motzkin）必須。

- 使用 basis overrides，當 SDP 可行但精確化失敗，建議縮小特定 SOS 區塊的基底度數。

- 使用分母模板，透過自由參數引導求解器。

- 嘗試 Schmüdgen 替代 Putinar，前者更強大但計算量大。

- 預先生成證書，避免互動式求解過慢。

對大型多項式，Lean 證明重建可能達到預設 heartbeat 限制，可局部提高。

若子目標未自動完成，會保留為命名目標（如 sos_identity 或 sos_nonneg），供手動完成。

使用技術包括：Lean 的 Mathlib（多變量多項式、positivity 策略）、Python 的 sympy、numpy、cvxpy、clarabel。

本策略集為多項式不等式證明提供強大工具，結合數值優化與形式驗證，提升證明能力與效率。