یک هوش مصنوعی معمای رنگ‌آمیزی را می‌گشاید
شبکه‌ای از نقطه‌ها را در نظر بگیرید که با خط‌هایی به هم وصل شده‌اند — چیزی که ریاضی‌دانان گراف می‌نامند. حالا نقطه‌ها را طوری رنگ کنید که دو نقطهٔ متصل با یک خط هرگز هم‌رنگ نباشند. کمترین تعداد رنگی که جواب می‌دهد عدد رنگی گراف است. یک حالت خاص مشهور، قضیهٔ چهار رنگ است که در 1977 اثبات شد و عنوانش همه چیز را می‌گوید: «Every planar map is four colorable» (هر نقشهٔ مسطح را می‌توان با چهار رنگ رنگ‌آمیزی کرد).
شرط‌بندی هادویگر در 1943
در 1943، هادویگر قاعده‌ای فراگیر برای همهٔ گراف‌ها پیشنهاد کرد. گرافی را با حذف نقطه‌ها یا خط‌ها، و با ادغام دو نقطهٔ متصل در یک نقطه، کوچک کنید. نتیجه را مینور می‌نامند. هادویگر به بزرگ‌ترین گراف کامل — خوشه‌ای که در آن هر نقطه به همهٔ نقطه‌های دیگر وصل است — که از این راه به دست می‌آید نگاه کرد و حدس زد که تعداد رنگ‌های لازم هرگز از اندازهٔ این خوشه فراتر نمی‌رود.
مقاله آن را «از کهن‌ترین و بنیادی‌ترین مسائل نظریهٔ گراف» می‌خواند. این حدس فقط برای حالت‌های کوچک اثبات شده است: تا خوشه‌های پنج‌تایی، که معلوم می‌شود هم‌ارز قضیهٔ چهار رنگ است یا به آن تحویل‌پذیر است. از شش به بعد، باز است.
نزدیک شدن، یک لگاریتم در هر بار
چون صورت دقیق مقاومت می‌کند، پژوهشگران کوشیدند تعداد رنگ‌ها را با تابعی از اندازهٔ خوشه که تا حد ممکن کند رشد کند کران‌دار کنند. مقاله این پیشرفت را روایت می‌کند. ده‌ها سال، بهترین کران اندکی سریع‌تر از رشد متناسب بالا می‌رفت — با ضریبی شامل ریشهٔ دوم یک لگاریتم. چند سال پیش، نورین، پوستل و سونگ این سد را شکستند. سپس دلکور و پوستل آن را بیشتر بهبود دادند و، مهم‌تر از همه، نشان دادند که پرداختن به گراف‌های نسبتاً کوچک کافی است. لیو و لوئو ضریب اضافی را تا لگاریتم سه‌گانه پایین آوردند.
مقصد طبیعی حدس خطی هادویگر است: مضرب ثابتی از اندازهٔ خوشه همیشه کافی است. این همان چیزی است که سرگئی نورین از دانشگاه مک‌گیل در مونترال و رافائل اشتاینر از ETH زوریخ اکنون مدعی اثباتش هستند.
نقشی که ماشین ایفا کرد
نویسندگان صریح‌اند: اثبات را GPT-6 Astra، مدلی از OpenAI، با پیروی از رهنمودهای آن‌ها یافت. ابتدا از آن خواستند حالت گراف‌های بسیار چگال را اثبات کند، که به باورشان تکهٔ گم‌شده بود. به نوشتهٔ آن‌ها، «تنها پس از چند ساعت و کمی تشویق» موفق شد. وقتی از آن خواسته شد یک وابستگی را صریح کند، گراف‌ها را تا اندازهٔ معینی پوشش داد — اما نه کاملاً بازهٔ لازم را. سپس از آن ایده‌ای بدیع برای پر کردن شکاف خواستند که گام «خودراه‌انداز» (bootstrap) اثبات نهایی را پدید آورد. به گفتهٔ آن‌ها، تقریباً هیچ‌یک از ایده‌های اثباتی خاص خودشان باقی نماند، جز یک پیشنهاد دربارهٔ انقباض‌ها.
نگارش انسانی است. مدل دیگری از OpenAI در ویرایش و کتاب‌نامه کمک کرد. نویسندگان گزارش می‌کنند که Codex از OpenAI نسخه‌ای صوری و قابل وارسی با ماشین از کل اثبات را در دستیار اثبات Lean تولید کرد که همراه با پیش‌نویس اولیه‌ای که هوش مصنوعی نوشته بود به‌صورت برخط منتشر شده است. آن‌ها مسئولیت کامل ریاضیات را بر عهده می‌گیرند.
درون اثبات
استدلال دو نیمه دارد:
- گراف‌های کوچک، رنگ‌های اندک. برای گراف‌هایی که چندان بزرگ‌تر از حد خوشه نیستند، نویسندگان نشان می‌دهند که حدود چهار برابر اندازهٔ خوشه کافی است. نقطهٔ آغاز نتیجه‌ای از رید و سیمور در 1998 است: شکلی آزادتر و «کسری» از رنگ‌آمیزی، همین حالا با ضریب دو از قاعدهٔ خطی پیروی می‌کند. کار تازه رنگ‌آمیزی‌های کسری را با افزودن چند خط اضافی به گراف و یافتن جورسازی‌های (matching) عظیم در یک ساختار کمکی، به رنگ‌آمیزی‌های واقعی تبدیل می‌کند.
- یک خودراه‌اندازی. استدلال دوم در هر گام، بازهٔ اندازه‌های گراف تحت پوشش را با ضریب چهار سوم در نما گسترش می‌دهد، به بهای ثابتی بزرگ‌تر. ده گام بازه را از یک‌سوم به حدود 5.92 می‌رساند، فراتر از آستانهٔ 5 که تحویل دلکور-پوستل لازم دارد. این نیمه از ترفندی قدیمی متعلق به جارفاش (Gyárfás) استفاده می‌کند که به گفتهٔ نویسندگان هرگز روی این مسئله به کار نرفته بود.
نویسندگان اثبات را ساخته‌شده از ابزارهای شناخته‌شده توصیف می‌کنند — «درون پوش محدب نتایج موجود،» اما نه بر لبهٔ آشکاری از آن.
آنچه باز می‌ماند
ثابت عظیم است: برآوردی سرانگشتی حدود 10¹⁰⁰ به دست می‌دهد. نویسندگان جا برای پایین آوردن آن به زیر 10¹⁰ می‌بینند، اما گمان می‌کنند رسیدن به مثلاً 100 به ایده‌های تازه نیاز دارد. حدس دقیق هادویگر دست‌نخورده مانده است: می‌نویسند «ما مردّدیم.» مقاله پیش‌چاپ است؛ 41 صفحه ریاضیات تازه اکنون باید از بوتهٔ نقد دیگر متخصصان بگذرد.