λ
DPSY / SOSv7.1.6
✣ 01 / TỔNG QUAN · DPSY / SOS v7.1.6

TOOL Giải / Chứng minh
Bất Đẳng Thức
DPSY & Exact SOS

TOOL được phát triển nhằm hỗ trợ quá trình khám phá và chứng minh các bất đẳng thức ba biến. Hai thành phần trọng tâm của hệ thống là DPSY và SOS, được xây dựng để phục vụ việc tìm kiếm cấu trúc chứng minh và xác minh các biểu diễn đại số. TOOL sẽ tiếp tục được nghiên cứu, hoàn thiện và mở rộng trong các phiên bản tiếp theo.

Foundational Invariant:
∑cycf(a,b,c)≥Φ  ⟺  F≤f∧∑cycF=Φ\displaystyle \sum_{\text{cyc}} f(a,b,c) \ge \Phi \iff F \le f \quad \wedge \quad \sum_{\text{cyc}} F = \Phi
Thử nghiệm Giải bài mẫuNăng lực Hệ thống
DPSY / SOS · Technical Profile

Một số chỉ số đại diện cho khả năng xử lý và xác minh của phiên bản hiện tại.

Độ trễ khớp F
0.028s
Tiếp xúc vi sai bậc hai
Trung bình trên bộ kiểm thử
Xác minh hữu tỉ
100%
Exact certificate verification
Trên bộ kiểm thử hiện tại
Thông lượng đơn thức
12,800+
Monomial orbits / s
Symbolic orbit processing
Bậc đa thức tối đa
Bậc 12
Số mũ tối đa 16 · Bậc đa thức 12
Đa thức · Phân thức · Căn thức
CREATOR PROFILE
Đang hoạt động
NA

Nguyễn Thái An

AUTHOR

Tác giả của Tool DPSY & Exact SOS

Việt Nam 🇻🇳·University of Science - VNUHCM

Chào bạn, mình là Nguyễn Thái An. Năm 2023 khi mình làm bất đẳng thức thì mình đã thấy một số người sử dụng Tool DPSY và SOS trong chứng minh bất đẳng thức. Từ đó, mình bắt đầu có ấn tượng và quyết tâm sau này sẽ phát triển Tool này. Và thật may mắn, qua nhiều năm nghiên cứu và học hỏi từ các nguồn mở, mình đã xây dựng và phát triển được bộ công cụ như các bạn thấy ở đây. Mặc dù mình đã cố gắng làm cho hoàn thiện nhất có thể, Tool vẫn sẽ không thể tránh khỏi những thiếu sót và sai sót, cũng như những hạn chế khi giải những bài khó. Vì thế nên mình rất hy vọng được các bạn góp ý để mình có cơ hội phát triển Tool thêm nữa. Cảm ơn và chúc bạn học tốt!

Lĩnh vực trọng tâm & Nghiên cứu
Sinh viên ngành Toán - TinBất đẳng thức · Tối ưu hóaTool Bất đẳng thứcPython · SymPy · CVXPY
2023
Nguồn cảm hứng
v7.1.6
Engine Core
100%
Độ tin cậy
Gửi Email
✣ 02 / BÀN LÀM VIỆC MẪU

Bàn Làm Việc Mẫu

Đã Xác Thực
λ

BÀN LÀM VIỆC

Problem PreviewSOS Mode
For all a,b,c≥0a, b, c \ge 0, prove that:
a(a−b)(a−c)+b(b−c)(b−a)+c(c−a)(c−b)≥0a\left(a - b\right)\left(a - c\right) + b\left(b - c\right)\left(b - a\right) + c\left(c - a\right)\left(c - b\right) \ge 0
Chọn mẫu ở trên để đổi lệnh
Mẫu thử
💡 Bạn có thể bôi đen để sao chép lệnh mẫu này.

BỘ XUẤT BẢN THẢO (EXPORT SUITE)

OVERLEAF READY

Xuất chứng minh bất đẳng thức thành bản thảo LaTeX độc lập với đầy đủ môi trường Theorem, Lemma và Proof sẵn sàng để nộp bài báo hoặc tài liệu nghiên cứu.

HIỆU NĂNG THỰC NGHIỆM ENGINE

v7.1.6 PRO

Đo lường trên bộ 150+ bài toán bất đẳng thức Olympiad (VMO, IMO, USAMO, Putnam). 100% chứng chỉ được nghiệm chứng trên trường số hữu tỉ ℚ.

