وقتی AI ریاضی رو حل می‌کنه، ریاضی‌دان بودن یعنی چی؟
هوش مصنوعیClaude Opus 4.8خلاصهٔ کامل‌تر
نویسنده، بنجامین اسکیوز، از تجربهٔ دورهٔ دکتری خودش شروع می‌کنه و می‌گه حالا می‌فهمه هم‌اتاقی‌های ریاضی محضش چرا سال‌ها روی مسائلی کار می‌کردن که فقط چند نفر تو دنیا براشون مهم بود: اون‌ها از خودِ مسیرِ طولانیِ فهمیدن لذت می‌بردن. به گفتهٔ جرمی اویگاد از کارنگی ملون، «گاهی فهمیدن فقط به نظرت خیلی زیبا میاد».
ولی سرعت پیشرفت AI داره همین فرآیند کند و تأملی رو دور می‌زنه. مقاله یادآوری می‌کنه که تابستون پارسال سیستم‌های گوگل دیپ‌مایند و OpenAI به سطح مدال طلای المپیاد جهانی ریاضی رسیدن. امسال سیستم آزمایشی دیپ‌مایند به اسم Aletheia به‌شکل خودمختار نتیجه‌ای در سطح پژوهش دکتری تولید کرد و یه مدل عمومی از OpenAI هم یه حدس مهم در هندسهٔ ترکیبیاتی رو رد کرد — کاری که اگه انسان انجامش داده بود، ارزش انتشار تو یه ژورنال درجه‌یک رو داشت.
تحول دوم از ترکیب مدل‌های زبانی با دستیارهای اثبات مثل Lean و Isabelle و Rocq اومده. این‌ها زبان‌های تخصصی‌ای هستن که هر گام یه اثبات رو بررسی می‌کنن. تا حالا ترجمهٔ دستی اثبات به این فرم — یعنی فرمال‌سازی — یه گلوگاه پرزحمت بود؛ حالا مدل‌ها دارن همین ترجمه رو خودکار می‌کنن. نمونه‌ش شرکت Math, Inc. که با ایجنت Gauss اول به آدم‌ها کمک کرد اثبات ویازوسکا برای بسته‌بندی کره در ۸ بعد رو فرمال کنن و بعد حالت ۲۴ بعدی رو تو دو هفته به‌تنهایی فرمال کرد.
واکنش جامعه اما یکدست نیست. تو دوازدهمین فروم لاریت هایدلبرگ، نویسنده می‌گه اضطراب تو سالن حس می‌شد؛ یانگ-هویی هی جملهٔ ماندگاری گفت که ریاضی‌دان‌های انسانی ممکنه به «کشیشانِ اوراکل‌ها» تبدیل شن. جسیکا رندال هم تعریف می‌کنه که یه ترس وجودی جمعی بین ریاضی‌دان‌های جوان شکل گرفته بود.
مقاله سه آیندهٔ ممکن رو کنار هم می‌ذاره: AI به‌عنوان ابزار که اولویت با فهم انسانه، AI به‌عنوان شریک که کشف مشترک اهمیت داره، و AI به‌عنوان اوراکل که فقط جواب مهمه. آکشای ونکاتش از پرینستون طرف دیدگاه انسان‌محوره و می‌گه ریاضی صرفاً توصیف پدیده‌های عددی نیست، «راهیه برای اینکه همه سر یه معنا به توافق برسیم».
مایا فریزر از دانشگاه اتاوا هم اضافه می‌کنه که حتی اگه AI یه حدس رو ثابت کنه، پیدا کردن یه اثبات زیبا و قابل‌فهم برای انسان هنوز یه مسئلهٔ باز و ارزشمنده. در مقابل، ترنس تائو دیدگاه همکارانه‌تری داره: او از «ریاضیات بزرگ» حرف می‌زنه، یعنی همکاری‌های گستردهٔ غیرمتمرکز بین آدم‌ها و ماشین‌ها که آدم بخش خلاق رو برمی‌داره و AI کار فنی سنگین رو.
کلید دیدگاه تائو هم فرمال‌سازیه: وقتی اثبات به کد ترجمه و گام‌به‌گام بررسی میشه، اعتماد به‌جای شهرت و رابطه، از راه راستی‌آزمایی ساخته میشه؛ پس ایدهٔ یه پژوهشگر ناشناس یا حتی آماتور هم اگه اثبات فرمال داشته باشه جدی گرفته میشه.
نگرانی‌ها اما جدی‌ان. اگه فرآیند کند و عمیق ریاضی دیگه برای جامعه و بودجه‌دهنده‌ها ارزش نداشته باشه، ریاضی ممکنه به فعالیتی نخبه‌گرا تبدیل شه که فقط سازمان‌های دارای مدل‌های اختصاصی انجامش می‌دن. ونکاتش می‌پرسه اگه کامپیوتر بخش بزرگی از فکر کردن رو برات انجام بده، هنوز انگیزهٔ صرف اون سال‌ها رو داری؟ و اگه دانشجوها همیشه مستقیم برن سراغ جواب، شهود شخصی‌شون از کجا ساخته میشه؟
نکات کلیدی:
- مدل‌ها از مدال طلای المپیاد تا رد کردن یه حدس منتشرنشده پیش رفتن
- ترکیب LLM با دستیارهای اثبات مثل Lean، گلوگاه فرمال‌سازی رو برداشته
- سه آیندهٔ محتمل: AI به‌عنوان ابزار، شریک، یا اوراکل
- تائو از «ریاضیات بزرگ» می‌گه؛ اعتماد از راه راستی‌آزمایی، نه شهرت
- نگرانی اصلی: افت انگیزه، دسترسی نابرابر و آتروفی شهود نسل بعد
