به نظر می‌رسد هوش مصنوعی هر هفته از پس یک مسئله ریاضی تازه برمی‌آید. فقط ماه گذشته، OpenAI به‌تنهایی ۷۱۹ دست‌نوشته منتشر کرد که مدعی ارائه راه‌حل‌هایی برای برخی از دشوارترین مسائل این حوزه بودند. حتی بررسی‌های رایانه‌ای هم ممکن است خطا داشته باشند. پس از سال‌ها محتوای بی‌کیفیت تولیدشده با هوش مصنوعی، جای سؤال است که آیا نوبت ریاضی هم رسیده است یا نه.

AxiomMath شرط بسته که ریاضی می‌تواند از این سرنوشت در امان بماند؛ نه با کندکردن روند، بلکه با بناکردن آن بر پایه‌ای محکم‌تر. این استارتاپ ۱.۶ میلیارد دلاری می‌خواهد بنیانی تأییدشده بسازد که عامل‌های هوش مصنوعی بتوانند برای نوشتن نرم‌افزار و در نهایت انجام پژوهش‌های علمی به آن اتکا کنند.

این شرکت روز چهارشنبه اعلام کرد که پروژه Stacks را به‌طور رسمی راستی‌آزمایی کرده است؛ یکی از بزرگ‌ترین مجموعه‌های ریاضی که تاکنون به‌دست انسان نوشته شده است. ریاضی‌دانان اغلب جایگاهی کم‌نظیر برای Stacks قائل‌اند. Peter Woit، ریاضی‌دان دانشگاه Columbia، گفته است که «واقعاً هیچ چیز دیگری با آن قابل‌مقایسه نیست» و این پروژه را با «کتاب‌های مشهور Bourbaki» مقایسه کرده است؛ مجموعه‌ای که در قرن بیستم ریاضی را از پایه بازسازی کرد.

Johan de Jong، همکار Woit در دانشگاه Columbia، پروژه Stacks را در سال ۲۰۰۵ به‌عنوان مرجعی متن‌باز راه‌اندازی کرد. از آن زمان، ریاضی‌دانان در گسترش آن مشارکت کرده‌اند و نتایجی را از جبر در سطح دانشگاهی تا پیشرفته‌ترین ایده‌های حوزه‌های جبر، هندسه و نظریه اعداد به آن افزوده‌اند.

مجموعه عامل‌های هوش مصنوعی این شرکت، حدود ۷۶۵۴ صفحه از این کتابخانه را به حدود ۱۶ میلیون خط کدی تبدیل می‌کند که با رایانه بررسی شده‌اند.

صورت‌بندی صوری ریاضی راهی برای اطمینان از درستی ساختار زیربنایی آن است. ریاضی‌دانان برهان را با زبان برنامه‌نویسی‌ای به نام Lean به کد تبدیل می‌کنند و برنامه‌ای به نام دستیار اثبات، کد را خط‌به‌خط بررسی می‌کند. اگر برهان از این بررسی سربلند بیرون بیاید، ریاضی‌دانان می‌توانند از درستی منطقی آن اطمینان داشته باشند.

مهندسان نیز از همین ایده که «راستی‌آزمایی صوری» نام دارد، برای تأیید عملکرد درست طراحی تراشه‌هایشان استفاده می‌کنند. پژوهشگران فرانسوی هم از این روش برای پیداکردن باگ‌ها در نرم‌افزاری استفاده کرده‌اند که مزایای خانوادگی را محاسبه می‌کند.

در کتابخانه‌ای مانند پروژه Stacks، بررسی تک‌تک قضیه‌ها تنها بخشی از کار است. قضیه‌ها و تعریف‌های Stacks به هم پیوسته‌اند و هرکدام بر موارد پیش از خود بنا می‌شوند. مانند شجره‌نامه، بسیاری از نتایج Stacks به نتایج پیشین خود بازمی‌گردند.

همین پیوستگی باعث شد Axiom در ابتدا درباره عملی‌شدن این پروژه تردید داشته باشد. تیم باید همه این پیوندها را در حدود ۱۶ میلیون خط کد Lean دست‌نخورده نگه می‌داشت.

Carina Hong، مدیرعامل Axiom، به TechCrunch گفت: «چیزهای بزرگ و چیزهای ظریف در زندگی معمولاً با هم جور درنمی‌آیند. [Stacks] مجموعه‌ای از نتایج ریاضی است که بنیان ریاضی را تشکیل می‌دهد. می‌خواهید [قضیه‌ها] با هم سازگار باشند و مثلاً به تناقض نرسند. می‌خواهید تعریف‌ها با هم تعارض نداشته باشند.»

این مدیرعامل ۲۵ساله تحصیل در دوره دکتری ریاضی دانشگاه Stanford را نیمه‌کاره رها کرد و در مارس ۲۰۲۵ این شرکت را بنیان گذاشت. Axiom در مارس، دور سرمایه‌گذاری سری A به ارزش ۲۰۰ میلیون دلار را به رهبری Menlo Ventures جذب کرد.

