Axiom Math پروژه Stacks را به‌صورت رسمی تأیید کرد

به گزارش TechCrunch، استارتاپ Axiom Math اعلام کرد پروژه Stacks را به‌صورت رسمی تأیید کرده است. این پروژه یکی از بزرگ‌ترین مجموعه‌های ریاضیاتی است که تاکنون توسط انسان‌ها نوشته شده است. شرکت می‌گوید این کار گامی برای ساختن بنیانی قابل اعتماد است تا عامل‌های هوش مصنوعی بتوانند روی آن نرم‌افزار بنویسند و در نهایت به کار علمی بپردازند.

جزئیات

Axiom Math می‌گوید عامل‌های هوش مصنوعی آن کتابخانه‌ای با حدود ۷۶۵۴ صفحه را به حدود ۱۶ میلیون خط کد رایانه‌ای تأییدشده تبدیل کرده‌اند. این کد در زبان برنامه‌نویسی Lean نوشته می‌شود و یک برنامه کمکی به نام proof assistant آن را خط به خط بررسی می‌کند. اگر اثبات از این بررسی عبور کند، ریاضی‌دانان می‌توانند به درستی منطقی آن اعتماد کنند.

تأیید رسمی ریاضیات به این معناست که ساختار زیرین اثبات‌ها سالم باشد. در پروژه Stacks، قضیه‌ها و تعاریف به‌هم پیوسته‌اند و هر کدام بر پایه نتایج قبلی ساخته می‌شوند. تیم Axiom می‌گوید در ابتدا مطمئن نبود این پروژه کار کند، چون باید همه پیوندها در حدود ۱۶ میلیون خط کد Lean حفظ می‌شد. کارینا هنگ، بنیان‌گذار و مدیرعامل ۲۵ ساله شرکت، به TechCrunch گفت: «Things that are big and things that are delicate in life just don’t go together.»

هنگ از برنامه دکترای ریاضیات دانشگاه استنفورد خارج شد و شرکت را در مارس ۲۰۲۵ تأسیس کرد. در همان ماه، Axiom یک دور سرمایه‌گذاری سری A به ارزش ۲۰۰ میلیون دلار جذب کرد که Menlo Ventures آن را رهبری کرد. او گفت تیم در ابتدا مطمئن نبود «vibe coding» بتواند زیبایی پروژه Stacks را حفظ کند.

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

پیشینه

پروژه Stacks را یوهان دی یونگ، همکار پیتر وویت در دانشگاه کلمبیا، در سال ۲۰۰۵ به‌عنوان یک مرجع متن‌باز آغاز کرد. از آن زمان، ریاضی‌دانان به آن کمک کرده‌اند و نتایج را از جبر سطح دانشگاه تا پیشرفته‌ترین ایده‌های جبر، هندسه و نظریه اعداد گسترش داده‌اند. پیتر وویت، ریاضی‌دان دانشگاه کلمبیا، گفته است چیز دیگری واقعاً قابل مقایسه با آن نیست و آن را با کتاب‌های معروف بورباکی مقایسه کرده است.

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

چه معنایی دارد

Axiom استدلال می‌کند هر نتیجه تأییدشده به یک بلوک ساختمانی تبدیل می‌شود، بنابراین اثبات‌های آینده می‌توانند روی ریاضیات تأییدشده تکیه کنند، نه اینکه از صفر شروع کنند. ترنس تائو، ریاضی‌دان دانشگاه UCLA و برنده مدال فیلدز، این ایده را ساده‌تر بیان کرده است: هر چه اثبات‌های تأییدشده بیشتر باشد، اثبات‌های تأییدشده بیشتری می‌توان ساخت.