مسابقات ریاضی دانشگاه گیلان

...و اثبات در Lean بررسی شده است. سعی می‌کنم توضیح بدم که چطور باید با ادعاهایی از این دست که "این قضیه درسته، چون توی Lean اکی شده" برخورد کنیم. خلاصه حرفم اینه: اگه اثبات رو AI انجام داده، قبلش باید چند تا چیز رو چک کنیم و به طور خاص توی یه سری اثبات که OpenAI ارائه کرده این کارها انجام نشده. ۱.گزاره‌ توی Lean همون گزاره ریاضی هست؟ توی Lean یه گزاره اصلی داریم که صورت قضیه رو بیان می‌کنه و نه اثبات رو. مثلا این رو در نظر بگیرید: import Mathlib def FermatsLastTheorem : Prop := ∀ a b c n : ℕ, n ≥ 3 → a^n + b^n ≠ c^n نگاه می‌کنید و می‌گین خب، FLT هست دیگه. ولی نه! توی Lean ℕ شامل صفر هم می‌شه و این باعث می‌شه که اثبات درست ازش ارائه نشه. پس سوال اول اینه: گزاره توی Lean و گزاره توی pdf یکی هستند؟ برای یه متخصص انسانی بررسی این کار راحته و البته نه همیشه. مثلا جدیدا شرکت Axiom گفته قضیه طبقه‌بندی گروه‌های ساده متناهی رو توی Lean اکی کرده. بالای ۵۰۰۰ خط از کدها خیلی اساسی و مهم هستند و باید توسط انسان بررسی بشه تا بشه گفت تعاریف درست بیان شده. توی کدهای ارائه شده توسط OpenAI هم وضع همین هست در بعضی موارد. توی ۳۸ مورد حتی صورت گزاره اصلی بیان نشده، چه برسه به اثباتش. OpenAI گفته: اینم یه کمی کد Lean. ۲. کد اصلا کامپایل می‌شه؟ وقتی آنتروپیک FLT رو اکی کرد از من خواست بررسی‌اش کنم. دانلودش کردم و توی یه محیط Sandbox بررسی کردم (چرا؟ چون کد توسط AI تولید شده بود و باید احتیاط کرد) نتونستم اجراش کنم و به من دسترسی دادند تا بتونم اون رو اجرا کنم. ۳. کد Lean داره همون قضیه رو واقعا اثبات می‌کنه؟ از کجا بدونیم کلکی نزدند اون وسط؟ یه اصل جدید وارد نکردند که به نتیجه برسند؟ ۴. و اینکه از کجا بدونیم کد از Lean’s official kernel سوءاستفاده نمی‌کنه؟ https://xenaproject.wordpress.com/2026/11/12/and-the-proof-is-checked-in-lean/