‏Claude فرضیهٔ زمان نمایی (ETH) رو رد کرد

یه مدل تحقیقاتی داخلی Claude تو Anthropic یه الگوریتم قطعی (deterministic) پیدا کرده که مسئلهٔ 3-SAT رو با n متغیر در زمان 2^o(n) حل می‌کنه. 3-SAT یعنی اینکه بفهمیم یه فرمول منطقی که هر بندش سه متغیر داره، اصلاً جوابی داره که درستش کنه یا نه. این نتیجه Exponential Time Hypothesis یا ETH رو رد می‌کنه. ETH یه فرض مهم تو نظریهٔ پیچیدگی بود که می‌گفت 3-SAT رو نمی‌شه سریع‌تر از زمان نمایی حل کرد.

الگوریتم در واقع یه مسئلهٔ سخت‌تر رو هم حل می‌کنه: #3-SAT، یعنی شمردن تعداد همهٔ جواب‌های درست یه فرمول. زمانش 2^O(n log log n / √log n) هست. خود مخزن تأکید می‌کنه که این نتیجه کاملاً مجانبی (asymptotic) هست، یعنی فقط برای nهای خیلی بزرگ معنی داره و دربارهٔ حل فرمول‌ها تو دنیای واقعی حرفی نمی‌زنه.

کنار مقاله، یه اثبات رسمی به زبان Lean 4 هم منتشر شده که اونم مدل‌های AI نوشتن. Lean یه زبان اثباته که کامپیوتر باهاش خط‌به‌خط درستی یه اثبات ریاضی رو چک می‌کنه. فایل MainResults.lean دو قضیه رو روی ماشین‌های تورینگِ Mathlib بیان می‌کنه: ETHIsFalse و MainTheorem. این فایل هیچ اثباتی نداره و فقط Mathlib رو import می‌کنه.

طبق توضیح مخزن، Lean اثبات‌ها رو چک می‌کنه ولی هیچ ماشینی چک نمی‌کنه که MainResults.lean دقیقاً همون حرف مقاله رو می‌زنه. برای همین این فایل رو عمداً کوتاه نگه داشتن تا خود خواننده بتونه مقایسه‌ش کنه. پیوست E مقاله هم همین فایل رو چاپ کرده و تفاوت‌هاش با صورت چاپی قضیه‌ها رو گفته.

به گفتهٔ مخزن، build حدود ۸ دقیقه روی ۲۴ CPU مجازی طول کشیده و بزرگ‌ترین پروسه‌ش حدود 7 GB حافظه گرفته. چک نهایی نشون می‌ده هر دو قضیه فقط به سه axiom استاندارد Lean تکیه دارن: propext، Classical.choice و Quot.sound. CI مخزن هم با ابزار Comparator صورت قضیه‌ها رو با Challenge.lean مقایسه می‌کنه و اثبات‌ها رو با یه kernel مستقل دیگه به اسم nanoda دوباره چک می‌کنه.

یه نکتهٔ جالب دیگه اینه که مخزن یه توضیح خیلی فشرده از ایدهٔ اصلی گذاشته و می‌گه Claude Opus 5.5 با effort بالا می‌تونه از روی همین چند خط، رد ETH رو دوباره اثبات کنه. ایده حول contract کردن tensor networkها می‌چرخه، یعنی ادغام یه شبکه از تنسورها تا به یه عدد برسیم. البته چیزی که از این توضیح بازسازی می‌شه فقط اینه که 3-SAT برای هر δ مثبت در زمان O(2^(δn)) حل می‌شه، نه کران دقیق‌ترِ مقاله.

نکات کلیدی:

• الگوریتم قطعیه و 3-SAT رو در زمان 2^o(n) حل می‌کنه، پس ETH غلطه.
• نسخهٔ شمارشی، یعنی #3-SAT، در زمان 2^O(n log log n / √log n) حل می‌شه.
• اثبات با Lean 4 و Mathlib نسخهٔ v4.33.1 نوشته شده و فقط به سه axiom استاندارد Lean تکیه داره.
• اثبات‌ها با kernel دوم و مستقلی به اسم nanoda هم دوباره چک می‌شن.
• نتیجه صرفاً مجانبیه و برای حل SAT تو عمل فعلاً چیزی عوض نمی‌کنه.
• مخزن با لایسنس Apache 2.0 منتشر شده و نگهداری نمی‌شه.