مدل‌های هوش مصنوعی می‌توانند زبان مشترکی را به ریاضی‌دانان ارائه دهند

«مسئله انباشت کره» (Sphere-Packing Problem)، برای قرن‌ها هندسه‌دانان مشغول خود کرده بود؛ اما یک پیشرفت غیرمنتظره در سال ۱۹۹۸ همه چیز را تغییر داد. «توماس هِیلز» (Thomas Hales)، ریاضی‌دانی که در آن زمان در دانشگاه میشیگان فعالیت می‌کرد، ادعا کرد آنچه را که مدت‌ها حدس زده می‌شد، اثبات کرده است. حدسی که بیان می‌کرد «چینش شش‌ضلعی» که در آن هر کره در فرورفتگیِ ایجادشده توسط حلقه‌ای متشکل از شش کره در لایه زیرین خود قرار می‌گیرد، متراکم‌ترین پیکربندی ممکن را فراهم می‌کند.

داستان کاملاً در همین نقطه به پایان نرسید. بیش از یک دهه بررسی و بازبینیِ مکرر به طول انجامید تا همکاران ریاضی‌دان او متقاعد شوند که محاسبات هیلز در واقع درست بوده است. چنین وضعیتی چندان غیرعادی نیست. پیش از آن که یک نتیجه‌گیری ریاضی بتواند به جایگاه والای یک «اثبات» (Proof) ارتقا یابد، مراحل آن باید با زحمتی طاقت‌فرسا، نماد به نماد و گزاره به گزاره، مورد بررسی قرار گیرد. «پاتریک شفتو»  (Patrick Shafto)که در آژانس پروژه‌های پژوهشی پیشرفته دفاعی آمریکا (DARPA) مشغول به کار است می‌گوید این امر «گلوگاه اصلی در ریاضیات، یعنی مسئله اعتماد» را برجسته می‌کند.

ورود هوش مصنوعی به دنیای اثبات‌های ریاضی

«شفتو» رهبری تیمی را بر عهده دارد که امیدوارند با استفاده از هوش مصنوعی، سرعت پیشرفت در ریاضیات محض را از طریق ساده‌سازی «فرایند فرمولاسیون» (Formalisation Process) سرعت بخشند. اگر مدل‌های زبانی بزرگ پیشرفته و مسلط به ریاضیات بتوانند واقعاً اثبات‌های موجود را تأیید کرده و همچنین به توسعه اثبات‌های جدید کمک کنند، بسیاری از ریاضی‌دانان امیدوارند که این مدل‌ها بتوانند روند اکتشاف در حوزه‌ای که در حالت عادی به شکلی عذاب‌آور کند است را نیز سرعت ببخشند.

تفاوت تفکر انسان و مدل‌های زبانی

موضوعی که از همین حالا کاملاً روشن است، این است که نحوه پردازش منطق ریاضی توسط LLMها با انسان‌ها تفاوت‌هایی بنیادین دارد. انسان‌ها پیش از درگیرشدن در یک محاسبه چالش‌برانگیز، تمایل دارند حداقل طرح کلیِ یک استراتژی برای حل مسئله را تدوین کنند؛ به این معنا که اهداف خود را با نیتِ نوشتن اثبات‌هایی که در هر مرحله قابل‌پیگیری باشند، مشخص می‌کنند. در نقطه مقابل، «ترنس تائو» (Terence Tao) ریاضی‌دان UCLA معتقد است که LLMها به‌صورت یک «جریان سیال ذهنی» عمل می‌کنند؛ بنابراین چنین سیستم‌هایی مسائل را بر اساس آنچه فکر می‌کنند در گام بعدی باید ببینند حل می‌کنند، نه بر اساس مراحل دورتر در آینده. LLMها در مسیر حل مسئله پرسه می‌زنند و خروجی آن‌ها بیشتر شبیه به «گفت‌وگوهای بداهه است تا متون از پیش نوشته‌شده.»

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

ابزارهای جدید برای اثبات ریاضی

از دیدگاه «پوشمیت کوهلی» (Pushmeet Kohli)، رئیس بخش «هوش مصنوعی برای علم» در Google DeepMind، پیشرفت در این زمینه در گرو حصول اطمینان از این است که این مدل‌ها بتوانند فرایند حل مسئله خود را به‌گونه‌ای بیان کنند که برای ریاضی‌دانان قابل‌درک و پیگیری باشد.  AlphaEvolve یکی از مدل‌هایی است که او و تیمش با درنظرداشتن این هدف تولید کرده‌اند. مدل AlphaEvolve برای تولید اثبات مسائل «بهینه‌سازی» (Optimisation) طراحی شده است؛ مسائلی که هدف آن‌ها یافتن اشیای ریاضی مانند متراکم‌ترین حالت انباشت کره است که به بهترین شکل معیارهای مفروض را برآورده می‌کنند. اگرچه پیش‌تر نیز تکنیک‌هایی برای حل چنین مسائلی وجود داشت، اما تنها متخصصان قادر به استفاده از آن‌ها بودند. در مقابل، می‌توان به AlphaEvolve با استفاده از زبان طبیعی، پرامپت داد که به معنای امکان کار افراد غیرمتخصص با این ابزار است. تائو که در توسعه این ابزار مشارکت داشته است می‌گوید که هرچند گاهی اوقات پیگیری منطق و استدلال این مدل دشوار است؛ اما معتقد است که DeepThink AI، یکی دیگر از ابزارهای گوگل، قادر است نحوه کارکرد خود را به شکلی مناسب توضیح دهد.

