‏MathCode: دستیار ترمینالی که ریاضی رو ثابت می‌کنه

مسئله رو به زبون معمولی تو ترمینال می‌نویسی و MathCode خودش اونو به یه قضیهٔ Lean 4 ترجمه می‌کنه و می‌ره سراغ اثبات رسمی. تو صفحهٔ پروژه اومده که این ابزار یه دستیار کدنویسی ترمینالیه با موتور فرمال‌سازی ریاضی داخلش — یعنی به‌جای اینکه فقط یه متن جواب بده، خروجی‌ش کدیه که کامپایلر Lean درستی‌شو تأیید می‌کنه. خروجی‌ها هم تو پوشهٔ LeanFormalizations/ ذخیره می‌شن.

چیزی که تیم Math-AI بیشتر از همه روش تأکید می‌کنه سرعته: یه Lean REPL دائمی — یعنی یه language server که یک بار بالا میاد و باز می‌مونه — زمان هر چک کامپایل رو بعد از یه warmup اولیه به حدود ۰.۴ ثانیه می‌رسونه، جای حدود ۳۰ ثانیه‌ای که حالت معمولی می‌گیره. یعنی حلقهٔ «کد بنویس، خطا بخون، دوباره امتحان کن» انقدر سریع می‌شه که agent می‌تونه ده‌ها بار تکرارش کنه.

دو تا کتابخونهٔ ماندگار هم داره: کتابخونهٔ قضیه‌ها که هر اثبات موفق رو خودکار اسم‌گذاری و ذخیره می‌کنه تا بعداً بشه import‌ش کرد، و کتابخونهٔ axiom که فرض‌های خود کاربر رو به‌شکل تعریف Lean کامپایل‌شده و از نظر سازگاری بررسی‌شده نگه می‌داره. برای پیدا کردن لم‌های آمادهٔ Mathlib هم leansearch.net و Loogle رو می‌گرده و از تشخیص‌های ساختاریافتهٔ LSP برای تعمیر خطاها استفاده می‌کنه.

روش اثباتش agentic هست: هر اثبات یه نشست تعاملیه که مدل توش کاندیدا می‌نویسه، خطای کامپایلر رو می‌خونه و دوباره کامپایل می‌کنه. برای قضیه‌های سنگین‌تر، Tree-of-Subgoals قضیه رو به زیرهدف‌های مستقل می‌شکنه، موازی ثابتشون می‌کنه و آخرش به هم می‌دوزه؛ چند planner هم هم‌زمان اجرا می‌شن تا استراتژی‌های متنوع بدن و prover بهترین‌شو برداره. یه Obsidian vault هم می‌سازه که وابستگی قضیه‌ها به لم‌ها رو مثل یه گراف دانش نشون می‌ده.

برای اجرا فعلاً macOS روی arm64 یا لینوکس x86_64 لازمه و بک‌اند پیش‌فرضش به CLI ابزار codex وصله؛ یه رابط تحت وب هم داره. تیم می‌گه خط لولهٔ فرمال‌سازی و اثباتش روی پروژهٔ AUTOLEAN بنا شده.

نکات کلیدی:

• Lean REPL دائمی زمان هر چک کامپایل رو از حدود ۳۰ ثانیه به حدود ۰.۴ ثانیه می‌رسونه.
• هر قضیهٔ ثابت‌شده خودکار اسم می‌گیره و تو کتابخونه ذخیره می‌شه تا دوباره import بشه.
• Tree-of-Subgoals قضیه رو به زیرهدف‌های مستقل می‌شکنه و موازی ثابت می‌کنه.
• برای پیدا کردن لم‌های Mathlib از leansearch.net و Loogle استفاده می‌کنه.
• فقط روی macOS arm64 و لینوکس x86_64 اجرا می‌شه و بک‌اند پیش‌فرضش codex CLI هست.