🚀 Math, Inc.
معرفی کرد: Gauss — عامل خودکار برای فرمال‌سازی ریاضیات

❌شرکت Math, Inc. امروز از عامل هوش مصنوعی جدید خود با نام Gauss رونمایی کرد؛ ابزاری که توانسته است در حدود ۳ هفته فرمال‌سازی کامل قضیه اعداد اول قوی (Strong Prime Number Theorem – PNT) را در زبان رسمی Lean به انجام برساند.

🔹 این چالش نخستین بار در ژانویه ۲۰۲۴ توسط Terence Tao و Alex Kontorovich مطرح شد.

🔹 در ژوئیه ۲۰۲۵، آنها پیشرفت‌هایی در نسخه میانی (Medium PNT) گزارش کردند، اما در بخش‌های مربوط به آنالیز مختلط متوقف ماندند — جایی که Gauss موفق شد آن موانع را برطرف کند.

📂 خروجی پروژه شامل:

✳️حدود ۲۵ هزار خط کد Lean
✳️بیش از ۱۱۰۰ تعریف و قضیه
✳️یک blueprint در LaTeX و مستندات رندر شده

✅همچنین README پروژه تأکید دارد که «بیشتر گزاره‌ها و اثبات‌ها توسط Gauss تولید شده‌اند»، در حالی که بخش‌هایی با کمک هدفمند انسانی ساختاربندی یا بازنویسی شده‌اند.


💡 پروژه از کدهای قبلی PrimeNumberTheoremAnd نیز بهره گرفته است.

🔧 حامی مالی و شریک اصلی: برنامه DARPA expMath

🔗 وبلاگ معرفی
🔗 مخزن GitHub
🔗 دسترسی زودهنگام

#هوش_مصنوعی #ریاضیات #Lean #فرمال‌سازی #PrimeNumberTheorem #DARPA #Gauss