Tốc Độ Khớp F
0.028s
Tiếp xúc vi sai bậc 2
Độ trễ trung bình / bài
Tính Sound Tuyệt Đối
100%
Số học hữu tỉ trên ℚ
0% sai số dấu phẩy động
Quỹ Đạo Đơn Thức
12,800+
Monomial Orbits / s
Tối ưu hóa đơn thức
Bậc Đa Thức Max
Bậc 12
Số mũ tối đa: 16
Căn thức, phân thức & khử tích
BẢO ĐẢM TÍNH SOUND TUYỆT ĐỐI:
Zero False Proof

Mọi kết quả PROVED đều đi kèm hàm tiếp xúc F(a,b,c) và phân tích phần dư SOS được kiểm chứng độc lập bởi Verifier đại số không dùng xấp xỉ số học.

✣ 03 / NĂNG LỰC HỆ THỐNG · WHAT YOU CAN DO

Từ Một Bất Đẳng Thức. Đến Một Chứng Minh Có Thể Kiểm Chứng.

DPSY kết hợp các công cụ xử lý bất đẳng thức để hỗ trợ khám phá hướng chứng minh, xây dựng chứng minh đại số và kiểm tra kết quả bằng tính toán chính xác.

01 · PHÂN TÍCH HỆ THỐNGDOMAIN: (a,b,c) ∈ ℝ₊³

Đưa Bất Đẳng Thức Vào Một Quy Trình Có Hệ Thống

Từ biểu thức ban đầu, tool hỗ trợ phân tích cấu trúc và tìm những hướng biến đổi phù hợp thay vì thử nghiệm thủ công một cách rời rạc.

Biểu thức ban đầu (Raw)Dạng chuẩn tắc đối xứng (Canonical)
ab+c+bc+a+ca+b≥32\displaystyle \frac{a}{b+c} + \frac{b}{c+a} + \frac{c}{a+b} \ge \frac{3}{2}
→
∑cycab+c≥32\displaystyle \sum_{\text{cyc}} \frac{a}{b+c} \ge \frac{3}{2}
Tự động nhận diện quỹ đạo hoán vị cyclic và ràng buộc miền biến số
02 · KHÁM PHÁ CHẶN ĐẠI SỐCONTACT: k=2

Khám Phá Chặn Đại Số Với DPSY

DPSY hỗ trợ xử lý nhiều lớp bài toán bất đẳng thức và tìm các biểu diễn đại số thuận lợi cho quá trình chứng minh.

Biểu diễn chặn cục bộ F(a,b,c)Tâm (1,1,1)
F(a,b,c)=8a−b−c4(a+b+c)F(a,b,c) = \frac{8a - b - c}{4(a+b+c)}
Cộng hoán vị đạt chặn đích:
∑cycF(a,b,c)=32\displaystyle \sum_{\text{cyc}} F(a,b,c) = \frac{3}{2}✓ PROVED
03 · CHỨNG MINH SOS

Chứng Minh Sum-of-Squares Chính Xác

Khi bài toán phù hợp, hệ thống đưa hiệu hai vế về chứng nhận không âm dưới dạng tổng bình phương trên trường hữu tỉ.

Đồng nhất thức phần dư SOSQ ⪰ 0
(2a−b−c)2≥0(2a - b - c)^2 \ge 0
Số học hữu tỉ trên ℚVERIFIED
04 · CĂN THỨC & PHÂN THỨC

Xử Lý Biểu Thức Khó Thao Tác Bằng Tay

Hỗ trợ các biểu thức căn thức, mẫu thức lệch và lũy thừa bậc cao, giảm thiểu sai sót biến đổi so với làm thủ công.

Căn thức đối xứng lồng nhauSign-Safe
∑cyca2+ab+b2≥3(a2+b2+c2)\sum_{\text{cyc}} \sqrt{a^2+ab+b^2} \ge \sqrt{3(a^2+b^2+c^2)}
Bảo toàn dấu tuyệt đối trước lũy thừa
05 · XÁC MINH ĐỘC LẬP

Kiểm Tra Kết Quả Trước Khi Tin Vào Nó

Các kết quả đại số quan trọng có thể được kiểm tra lại bằng số học chính xác và các bước xác minh độc lập, tránh sai số số thực.

