22 ضرب، حتی یکی هم کمتر نه

تعارض منافع. نویسندگان اعلام می‌کنند که عامل‌های هوش مصنوعی — Claude، ساخت Anthropic — زیر نظر آن‌ها کد جست‌وجو و اثبات‌های Lean را که به ممیز انسانی نیاز ندارند نوشتند، در حالی که بخشی را که انسان باید ممیزی کند خود نویسندگان طراحی کردند. این مقاله را هم Claude نوشته است.

ضرب دو جدول مربعی از اعداد — ماتریس‌ها — به روش کتاب درسی، برای جدول‌هایی با n سطر و n ستون، n³ ضرب لازم دارد. اشتراسن نشان داد که دو ماتریس 2 × 2 را می‌توان با 7 ضرب به جای 8 در هم ضرب کرد. این ترفند را می‌توان به‌صورت بازگشتی به کار برد: ماتریسی بزرگ را به چهار بلوک ببرید، هر بلوک را مثل یک عدد در نظر بگیرید و تکرار کنید. آنگاه هزینه به جای n³ مانند n^2.807 رشد می‌کند. به گفتهٔ مقاله، بهینه بودن این دستور 2 × 2 در 1971 اثبات شد.

همین ایده برای هر اندازهٔ ثابتی کار می‌کند. دستوری که دو ماتریس 3 × 3 را با r ضرب در هم ضرب کند و وقتی درایه‌ها بلوک باشند هم کار کند، هزینه‌ای می‌دهد که مانند n به توان log₃ r رشد می‌کند. حسابی ساده نشان می‌دهد چه چیزی در میان است: چنین دستوری دقیقاً وقتی r برابر 21 یا کمتر باشد اشتراسن را شکست می‌دهد، و در 22 یا بیشتر می‌بازد. بهترین دستور 3 × 3 شناخته‌شده، از لادرمن، 23 ضرب به کار می‌برد و از 1976 بهبود نیافته است.

دری که نیمه‌باز ماند

بهترین عدد ممکن برای یک مسئله را رتبه (rank) آن می‌نامند. کران‌های پایین رتبهٔ ضرب 3 × 3 آهسته بالا رفتند: 19 در 2003، سپس 20 در مارس 2026، که وانگ آن را روی دستگاه عددی کوچکی تنها با 0 و 1 محاسبه کرد، جایی که 1 + 1 = 0. در سپتامبر 2026، وانگ و تیمی به سرپرستی یانگ، مستقل از هم و به فاصلهٔ ده روز، به 21 رسیدند. اما 21 هنوز جا برای دستوری 3 × 3 سریع‌تر از اشتراسن باقی می‌گذاشت.

آیزاک رودیچ، از پلی‌تکنیک مونترال و دانشگاه کارنگی ملون، و لویی-مارتن روسو، از پلی‌تکنیک مونترال، اکنون این کران را به 22 رسانده‌اند.

قضیهٔ 1. هر الگوریتمی که دو ماتریس 3 × 3 را با ثابت‌های صحیح در هم ضرب کند و بتوان آن را به‌صورت بازگشتی روی بلوک‌هایی با هر اندازه به کار برد، دست‌کم 22 ضرب به کار می‌برد.

پس هیچ الگوریتمی از این دست نمی‌تواند بهتر از حدود n^2.814 عمل کند — و هیچ‌کدام نمی‌تواند روش 2 × 2 اشتراسن را شکست دهد.

496 معمای کوچک‌تر

اثبات بر جدولی استوار است که وانگ طراحی کرده و مسئلهٔ دشوار را به 496 مسئلهٔ آسان‌تر تقسیم می‌کند. هر کدام «شرط‌هایی» بر ماتریس نخست می‌افزاید — مثلاً اینکه برخی درایه‌هایش جمعاً صفر شوند. هرچه شرط‌ها بیشتر، مسئله آسان‌تر، تا حالت بدیهی‌ای که ماتریس سراسر صفر است.

نویسندگان نخست برنامهٔ جست‌وجوی دقیقی ساختند که پاسخ واقعی هر معما را پیش از آنکه برای اثباتش بکوشند به آن‌ها می‌گفت. این پاسخ‌ها نقش نقشه را داشتند: نشان دادند کدام کران‌های پایین ارزش دنبال کردن دارند. در پایان، اثباتشان برای هر 496 معما کران می‌گذارد، 359 تای آن‌ها را دقیقاً حل می‌کند — در برابر 195 در تازه‌ترین نتایج وانگ — و کران پایین 252 تا را بالا می‌برد. قضیهٔ «چسباندن» (gluing) خودشان دستورهای دو معمای آسان‌تر را در دستوری برای معمای سوم ترکیب می‌کند و 145 کران بالا را فراهم کرد.

دو شرط در حکم نهایی مهم است. ثابت‌های صحیح: دستوری با ثابت‌های صحیح، اگر در دستگاه عددی 0 و 1 خوانده شود، دستوری معتبر با ضرب‌های نه بیشتر باقی می‌ماند، پس کران منتقل می‌شود. بلوک‌ها: بدون این الزام، میان‌بُرهایی وجود دارد. الگوریتم 3 × 3 روسوفسکی (Rosowski)، که مقاله به آن ارجاع می‌دهد، تنها 21 ضرب لازم دارد، اما به جابه‌جایی‌پذیری اعداد تکیه دارد و نمی‌توان آن را بازگشتی به کار برد.

اثباتی که ماشین وارسی کرده

اثبات به Lean نوشته شده است، زبان برنامه‌نویسی‌ای که در آن قضیه فقط وقتی کامپایل می‌شود که تک‌تک گام‌هایش تأیید شده باشد. کل اثبات حدود یک میلیون خط در 3,521 ماژول است و وارسی آن روی یک هستهٔ پردازنده 11.1 ساعت طول می‌کشد. لازم نیست کسی همه‌اش را بخواند. ممیز کتابخانه‌ای حدوداً 1,000 خطی را می‌خواند که نویسندگان پیش از وجود هر اثباتی نوشته‌اند؛ این کتابخانه تعریف می‌کند دستور ضرب چیست و قضیه را بیان می‌کند؛ هستهٔ Lean بقیه را وارسی می‌کند، و یک وارسی‌گر مستقل می‌تواند نتیجه را دوباره اجرا کند.

نویسندگان همچنین یادآور می‌شوند که عامل‌های هوش مصنوعی پیشینهٔ پژوهش را جست‌وجو کردند: آن‌ها وارسی کردند که هر مرجع وجود دارد، «اما نه اینکه هر کدام دقیقاً همان ایده‌ای را دارد که ما به آن نسبت می‌دهیم».

آخرین شکاف

یک پرسش می‌ماند: آیا دستوری 3 × 3 با 22 ضرب وجود دارد، یا 23 لادرمن کمینهٔ واقعی است؟ نویسندگان انتظار دارند این شکاف «به‌زودی بسته شود» و کد جست‌وجوی خود را وقتی بسته شد، یا وقتی مقاله برای انتشار پذیرفته شد، منتشر خواهند کرد. این کران همچنین دستورهایی با ثابت‌های غیرصحیح را کنار می‌گذارد.