Hong گفت: «مطمئن نبودیم vibe coding بتواند زیبایی Stacks را حفظ کند.»

برای پیشبرد پروژه، تیم چارچوبی کلی در اختیار عامل‌هایش گذاشت و اجازه داد موازی کار کنند. Ashvin Swaminathan، از اعضای تیم فنی Axiom، گفت: «در مورد Stacks، سلسله‌مراتبی تعیین کردیم… [اما] این‌طور نبود که سلسله‌مراتبی کامل وضع کنیم و مشخص کنیم هر عامل دقیقاً چه کاری انجام دهد. عامل‌ها خودشان کارهایی را پیدا می‌کردند و تشخیص می‌دادند چه چیزهایی را می‌توانند به‌طور موازی انجام دهند.»

Axiom همچنین مدل‌های اختصاصی خود را برای عملکرد بهتر در ریاضی آموزش داد؛ رویکردی که به‌گفته Hong، بیشتر استارتاپ‌های دیگرِ فعال در حوزه راستی‌آزمایی در پیش نگرفته‌اند. در ابتدا، تیم از یکی از متخصصان داخلی Lean کمک گرفت تا حس تشخیص و سلیقه انسانی را به عامل‌ها بیاموزد. Hong گفت عامل‌ها به‌مرور خودشان این سلیقه را پیدا کرده‌اند.

نتیجه این کار یکی از بزرگ‌ترین خلأهای ریاضی صورت‌بندی‌شده را پر می‌کند. Swaminathan گفت: «وقتی به چیزهایی که در ریاضی صورت‌بندی شده‌اند نگاه می‌کنید، با سیاه‌چاله‌ای عظیم روبه‌رو می‌شوید؛ سیاه‌چاله‌ای که هندسه جبری را دربرمی‌گیرد.»

Swaminathan گفت تا پیش از این، پژوهشگرانی که می‌خواستند پژوهش‌های جدید در هندسه جبری را با Lean بررسی کنند، مبنای چندانی برای کار نداشتند. «خب، حالا دارند.»

Axiom می‌گوید هر نتیجه تأییدشده به یک بلوک سازنده تبدیل می‌شود و در نتیجه، برهان‌های آینده می‌توانند به ریاضیِ بررسی‌شده تکیه کنند، نه اینکه همه‌چیز را از صفر آغاز کنند. Terence Tao، ریاضی‌دان دانشگاه UCLA و برنده مدال فیلدز، اصل کلی این ایده را ساده‌تر بیان کرده است: «هرچه برهان‌های صورت‌بندی‌شده بیشتری داشته باشید، می‌توانید برهان‌های صورت‌بندی‌شده بیشتری بسازید.»

ریاضی‌دانان تنها مخاطبان موردنظر Axiom نیستند. توسعه‌دهندگان مدت‌هاست برای تضمین عاری‌بودن کدهایشان از باگ و حفره‌های امنیتی با دشواری روبه‌رو هستند. با نوشتن بخش بیشتری از کدهای جهان به‌دست عامل‌های هوش مصنوعی، این مشکل نیز بزرگ‌تر می‌شود.

Axiom شرط بسته که نرم‌افزارهای آینده، درست مانند Stacks در حال حاضر، باید بر پایه‌هایی تأییدشده بنا شوند.

Swaminathan گفت: «باور داریم ریاضی حوزه‌ای است که باید ساخت چنین چیزهایی را از آن آغاز کرد و این مهارتی انتقال‌پذیر است. عامل‌ها می‌توانند کد ما را بخوانند، درک کنند و زیرساخت‌های تازه‌ای بر پایه آن بسازند. صورت‌بندی Lean ما اکنون بستری است که عامل‌ها می‌توانند بر آن بنا کنند.»

Hong انتظار دارد بخش بزرگی از کارهای آینده هوش مصنوعی به همان شیوه‌ای انجام شود که عامل‌های Axiom پروژه Stacks را ساختند: با کار موازی و انتخاب وظایف به‌دست خودشان. به‌گفته او، عامل‌های هوش مصنوعی برای پرهیز از تولید محتوای بی‌کیفیت به بدنه‌ای از دانش نیاز دارند که به‌خوبی ساخته شده و بتوان بارها از آن استفاده کرد.

Hong گفت: «می‌خواهید [عامل‌ها] کتابخانه‌ای داشته باشند که بتوانند بارها از آن استفاده کنند، بر پایه‌اش بسازند و مرزهای دانش را گسترش دهند. اگر از همان ابتدا با مهندسی ضعیف، کار بی‌کیفیتی تحویل دهید، گسترش آن مرز برایشان بسیار دشوار می‌شود.»

Hong آن‌قدر به این رویکرد اطمینان دارد که دیگران را به چالش می‌کشد: «صریحاً همه شرکت‌های فعال در حوزه کدنویسی را به کار روی صورت‌بندی در این مقیاس دعوت به چالش می‌کنم.»