Quy trình thẩm định100% Sound
Candidate F
Exact Check
Verified
Thẩm định độc lập 100% bằng số học hữu tỉ trên ℚ
QUY TRÌNH THAO TÁC LIỀN MẠCH

4 Bước Khám Phá & Chứng Minh Bất Đẳng Thức

Quy trình đại số chuẩn tắc • Không cài đặt phức tạp
STEP 01

Nhập bài toán

Đưa bất đẳng thức vào dưới dạng biểu thức toán học tự nhiên.

Natural Math AST
STEP 02

Khảo sát cấu trúc

Khảo sát quỹ đạo hoán vị, bậc thuần nhất và điều kiện biên.

Cyclic Orbit C₃
STEP 03

Dựng đồng nhất thức

Tìm hàm chặn cục bộ F và phân tích phần dư SOS chính xác.

Exact SOS Identity
STEP 04

Thẩm định 100% Sound

Kiểm tra lại toàn bộ chứng minh qua Replay Verifier hữu tỉ.

100% Exact Soundness
|dpsy-workspace / preview / vmo_benchmark.dpsy
EXACT VERIFIED ●
BÀI TOÁN ĐẦU VÀOAST Canonical
Miền & Ràng buộc:a,b,c≥0,a+b+c=3a,b,c \ge 0, \quad a+b+c=3
∑cycab2+1≥32\sum_{\text{cyc}} \frac{a}{b^2 + 1} \ge \frac{3}{2}
Dạng: Phân thức hoán vị ba biếnTự động nhận diện
CHỨNG CHỈ ĐẠT ĐƯỢC100% Soundness
Hàm tiếp xúc cục bộ: F(a,b,c)=4a−b−c+16\displaystyle F(a,b,c) = \frac{4a-b-c+1}{6}
Đẳng thức xảy ra khi: a=b=c=1a = b = c = 1
Kiểm tra đại số chính xác 100% qua Replay Verifier
Sẵn sàng chép LaTeX & xuất .texThử trên Bàn Làm Việc →
＋＋＋＋
TRIẾT LÝ HỆ THỐNG · PHILOSOPHY

Không thay thế tư duy chứng minh — mà mở rộng không gian bạn có thể khám phá.

Khám phá cấu trúc đại số · Tự động hóa tiếp tuyến cục bộ · Kiểm chứng chính xác trên ℚ.

100% Không trôi số thựcKhớp F tiếp xúc vi saiPhân rã SOS hữu tỉ
Bắt Đầu Với Bàn Làm Việc MẫuXem Thư Viện Kết Quả ↓
✣ 04 / THƯ VIỆN KẾT QUẢ

Từ Bất Đẳng Thức Olympiad Đến Chứng Nhận Đại Số Chính Xác.

Tuyển tập các bất đẳng thức đối xứng, phân thức và căn thức phức tạp đã được phân rã thành tổng bình phương và kiểm chứng độc lập.

CASE 01 · BÀI TOÁN TIÊU BIỂUĐiều kiện: a,b,c≥0a, b, c \ge 0
∑cyc(a2+ab+b2)(b2+bc+c2)≥(a+b+c)2\sum_{\text{cyc}} \sqrt{(a^2+ab+b^2)(b^2+bc+c^2)} \ge (a+b+c)^2
Hàm chặn cục bộ F:F(a,b,c)=b2+b(a+c)2+ac  ⟹  f2−F2=34b2(a−c)2≥0\displaystyle F(a,b,c) = b^2 + \frac{b(a+c)}{2} + ac \implies f^2 - F^2 = \frac{3}{4}b^2(a-c)^2 \ge 0
SOS Phần dư ≥ 0
CĂN THỨC ĐỐI XỨNG · DPSYĐÃ XÁC MINH CHÍNH XÁC

Bất đẳng thức Căn thức Đối xứng (Olympiad Classic)

Xử lý triệt để căn thức hai tầng không cần bình phương toàn cục, tự động khớp tiếp tuyến bậc hai và bảo toàn tính dương cục bộ.

Tiếp xúc bậc hai tại điểm đối xứng (1, 1, 1)
Phần dư phân rã SOS: ¾ b²(a-c)² ≥ 0 hiển nhiên
100% Hệ số hữu tỉ chính xác tuyệt đối
02EXACT SOS · ĐA THỨC
VERIFIED

Bất đẳng thức Schur Bậc 3 (Kinh điển SOS)