استارتاپ‌ها و رقابت در ریاضیات هوش مصنوعی

بازیگران پرشمار دیگری نیز در این فضا حضور دارند. یکی از آن‌ها، استارتاپ آمریکایی Harmonic است. زمانی که ربات این شرکت با نام Aristotle یک اثبات را اعتبارسنجی می‌کند، تلاش می‌کند تا مراحل را دقیقاً مطابق با آنچه کاربر ارسال کرده است، دنبال کند. این ربات ابتدا اثبات را به یک زبان دقیق متشکل از نمادها و اصول موضوعه (Axiom) ترجمه می‌کند تا امکان بررسی تک‌تک مراحل فراهم شود. ارسطو از یک زبان برنامه‌نویسی متن‌باز و محبوب در میان ریاضی‌دانان به نام Lean بهره می‌برد. اگر فردی که اثبات را نوشته خطاهای کوچکی مرتکب شده باشد، Aristotle تلاش می‌کند آن‌ها را اصلاح کند. چنانچه انسان برخی از مراحل را جا انداخته باشد و ریاضی‌دانان نیز اغلب برخی مراحل اثبات شهودی را جا می‌اندازند؛ Aristotle جزئیات را تکمیل می‌کند. «تودور آکیم» (Tudor Achim)، مدیرعامل هارمونیک می‌گوید که نتیجه کار Aristotle یک اثباتِ بی‌نقص و نفوذناپذیر است که از همان اصولِ اثباتِ اولیه پیروی می‌کند. او توضیح می‌دهد که اگر یک انسان بخواهد این اثبات را درک کند، همچنان باید برای تجزیه‌وتحلیل آن کمی زحمت بکشد، «اما آن‌ها می‌دانند که تک‌تک مراحل قطعاً صحیح هستند.»

استارتاپ هوش مصنوعی .Math, Inc نیز اهداف مشابهی را دنبال می‌کند. این شرکت در حال توسعه مدلی به نام Gauss است که آن نیز می‌تواند یک اثباتِ نوشته‌شده توسط انسان را به خطوطی از کدهای زبان Lean تبدیل کند. یکی از اهداف دوگانه‌ای که این مدل دنبال می‌کرد، بررسی اثبات‌های مربوط به نسخه‌هایی با ابعاد بالاتر برای مسئله انباشت کره بود که در سال ۲۰۱۶ توسط «مارینا ویازوفسکا» (Maryna Viazovska)، ریاضی‌دان وقت دانشگاه هومبولت برلین، به دست آمده بود. مدل گاوس در عرض چند هفته توانست این اثبات‌ها را به ترتیب برای کره‌های ۸ و ۲۴ بُعدی با موفقیت فرموله کند. باوجوداینکه هر دو اثبات پیش‌ازاین بدون استفاده از هوش مصنوعی اعتبارسنجی شده بودند، اما کارکرد مدل Gauss به درک بهتر ریاضی‌دانان از ابزارهای به‌کاررفته در اثبات‌های ویازوفسکا کمک شایانی کرده است.

DARPA  و شفتو نیز امیدوارند راهی برای خودکارسازیِ فرایند ترجمه میان زبان طبیعی و زبان‌های فرمولی مانند Lean بیابند و اثبات‌های پیچیده را به گزاره‌هایی که معمولاً از آن‌ها تشکیل شده‌اند، تجزیه کنند. گردآوری آنچه شفتو در حال حاضر به‌عنوان «آشفتگی وحشتناکی از مقالات، کتاب‌های درسی و ذهنیت‌های انسانی» توصیف می‌کند در قالب یک پیکره یکپارچه، به ریاضی‌دانان جوان‌تر اجازه می‌دهد تا با سهولت بیشتری در میان منابع علمی موجود به جست‌وجو و کاوش بپردازند. این امر می‌تواند روند پیشرفت کار ریاضی‌دانان محض را تسریع کرده و موانع ورود سایر ریاضی‌دانان به این حوزه را کاهش دهد. بااین‌حال، او هشدار می‌دهد که در حال حاضر، تخصص ریاضی همچنان یک مهارت ارزشمند محسوب می‌شود و می‌گوید: «هوش مصنوعی دچار اشتباه می‌شود و ریاضی‌دان باید بتوانید تشخیص دهید این اشتباه دقیقاً در کجا رخ داده است.»

محدودیت‌های خلاقیت در هوش مصنوعی

