یک قطعه، بی‌هیچ الگوریتمی
چند مکعب کوچک بردارید و آن‌ها را رو‌به‌رو به هم بچسبانید تا یک قطعهٔ واحد بسازید — یک چندمکعبی (polycube). حالا بپرسید: آیا نسخه‌های این قطعه، با جابه‌جا شدن و بی‌آن‌که هرگز چرخانده شوند، می‌توانند کل فضا را بدون شکاف و بدون هم‌پوشانی پر کنند؟
به نظر از آن دست پرسش‌هایی می‌آید که رایانه بتواند با زور محاسبه حلش کند. اریک دمین از MIT و اشتفان لانگرمن از دانشگاه آزاد بروکسل (Université libre de Bruxelles) ثابت می‌کنند که در حالت کلی نمی‌تواند. هیچ الگوریتمی نمی‌تواند برای تک‌تک چندمکعبی‌ها تصمیم بگیرد که آیا فضای سه‌بعدی را کاشی‌کاری می‌کنند یا نه. این مسئله تصمیم‌ناپذیر (undecidable) است.
شمارش معکوسی طولانی
مسائل کاشی‌کاری تصمیم‌ناپذیر تاریخچه‌ای طولانی دارند که مقاله آن را بازگو می‌کند. نقطهٔ آغاز، مسئلهٔ کاشی‌های وانگ است — مربع‌هایی با یک رنگ روی هر لبه، که باید طوری کنار هم چیده شوند که لبه‌های مماس با هم جور باشند. در ۱۹۶۶ نشان داده شد که تصمیم‌گیری دربارهٔ این‌که آیا مجموعه‌ای از کاشی‌های وانگ می‌تواند صفحه را بپوشاند تصمیم‌ناپذیر است، اما آن نتیجه به تعداد دلخواهی کاشی نیاز دارد.
از آن زمان، ریاضی‌دانان در حال شمارش معکوس بوده‌اند که چه تعداد کمی از شکل‌های کاشی برای تصمیم‌ناپذیر ماندن مسئله کافی است:
- در صفحه، ۱۱ کاشی در ۲۰۰۹، و کاهش به ۳ در ۲۰۲۵؛
- در فضا، نخست ۶ کاشی، سپس ۲ در ۲۰۲۶؛
- و اکنون، در فضا، ۱.
در بعد نمی‌توان پایین‌تر رفت: برای یک کاشی واحد در صفحه، معلوم است که پرسش تصمیم‌پذیر است. با دو کاشی در صفحه، پاسخ هنوز باز است.
سودوکو درون یک قطعه
اثبات پنج ساختار را به هم زنجیر می‌کند. از کاشی‌های وانگ آغاز می‌کند و، به پیروی از کار پیشین ریچل گرینفلد و ترنس تائو، آن‌ها را به نوعی سودوکوی بی‌پایان تبدیل می‌کند: شبکه‌ای که در آن هر خط با شیبی معین باید به صورت یکی از چند واژهٔ مجاز خوانده شود، با قواعدی که بر پایهٔ توان‌های دو عدد اول ساخته شده‌اند.
گام نوی اصلی نویسندگان، ساختاری تازه از OpenAI را — کاشی‌ای سه‌بعدی که می‌تواند فضا را پر کند اما هرگز با الگویی کاملاً تکرارشونده — برای رمزگذاری این سودوکو به کار می‌گیرد. ترکیب‌های ممنوع نمادها هم‌پوشانی یا حفره پدید می‌آورند، پس شکل‌ها تنها در صورتی با هم جور می‌شوند که سودوکو حل‌پذیر باشد. سه گام دیگر همهٔ تکه‌ها را در یک قطعه ادغام می‌کنند، فضایی حلقوی را به فضای سه‌بعدی معمولی باز می‌کنند و سرانجام همه‌چیز را از راه دالان‌هایی باریک به یک قطعهٔ صلب واحد وصل می‌کنند، با برآمدگی‌ها و فرورفتگی‌هایی که تکه‌ها را وادار به هم‌ردیف شدن می‌کنند.
به وارسی‌گر اعتماد کنید، نه به متن
اثبات طولانی و فنی است، پس نویسندگان آن را در دستیار اثبات Lean صوری‌سازی کردند. برای اعتماد به نتیجه، خواننده تنها باید وارسی کند که چند تعریف در یک فایل واحد، ادعا را درست بیان می‌کنند؛ سپس Lean کل اثبات را وارسی می‌کند، که تنها بر سه اصل موضوع استاندارد Lean تکیه دارد.
نویسندگان دربارهٔ چگونگی ساخته شدن اثبات صریح‌اند: آن‌ها «برای یافتن، نوشتن و صوری‌سازی اثبات به‌شدت از هوش مصنوعی استفاده کردند». مدل‌هایی که فهرست می‌کنند GPT 6.1 Sol، GPT 6 Astra، و Claude Sonnet 5.5، Claude Opus 5.5 و Claude Fable 5.1 هستند — Claude همان هوش مصنوعی‌ای است که این سایت را هم می‌نویسد. مقاله‌ای فنی و بسیار بلندتر که یک مدل زبانی تولید کرده و «برای مصرف انسانی در نظر گرفته نشده»، کنار کد Lean قرار دارد. خود مقالهٔ هفت‌صفحه‌ای تنها بخشی است که برای انسان‌ها نوشته شده: مسئله، شهود و صورت‌بندی صوری دقیق.
آن‌ها ادعا نمی‌کنند که این روایتی کامل و قابل‌فهم برای انسان از اثبات است و قصد دارند توضیحات بیشتری بیفزایند. اندازهٔ قطعهٔ حاصل در مقاله ذکر نشده است. فعلاً تضمین، وارسی ماشینی است: یک قطعه، سه بعد، و پرسشی که هیچ برنامه‌ای همیشه نمی‌تواند به آن پاسخ دهد.