‏آیا هوش مصنوعی ریاضیات دانشگاهی رو کشته؟

نویسنده‌ای با نام doomslide تو این مقاله، در جواب یادداشت Daniel Litt دربارهٔ آیندهٔ ریاضیات، می‌گه مسئلهٔ اصلی توانایی AI نیست. به نظر اون ریاضیات محض اساساً یه discourse (یعنی گفت‌وگوی جمعی بین ریاضی‌دان‌ها) هست. هم استانداردهای کیفیت از همین گفت‌وگو میاد، هم اعتبار دادن به کسی که یه ایده رو داده، که بخش مهمی از دستمزد ریاضی‌دان‌هاست.

نویسنده کار AI رو دو بخش می‌بینه: جست‌وجو تو مقاله‌ها و جست‌وجوی اثبات با کمک ابزارهای بررسی مثل Lean (یه زبان برای نوشتن اثبات‌هایی که کامپیوتر درستی‌شون رو چک می‌کنه). به گفتهٔ اون، نتیجه‌هایی که به این بررسی‌کننده‌ها تکیه دارن خیلی بیشتر پیشرفت کردن. ولی هنوز شاهد ساختن مفاهیم انتزاعی جدید بدون کمک آدم نیستیم و این توانایی احتمالاً آهسته بهتر می‌شه.

نکتهٔ اصلی مقاله اینه که شرکت‌های AI داده‌های کاربرها رو برای بهتر کردن مدل‌ها به کار می‌برن. یعنی ورودی یه کاربر می‌تونه روی خروجی کاربر دیگه اثر بذاره، بدون هیچ ردپایی. نویسنده یه سناریو می‌گه: گروه A ماه‌ها با AI روی یه مسئله کار می‌کنه، مدل از گفت‌وگوهاشون یاد می‌گیره و گروه B با مدل جدید همون مسئله رو زودتر حل و منتشر می‌کنه، بی‌خبر از این‌که عملاً ایدهٔ یکی دیگه رو برداشته.

به گفتهٔ مقاله، این سناریو شاید قبلاً اتفاق افتاده باشه. دعوای Alpöge و Buckmaster با OpenAI سر مسئلهٔ Navier-Stokes یه نمونه‌ست. OpenAI با ده‌ها میلیون دلار محاسبه یه مثال نقض پیدا کرد و طرف مقابل ادعا کرد ایده‌ها از چت‌های Codex دزدیده شده. نویسنده دربارهٔ کرهٔ شش‌بعدی مختلط هم مشکوکه که یه اثبات ۱۰۰ صفحه‌ای در واقع ترجمهٔ یه اثبات Lean اعلام‌نشده بوده. اسم این کار رو «پول‌شویی اثبات» می‌ذاره.

بحث مسئولیت هم مطرحه. نویسنده می‌گه مدل نمی‌تونه ضامن درستی اثبات باشه یا ماه بعد یه خلأ رو پر کنه، پس نمی‌تونه نویسنده حساب بشه. کسی که اثبات رو منتشر می‌کنه باید بگه دقیقاً به چه دلیلی بهش اعتماد داره. اگه دلیلش یه اثبات Lean یا یه ابزار داخلیه، همون بخشی از اثباته و باید منتشر بشه.

راه‌حل فنی به نظر نویسنده وجود داره: مدل‌های open-weight محلی، یا سرویس‌هایی با تعهد واقعی ZDR (یعنی نگه نداشتن هیچ داده‌ای از کاربر). اما به قانون و قاعدهٔ دانشگاهی هم نیازه تا استفاده از دادهٔ خصوصی برای آموزش ممنوع بشه. نویسنده انتظار نداره چنین تغییری اتفاق بیفته و نتیجه می‌گیره ریاضیات دانشگاهی عملاً مرده.

نکات کلیدی:

• ادعای اصلی: مشکل AI برای ریاضیات از بین رفتن ردپای ایده‌هاست، نه توانایی حل مسئله.
• استفادهٔ شرکت‌ها از داده‌های کاربر یعنی ایدهٔ یه گروه ممکنه بی‌صدا به گروه دیگه برسه.
• به نظر نویسنده مدل نمی‌تونه نویسندهٔ اثبات باشه چون نمی‌تونه ضامن درستیش بشه.
• اگه اثبات به Lean تکیه داره، کد Lean خودش بخشی از اثباته و باید منتشر بشه.
• راه‌حل پیشنهادی: مدل‌های محلی، سرویس‌های ZDR و ممنوعیت آموزش روی دادهٔ خصوصی کاربر.