Sostactic: Gói mở rộng Lean 4 chứng minh bất đẳng thức đa thức mạnh mẽ hơn nhờ Sum-of-Squares

Sostactic là một bộ sưu tập các chiến thuật (tactics) dành cho Lean 4, được thiết kế để chứng minh các bất đẳng thức đa thức thông qua phương pháp phân tích tổng bình phương (Sum-of-Squares - SOS). Gói mở rộng này hoạt động với sự hỗ trợ của một backend Python, giúp giải quyết những hạn chế hiện có của Lean trong việc xử lý các bất đẳng thức phi tuyến.

Tại sao cần Sostactic?

Hiện tại, sự hỗ trợ cho các bất đẳng thức phi tuyến trong Lean còn khá hạn chế. Sostactic ra đời để giải quyết vấn đề này bằng cách cung cấp các công cụ mạnh mẽ hơn nhiều so với các chiến thuật tích hợp sẵn như nlinarith hay positivity. Về mặt lý thuyết, Sostactic có thể chứng minh các loại phát biểu sau:

• Chứng minh một đa thức không âm trên toàn bộ miền số.
• Chứng minh một đa thức không âm trên một tập bán đại số (được định nghĩa bởi một hệ bất đẳng thức đa thức).
• Chứng minh một tập bán đại số là rỗng, tức là hệ bất đẳng thức đa thức tương ứng là không khả thi.

Nguyên lý hoạt động

Cốt lõi của Sostactic dựa trên một quan sát toán học quan trọng: nếu một đa thức có thể được viết dưới dạng tổng bình phương của các đa thức khác, thì nó luôn không âm ở mọi nơi. Các định lý chứng minh sự tồn tại của các phép phân tích này là một trong những thành tựu lớn của hình học đại số thực thế kỷ 20.

Sostactic kết nối lý thuyết này với lập trình bán xác định (Semidefinite Programming - SDP) trong thế kỷ 21 để biến nó thành một công cụ tính toán thực tế. Gói phần mềm sử dụng Python (cụ thể là thư viện cvxpy cho tối ưu hóa lồi) để giải bài toán SDP, sau đó Lean sẽ kiểm tra lại chứng chỉ (certificate) để đảm bảo tính chính xác tuyệt đối.

Ví dụ minh họa

Sostactic có thể xử lý các bài toán phức tạp mà các công cụ cũ không thể làm được. Ví dụ, chứng minh bất đẳng thức AM-GM trở nên cực kỳ đơn giản:

import Sostactic
example (x y : ℝ) : 2 * x * y ≤ x^2 + y^2 := by
  sos_decomp

Hoặc chứng minh tính không âm của đa thức Motzkin phức tạp hơn, vốn không thể biểu diễn trực tiếp dưới dạng tổng bình phương:

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)

Cách sử dụng và Cài đặt

Người dùng có thể cài đặt Sostactic thông qua trình quản lý gói của Lean (Lake) bằng cách thêm dependency vào lakefile.lean. Sau đó, cần thiết lập môi trường Python 3.10+ và cài đặt các thư viện cần thiết như cvxpy, sympy và numpy.

Gói phần mềm cung cấp ba cách sử dụng chính:

1. Python API: Để tích hợp vào các ứng dụng Python.
2. Python CLI: Để chạy từ dòng lệnh và tạo chứng chỉ JSON.
3. Lean Tactics: Các chiến thuật như sos_decomp, putinar_decomp và schmudgen_decomp để sử dụng trực tiếp trong mã nguồn Lean.

Đối với các bài toán lớn, người dùng có thể sử dụng Python CLI để tạo trước chứng chỉ (certificate) và lưu vào file JSON, giúp Lean không cần chạy lại bộ giải tối ưu hóa mỗi khi tải file, từ đó tăng tốc độ quá trình chứng minh.

Sostactic là một bước tiến quan trọng đối với cộng đồng sử dụng Lean, đặc biệt là trong các lĩnh vực yêu cầu chứng minh toán học chính xác cao và tự động hóa các bài toán tối ưu hóa phức tạp.