∑cyca(a−b)(a−c)≥0\sum_{\text{cyc}} a(a-b)(a-c) \ge 0
Điều kiện: a,b,c≥0a, b, c \ge 0

Khởi đầu mẫu mực cho mọi chứng minh SOS ba biến, đưa về tổng các đại lượng bình phương với trọng số thỏa mãn điều kiện Schur.

Đại số chính xác
Chi tiết
03EXACT SOS · PHÂN THỨC
VERIFIED

Bất đẳng thức Nesbitt (Dạng SOS Phân thức)

∑cycab+c≥32\sum_{\text{cyc}} \frac{a}{b+c} \ge \frac{3}{2}
Điều kiện: a,b,c>0a, b, c > 0

Phân tích chênh lệch f - 3/2 thành tổng các phân thức chính phương với mẫu số dương đối xứng.

Đại số chính xác
Chi tiết
04EXACT SOS · MA TRẬN GRAM
VERIFIED

Bất đẳng thức Bậc 4 Đối xứng (SOS Bậc 4)

a4+b4+c4+abc(a+b+c)≥2(a2b2+b2c2+c2a2)a^4+b^4+c^4 + abc(a+b+c) \ge 2(a^2b^2+b^2c^2+c^2a^2)
Điều kiện: ∀a,b,c∈R\forall a, b, c \in \mathbb{R}

Chứng minh tính không âm toàn cục trên R không cần giả thiết số dương nhờ cấu trúc ma trận Gram giải tích.

Đại số chính xác
Chi tiết
05DPSY CORE · PHÂN THỨC
VERIFIED

Nesbitt Phân thức (Mô hình Tuyến tính DPSY)

∑cycab+c≥32\sum_{\text{cyc}} \frac{a}{b+c} \ge \frac{3}{2}
Điều kiện: a,b,c>0a, b, c > 0

Minh họa cơ chế bất biến cyclic của DPSY: xây dựng hàm chặn cục bộ F có tổng đúng bằng hằng số biên.

Đại số chính xác
Chi tiết
06DPSY CHUẨN HÓA · VMO
VERIFIED

Cauchy Ngược Dấu (Chuẩn hóa a + b + c = 3)

∑cycab2+1≥32\sum_{\text{cyc}} \frac{a}{b^2+1} \ge \frac{3}{2}
Điều kiện: a,b,c>0, a+b+c=3a, b, c > 0, \ a+b+c = 3

Xử lý mẫu số bậc hai trên mặt phẳng chuẩn hóa affine a+b+c=3 bằng tiếp tuyến địa phương chuẩn xác.

Đại số chính xác
Chi tiết
BÀN LÀM VIỆC CHỨNG MINH THỰC THỤ

Muốn chứng minh một bất đẳng thức mới?

Nhập trực tiếp biểu thức trên Bàn Làm Việc để engine tự động phát hiện tiếp tuyến, phân rã hàm cục bộ và xuất chứng chỉ SOS đầy đủ.

Thử trên Bàn Làm Việc
✣ 05 / TIẾN TRÌNH TIẾN HÓA

Mỗi Phiên Bản Mở Rộng Một Lớp Bài Toán Mới.

Nhìn lại các cột mốc chính trong quá trình phát triển DPSY / SOS — từ nền tảng chứng minh đại số ban đầu đến engine hiện tại.

2023v4–v5NỀN TẢNG

Khởi Tạo Nhân Symbolic SOS & Parser Biểu Thức

Đặt nền móng cho xử lý tượng trưng và chứng nhận tổng bình phương SOS từ các công thức toán học tự nhiên.

Chuẩn hóa biểu thức và cấu trúc ngữ pháp toán học tự nhiên
Ánh xạ đa thức sang bài toán ma trận Gram bán xác định
Bộ kiểm chứng độc lập với số hữu tỉ chính xác tuyệt đối
MÔ HÌNH ĐẠI SỐv4–v5
P(x)=m(x)TQ m(x)≥0(Q⪰0)\mathcal{P}(x) = \mathbf{m}(x)^T Q \, \mathbf{m}(x) \ge 0 \quad (Q \succeq 0)
Biểu diễn ma trận Gram bán xác định dương
2024v6.xPHÂN RÃ ĐỐI XỨNG

Kiến Trúc Phân Rã Đối Xứng & Hạt Nhân Cyclic

Giới thiệu phương pháp phân rã cyclic dành cho bất đẳng thức ba biến, triệt tiêu bậc cao bằng không gian hạt nhân tổng bằng 0.

