Lean4’da Polynomial Tengsizliklarni Sum‑of‑Squares Yordamida Hal Qilish: Sostactic Paketi

Lean4 dasturlash tilida formal isbotlar yaratish sohasida yangi bir bosqich ochildi – Sostactic paketi. Ushbu paket polynomial tengsizliklarni sum‑of‑squares (SOS) dekompozitsiyalari orqali isbotlashga mo‘ljallangan bo‘lib, Python orqa‑fondidan foydalanadi. Natijada foydalanuvchilar Lean ichida yoki to‘g‘ridan‑to‘g‘ri Python orqali bu kuchli taktikalardan foydalanishlari mumkin.

Sostactic nima va qanday ishlaydi?

Sostactic paketining asosiy maqsadi Lean4’da mavjud bo‘lgan nlinarith va positivity taktikalari bilan solishtirganda ancha kengroq imkoniyatlar taqdim etishdir. U quyidagi turdagi masalalarni hal qila oladi:

import Sostactic

-- AM-GM inequality
example (x y : ℝ) : 2 * x * y ≤ x^2 + y^2 := by
  sos_decomp

-- Motzkin polynomial: ratio of SOS
example (x y z : ℝ) :
    0 ≤ x^4 * y^2 + x^2 * y^4 + z^6 - 3 * x^2 * y^2 * z^2 := by
  sos_decomp (degree := 2)

-- 4x³ - 3x + 1 ≥ 0 on [0, 1] (touches 0 at x = 1/2)
-- linarith, positivity, and nlinarith all fail
example (x : ℝ) (h1 : 0 ≤ x) (h2 : 0 ≤ 1 - x) :
    0 ≤ 4 * x^3 - 3 * x + 1 := by
  putinar_decomp (order := 2)

-- two disjoint disks centered at (0,0) and (3,3)
-- linarith and nlinarith fail
example : ¬∃ x y : ℝ, 0 ≤ 1 - x^2 - y^2 ∧ 0 ≤ 1 - (x - 3)^2 - (y - 3)^2 := by
  rintro ⟨x, y, h1, h2⟩
  schmudgen_empty (order := 1)

• Polinomialning butun dunyo bo‘ylab manfiy bo‘lmasligini isbotlash;
• Polinomialning ma'lum bir semialgebraik to‘plam (polinomial tengsizliklar to‘plami) ichida ham manfiy bo‘lmasligini tasdiqlash;
• Semialgebraik to‘plamning bo‘shligini, ya'ni polinomial tengsizliklar tizimining imkonsizligini ko‘rsatish.

Ushbu yondashuvning nazariy asosi sodda: agar bir polinomial boshqa polinomiallarning kvadratlari yig‘indisi sifatida ifodalanadigan bo‘lsa, unda u har qanday nuqtada manfiy bo‘lmaydi. 20‑asrda real algebraik geometriyada bu natija muhim ilmiy yutuq bo‘lib, 21‑asrda semidefinite dasturlash (SDP) bilan birlashtirilganda amaliy hisoblash vositasi sifatida keng qo‘llanila boshlandi.

[[require]]
name = "sostactic"
git = "https://github.com/mmaaz-git/sostactic.git"
rev = "main"

Python orqa‑fondi va Lean integratsiyasi

Sostactic paketida Python orqa‑fondi SOS dekompozitsiyalarini hisoblash uchun semidefinite dasturlash kutubxonalaridan foydalanadi. Natija esa Lean4 taktikasi sifatida qaytariladi, bu esa foydalanuvchiga isbotni to‘liq formal tarzda tasdiqlash imkonini beradi. Bu ikki platformaning birlashuvi quyidagi afzalliklarni beradi:

require sostactic from git
  "https://github.com/mmaaz-git/sostactic.git" @ "main"

• Tezkor hisoblash: Pythonning samarali numerik kutubxonalari yordamida katta hajmdagi SDP masalalari yechiladi;
• Formal isbot: Natija Lean4 ichida tasdiqlanadi, bu esa isbotning to‘g‘riligini matematik jihatdan kafolatlaydi;
• Qulaylik: Foydalanuvchi SOS isbotini Python skriptlari yoki bevosita Lean kodida chaqirishi mumkin.

Amaliy misollar

Quyidagi misolda polinomial p(x) = x^4 - 3x^2 + 2 ning har qanday real x uchun manfiy bo‘lmasligini isbotlash ko‘rsatiladi:

lake update sostactic
lake build

import sostactic
open Sostactic

example : ∀ x : ℝ, 0 ≤ x^4 - 3*x^2 + 2 := by
  sos_prove [x^4 - 3*x^2 + 2]

Bu kod Lean4 ichida sos_prove taktikasi yordamida SOS dekompozitsiyasini avtomatik tarzda topadi va isbotni yakunlaydi.

python3 -m venv .venv
.venv/bin/python3 -m ensurepip
.venv/bin/python3 -m pip install -r .lake/packages/Sostactic/python/requirements.txt

Nega bu muhim?

Formal tasdiqlash tizimlari dasturiy ta'minot, kriptografiya, robototexnika va ilmiy hisoblashlarda xatoliklarni kamaytirish uchun zarur. Polynomial tengsizliklar ko‘plab nazariy va amaliy muammolarda, masalan, barqarorlik tahlili yoki optimallashtirishda uchraydi. Sostactic kabi vositalar bu muammolarni avtomatlashtirishga yordam beradi, shu bilan birga isbotlarning ishonchliligini oshiradi.

export SOSTACTIC_PYTHON=/path/to/your/python3

Kelajakda nimalar kutish mumkin?

Sostactic hozirgi kunda hamjamiyat tomonidan faol rivojlantirilmoqda. Kelgusida quyidagilarni kutish mumkin:

from sympy import symbols, Poly
from python.sos import sos_decomp

x, y = symbols('x y')
result = sos_decomp(Poly(x**2 + y**2, x, y))
print(result["success"])  # True
print(result["exact_sos"])  # weighted SOS terms: [(weight, poly), ...]

• Ko‘proq semialgebraik to‘plamlar uchun qo‘llab‑quvvatlash;
• Yuqori darajadagi SDP solverlar bilan integratsiya;
• Lean4 ekotizimida boshqa taktikalar (masalan, nlinarith) bilan birgalikda ishlash imkoniyati.

Umuman olganda, Sostactic paketining chiqishi Lean4 foydalanuvchilari uchun polynomial tengsizliklarni isbotlashda yangi imkoniyatlar yaratadi va formal tasdiqlash sohasida yanada keng tarqalgan amaliyotga yo‘l ochadi.

x, y, z = symbols('x y z')
motzkin = Poly(x**4*y**2 + x**2*y**4 + z**6 - 3*x**2*y**2*z**2, x, y, z)
result = sos_decomp(motzkin, denom_degree_bound=2)
print(result["exact_num_sos"])  # numerator SOS decomposition
print(result["exact_den_sos"])  # denominator SOS decomposition