‏درس تلخ اثبات خودکار قضیه‌ها با هوش مصنوعی

جان لوبر تو این مقاله تجربه‌ی شخصیش از ساختن یه اثبات‌گر خودکار قضیه رو تعریف می‌کنه. اون از ۲۰۱۳ معتقد بود که هوش مصنوعی یه روز تحقیقات ریاضی رو به دست می‌گیره. به گفته‌ش، پیشرفت واقعی از اواخر ۲۰۲۴ با مدل‌های reasoning (یعنی مدل‌هایی که قبل از جواب دادن بیشتر فکر می‌کنن) شروع شد و امسال با ترکیب این مدل‌ها و Lean (یه زبان برای اثبات رسمی که درستی هر قدم رو ماشینی چک می‌کنه) راه باز شد.

برخلاف بیشتر آدم‌های این حوزه که اول اثبات رو به‌صورت متنی می‌نوشتن و بعد رسمیش می‌کردن، لوبر همه‌چیز رو مستقیم تو Lean انجام داد. چون فکر می‌کرد مدل‌ها بدون چک رسمی نمی‌تونن یه استدلال صدصفحه‌ای رو درست نگه دارن. برای همین یه fork خصوصی از Lean4 ساخت، یه harness اختصاصی نوشت که کار رو بین کلی subagent پخش می‌کرد، و حتی یه متابرنامه ساخت که برنامه‌های C++ موازی برای پیدا کردن مثال نقض تولید می‌کرد.

با GPT-5.5 سیستمش چند قضیه‌ی جدید ثابت کرد ولی کند بود. با GPT-5.6 Sol کیفیت بالاتر رفت و چند صد هزار خط Lean برای مسئله‌ی گراف Moore درجه‌ی ۵۷ و حدس Hadwiger تولید کرد، ولی اثبات Hadwiger هیچ‌وقت کامل نشد. بعد GPT-6 Astra اومد، چند روز بعدش مسئله‌ی Navier-Stokes حل شد و لوبر کار رو ول کرد.

چهار هفته بعد، OpenAI یه مدل منتشرنشده رو روی ۴۰۰۰ مسئله‌ی مهم اجرا کرد، به‌طور متوسط حدود ۳.۵ ساعت محاسبه برای هر مسئله. نتیجه یه ریپو با صدها نتیجه‌ی مهم بود، از جمله رد حدس Hadwiger با یه استدلال احتمالاتی. یعنی دلیل اینکه اثبات لوبر هیچ‌وقت بسته نمی‌شد این بود که حدس اصلاً غلط بود.

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

لوبر معتقده ریاضی حالا دو تیکه می‌شه: برای آدم‌ها بیشتر شبیه علوم انسانی می‌شه که به خاطر لذت یادگیری خونده می‌شه، و بخش کشف کاملاً دست هوش مصنوعی می‌افته. اون اول از کوتاه بودن دوره‌ی همکاری انسان و AI ناراحت بود، ولی حالا فکر می‌کنه این معامله‌ی خوبیه و همین اتفاق به‌زودی برای رشته‌های دیگه هم می‌افته.

نکات کلیدی:

• اثبات‌گر نویسنده روی یه fork خصوصی از Lean4 و یه harness چندعاملی اختصاصی ساخته شده بود.
• GPT-5.5، GPT-5.6 Sol و GPT-6 Astra هر کدوم یه جهش محسوس تو توانایی اثبات داشتن.
• OpenAI یه مدل جدید رو روی ۴۰۰۰ مسئله با حدود ۳.۵ ساعت محاسبه برای هر کدوم اجرا کرد و صدها نتیجه گرفت.
• حدس Hadwiger با یه استدلال احتمالاتی رد شد، بدون معرفی یه مثال نقض مشخص.
• حدود نصف نتایج ادعاشده هنوز اثبات رسمی Lean ندارن.