Phân rã cyclic qua không gian hạt nhân tổng bằng 0
Tự động tìm kiếm hàm chặn cục bộ hữu tỉ tối giản
Giảm bậc và cô lập các điểm kỳ dị đối xứng kinh điển
MÔ HÌNH ĐẠI SỐv6.x
∑cycf(a,b,c)≥Φ  ⟺  ∑cycF(a,b,c)=Φ,f≥F\sum_{\text{cyc}} f(a,b,c) \ge \Phi \iff \sum_{\text{cyc}} F(a,b,c) = \Phi, \quad f \ge F
Hàm chặn cục bộ F bảo toàn tổng cyclic
2025v7.0ĐỘ ỔN ĐỊNH & CĂN THỨC

Kiểm Soát Dấu Căn Thức An Toàn & Cách Ly Tiến Trình

Mở rộng khả năng xử lý căn thức phức tạp và tăng độ ổn định của pipeline tính toán với cơ chế kiểm tra dấu an toàn.

Cơ chế Sign-Safe loại bỏ hoàn toàn hiện tượng bình phương mù
Quản lý thời gian tính toán và cách ly tiến trình độc lập
Xuất gói chứng chỉ (proof bundle) có thể kiểm tra lại độc lập
MÔ HÌNH ĐẠI SỐv7.0
F(a,b,c)=F0+K(a,b,c)D(a,b,c),∑cycK=0F(a,b,c) = F_0 + \frac{K(a,b,c)}{D(a,b,c)}, \quad \sum_{\text{cyc}} K = 0
Chặn cục bộ phân thức khử căn thức an toàn
THẾ HỆ HIỆN TẠIv7.1.62026
100% EXACT SOUND VERIFIED

Thế Hệ Hiện Tại Của DPSY / SOS

Mở rộng khả năng xử lý các bài toán căn thức phức tạp, tích hợp ma trận Gram trên trường đại số và xuất chứng nhận SOS chính xác tuyệt đối.

QUY TRÌNH CHỨNG MINH ĐẠI SỐ CHÍNH XÁC (v7.1.6)
1. Biểu thức Đầu vào
f(a,b,c)≥0f(a,b,c) \ge 0
Đa thức, phân thức hoặc căn thức
2. Phân rã Cục bộ & Khớp Tiếp tuyến
f−F≥0,∑cycF=Φ\displaystyle f - F \ge 0, \quad \sum_{\text{cyc}} F = \Phi
Khớp tiếp điểm bậc 2 & Sign-Safe
3. Chứng chỉ SOS Hoàn tất
MP=∑wiqi2≥0\displaystyle M P = \sum w_i q_i^2 \ge 0
✓ Xác minh hữu tỉ độc lập
01 · Căn thức

Xử Lý Căn Thức Hai Tầng

Giải quyết căn thức phân thức và căn thức đối xứng phức tạp bằng tiếp tuyến cục bộ, không cần bình phương mù.

02 · Chứng nhận SOS

Tổng Bình Phương Chính Xác

Phân rã đa thức và phần dư thành các bình phương thực với hệ số hữu tỉ hoặc mở rộng đại số chính xác.

03 · Xác minh độc lập

Kiểm Chứng Không Xấp Xỉ

Mọi chứng chỉ đầu ra đều được kiểm tra độc lập bằng công cụ đại số giải tích, loại bỏ hoàn toàn sai số làm tròn.

LỘ TRÌNH TIẾP THEO
DPSY v8+ĐANG NGHIÊN CỨU
Định hình thế hệ tiếp theo

Những hướng nghiên cứu đang được khám phá nhằm mở rộng phạm vi bài toán và nâng cao khả năng chứng minh hình thức.

01 · Đa biến mở rộng

Bài Toán Đa Biến (n ≥ 4)

Mở rộng thuật toán phân rã đối xứng và chặn cục bộ sang các bất đẳng thức n biến tổng quát.

02 · Chứng minh hình thức

Tích Hợp Lean 4 Formalizer

Tự động xuất chứng chỉ đại số sang mã chứng minh hình thức được kiểm chứng bởi kernel của Lean 4.

03 · Hạ tầng tính toán

Pipeline Phân Tán Hiệu Năng Cao

Tối ưu hóa thuật toán tìm kiếm và xử lý song song cho các bài toán phân rã bậc cao quy mô lớn.