چطور تری تائو مبلّغ هوش مصنوعی تو ریاضیات شد
هوش مصنوعیClaude Opus 4.8خلاصهٔ کاملتر
این مقالهٔ Quanta که از کتاب کوین هارتنت اقتباس شده، روایت میکنه که چطور تری تائو، یکی از سرشناسترین ریاضیدانهای دنیا و برندهٔ مدال فیلدز، تبدیل به بزرگترین مبلّغ استفاده از هوش مصنوعی و کامپیوتر تو ریاضیات شده. به گفتهٔ نویسنده، تائو همیشه از ایدههای غیرمتعارف نترسیده؛ همون سال ۲۰۱۴ پیشبینی کرده بود که یه روز ریاضیدانها مقالههاشون رو نه با LaTeX بلکه با زبونی مینویسن که نرمافزار هوشمند تبدیلش میکنه به زبون صوری و هر از گاهی هم خطای کامپایل میگیرن.
نکتهٔ جالب شخصیت تائو اینه که با اینکه میتونست تنها کار کنه، همکاری با بقیه رو راه اصلی کشف ایدههای جدید میدونه. همین روحیه باعث شد به پروژهٔ Polymath تیموتی گاورز بپیونده؛ یه مدل همکاری عمومی و گسترده که توش هر کسی میتونست رو یه مسئلهٔ باز کمک کنه. به گفتهٔ تائو، کلید موفقیت این بود که مسئلههایی انتخاب بشن که میشه به زیرمسئلههای سادهتر شکستشون که موازی روشون کار بشه.
ولی Polymath یه مشکل بزرگ داشت: هرچی آدمهای بیشتری مشارکت میکردن، احتمال اشتباه هم بیشتر میشد و یه نفر باید همهچیزو دستی چک میکرد؛ همین گلوگاه کل ایده رو محدود میکرد. تائو فهمید که برای واقعی شدن این رؤیا یه جور تأیید کامپیوتری لازمه که خودکار کارها رو چک کنه، نه با دست.
همین شد که تائو سراغ Lean رفت؛ نرمافزاری که اجازه میده اثباتهای ریاضی به شکل کد کامپیوتری نوشته و چک بشن. اولین تجربهاش فرمالایز کردن یه اثبات ساده دربارهٔ نامساوی Maclaurin بود. نکتهٔ آموزندهای که کشف کرد این بود که بخشهای سخت اثبات راحت تو Lean فرمالایز میشدن، ولی بخشهای بهظاهر بدیهی کلی کار میبردن؛ مثلاً باید برای اثبات اینکه جمع سه عدد بزرگتر از ۱ حداقل ۳ میشه، میرفت دنبال یه لم تو کتابخونهٔ Mathlib.
اوج این مسیر پروژهٔ فرمالایز کردن اثبات حدس PFR (فریمن-روزا چندجملهای) بود که خودش با گاورز، گرین و منرز ثابتش کرده بودن. تائو اثبات رو به لمهای پنجخطی شکست تا تا حد ممکن ماژولار بشه و خیلیا بتونن مشارکتهای کوچیک بکنن. به گفتهٔ نویسنده، این پروژه با کمک داوطلبها خیلی سریع پیش رفت و چون Lean همهچیزو تأیید میکرد، تائو دیگه لازم نبود خودش کارها رو چک کنه.
بعدش تائو پروژهٔ بزرگتری به اسم Equational Theories رو راه انداخت: بررسی رابطهٔ بین حدود ۴٬۶۹۴ قانون جبری که بینشون ۲۲ میلیون استلزام منطقی وجود داشت. داوطلبها با اسکریپتهای سادهٔ پایتون و بعدش اثباتگرهای خودکار، تو همون روزهای اول بیش از ۹۹ درصد استلزامها رو حل کردن. تائو نوشت که سرعت و مقیاس پروژه حتی از PFR هم بیشتر بوده و باورنکردنی بوده.
نویسنده میگه دیدگاه نهایی تائو اینه که هوش مصنوعی به این زودیا جای ریاضیدانها رو نمیگیره؛ اون تو آزمایشهاش دیده که مدلهای زبانی مثل دانشجوهای بیشازحد مطمئنن که بدون تخصص پیشنهاد میدن. ولی به نظرش ترکیب بینش انسانی، خلاقیت مدلهای زبانی و تضمین درستی سیستمهای تأیید صوری مثل Lean میتونه مسیر جدیدی برای ریاضیات باز کنه: هوش مصنوعی انبوه زیرمسئلههای ساده رو حل کنه و خروجیاش رو Lean چک کنه، و آدمها سراغ سختترین قسمتها برن.
نکات کلیدی:
- تری تائو، برندهٔ مدال فیلدز، به مبلّغ اصلی استفاده از هوش مصنوعی و کامپیوتر تو ریاضیات تبدیل شده
- پروژهٔ Polymath نشون داد همکاری گستردهٔ عمومی ممکنه ولی گلوگاهش چک کردن دستی خطاها بود
- ابزار Lean و کتابخونهٔ Mathlib اجازه میدن اثباتها بهشکل کد نوشته و خودکار تأیید بشن
- فرمالایز کردن اثبات حدس PFR با شکستن به لمهای پنجخطی و کمک داوطلبها خیلی سریع انجام شد
- دیدگاه تائو: ترکیب انسان، مدلهای زبانی و تأیید صوری، نه جایگزینی کامل انسان با هوش مصنوعی