چالش‌ها و دام‌های دیگری نیز وجود دارد. «تیموتی گاورز» (Timothy Gowers)، ریاضی‌دان دانشگاه کمبریج در حال کار بر روی «اثبات خودکار قضیه» (Automatic Theorem Proving) است؛ حوزه‌ای که در آن رایانه‌ها آموزش می‌بینند تا با تلاش برای الگوبرداری از رویکرد انسان‌ها، اثبات‌ها را بیابند. آزمایشگاه وی به‌عنوان بخشی از این پژوهش در حال بررسی این موضوع است که آیا مدل‌های هوش مصنوعی می‌توانند به‌جای اینکه صرفاً مسیرهای قدیمی را دوباره طی کنند، ارتباطات غیربدیهی میان زیرشاخه‌های ریاضیات برقرار کنند یا خیر. گاورز می‌گوید زمانی که ریاضی‌دانان در حال تفکر پیرامون رویکردهای جایگزین برای حل یک مسئله هستند، «باید به‌نوعی در اطراف موضوع جست‌وجو و کنکاش کنید؛ یک فرایند کامل وجود دارد که در طی آن تلاش می‌کنید ایده‌هایی غیراستاندارد تولید کنید.»

آینده همکاری انسان و هوش مصنوعی در ریاضیات

تا به امروز، توانایی این مدل‌ها در تقلید از خلاقیت انسانی با کاستی‌هایی همراه بوده است. به گفته گاورز یکی از این نقاط ضعف این است که LLMها در اِعمال آموخته‌های ناشی از حل یک مسئله در مواجهه با مسئله‌ای دیگر، با مشکل مواجه هستند. همچنین ریاضی‌دانان مفهومی را توسعه می‌دهند که گاورز آن را «حس زیبایی‌شناختی» (Aesthetic Sense) می‌نامد؛ حسی که آن‌ها را ترغیب می‌کند تا به دنبال اثبات‌های ظریف‌تر و شسته‌رُفته‌تری باشند که گاهی می‌توانند به نتایج شگفت‌انگیزی منجر شوند. به نظر می‌رسد تقلید از این ترکیب حس زیبایی‌شناختی و دانش عمیق، برای مدل‌های هوش مصنوعی بسیار دشوار باشد. حداقل در این جبهه خاص، «انسان‌ها همچنان برتری دارند.»

ربات‌ها همچنین می‌توانند به روش‌های شگفت‌انگیزی رفتارهای ناهنجار و دور از انتظار از خود نشان دهند. در ماه مارس ۲۰۲۶، «دونالد کنوت» (Donald Knuth)، ریاضی‌دان دانشگاه استنفورد به همراه همکارش «فیلیپ استاپرز» (Filip Stappers) در حال کار بر روی مسئله‌ای مشابه «مسئله فروشنده دوره‌گرد» (Travelling Salesman Problem) بودند؛ مسئله‌ای که در آن باید کوتاه‌ترین مسیر برای یک فروشنده پیدا شود تا پیش از بازگشت به مبدأ، از چندین شهر دقیقاً یک بار بازدید کند. آن‌ها برای کمک به پیشبرد کار، به سراغ Claude Opus 4.6 رفتند.

پس از استفاده از چندین رویکرد متفاوت، Claude  توانست مسئله را برای مواردی حل کند که در هر توقفگاه، تعدادی فرد از مسیرها برای انتخاب باقی می‌ماند. اما زمانی که مدل برای حل مسئله در تمامی اعداد زوج تحت‌فشار قرار گرفت، دچار اختلال در عملکرد شد. استاپرز با اشاره به کدهایی که مدل برای بیان استدلال خود استفاده می‌کرد، نوشت: «در نهایت، مدل حتی قادر به نوشتن و اجرای صحیح برنامه‌های کاوشگر (Explore Programs) نیز نبود و بسیار عجیب است.» اما بااین‌وجود، کنوت نوشت که نحوه برخورد Claude  با این مسئله، او را تحت‌تأثیر قرار داده است. چند هفته بعد، پژوهشگر دیگری با استفاده از ChatGPT 5.4 Pro این کار را بسط داد تا مسئله را برای اعداد زوج نیز حل کند.

چنانچه بتوان بر این دشواری‌ها غلبه کرد، دستاوردهای فراوانی در افق پیش رو وجود خواهد داشت. از نظر تئوری، یک مدل هوش مصنوعی که قادر به حفظ و درکِ پیکره دانش ریاضی باشد، می‌تواند ارتباطات جدیدی را کشف کند که مدت‌ها از دید پژوهشگران پنهان مانده است. همچنین، مدلی که بتواند ریاضیات را استدلال کند، می‌تواند آموزش ببیند تا درباره سایر حوزه‌های کَمّی، از اقتصاد گرفته تا فیزیک نیز استدلال کند. کوهلی می‌گوید با در اختیار داشتن چنین توانایی‌های عظیمی در حل مسئله، چالش واقعی برای انسان‌ها یافتن مجموعه بعدی از مسائلی خواهد بود که ارزشِ پردازش و حل‌کردن را داشته باشند.

گزارش حاضر در نسخه April 11^th 2026 نشریه The Economist منتشر شده است.