آنچه ریاضیدانان باید در مورد اثبات قضیه ناب بدانند: قابلیت اطمینان و هوش مصنوعی

9 اکتبر 2026 در math.GM , نظر | برچسب ها: هوش مصنوعی , ناب , توماس هیلز | توسط ترنس تائو

[این یک پست مهمان توسط توماس هیلز است. این پست وبلاگ در ابتدا با فرمت فایل متفاوتی نوشته شد و با استفاده از هوش مصنوعی تبدیل شد. - تی.]

ریاضیدانان در مورد ارزشی که در مورد ریاضیات دارند، سنجیده اند. برای من چیزی که اهمیت دارد ثبات ریاضی و اعتبار بی نظیر آن در حمایت از علم و تمدن است.

برهان صوری یک برهان ریاضی است که به طور کامل در سطح مبانی ریاضی و قواعد اساسی منطق بررسی شده است. در تئوری، این ممکن است با دست انجام شود، اما به دلیل تعداد مراحل درگیر، این کار به طور کلی توسط کامپیوتر و با استفاده از نرم افزار طراحی شده برای این کار انجام می شود.

نمونه هایی از قضایا که رسمیت یافته اند عبارتند از قضیه چهار رنگ، قضیه فیت تامپسون (ترتیب فرد)، حدس کپلر، واژگونی کره، مسئله بسته بندی کره در ابعاد 8 و 24، انفجار اجباری ناویر استوکس و آخرین قضیه فرما. سه پروژه آخر رسمی سازی در سال جاری تکمیل شده و آگاهی گسترده ای را از پتانسیل رسمی سازی به ارمغان آورده است.

سیستم‌های نرم‌افزاری برای رسمی‌سازی به‌طور متفاوتی به نام‌های دستیار اثبات، اثبات‌کننده قضیه، یا اثبات‌کننده قضیه تعاملی نامیده می‌شوند. برای هدف این پست، این اصطلاحات به جای هم استفاده می شوند. دستیارهای اثبات بسیاری در طول سال ها توسعه یافته اند: Automath، HOL Light، Isabelle، Coq (سال گذشته به Rocq تغییر نام داد)، Metamath، Mizar و Lean. Freek Wiedijk کتابی با عنوان "هفده اثبات کننده جهان" را ویرایش کرد که برخی از این دستیاران اثبات را با هم مقایسه می کند و دلیلی بر غیرمنطقی بودن جذر 2 در هر یک از آنها ارائه می دهد.

در بین ریاضیدانان، اثبات قضیه ناب محبوب ترین است، و این پست بر روی ناب تمرکز خواهد کرد.

Lean توسط Leo de Moura در سال 2013، زمانی که در مایکروسافت بود، توسعه و معرفی شد. به نفع ما، دی مورا مایکروسافت را متقاعد کرد که این نرم افزار را منبع باز بسازد. کتاب کوین هارتنت در مورد تاریخچه Lean، "اثبات در کد"، بیان می کند که جرمی آویگاد (مدیر موسسه جدید NSF کارنگی ملون ICARM) اولین کاربر Lean بود. او سمیناری Lean را در سال 2015 برگزار کرد که من در آن شرکت کردم. در سال 2017، یکی از دانشجویان فارغ التحصیل جرمی، ماریو کارنیرو، که با یوهانس هولزل کار می‌کرد، بخش‌های موجود از کتابخانه اصلی Lean را برداشت و یک کتابخانه ریاضی ناب جداگانه به نام mathlib راه‌اندازی کرد.

این کتابخانه از ریاضیات رسمی در حال حاضر عظیم است و شامل نزدیک به 300000 قضیه، بیش از 100000 تعریف، 2.5 میلیون خط کد، با بیش از 700 مشارکت کننده است. از هر تعریف یا قضیه ای در mathlib می توان برای اثبات قضایای بیشتر استفاده کرد. به عنوان مثال، اگر اثباتی از نابرابری کوشی- شوارتز استفاده کند، نتیجه را می توان از کتابخانه استناد کرد نه اینکه آن را محکوم کند.

در گذشته، محققان مجبور بودند با کار انسانی، اثبات های کاغذی را به اثبات های رسمی تبدیل کنند. برای مثال، اثبات رسمی حدس کپلر بر روی بسته‌بندی‌های کره‌ای در سه بعدی، حدود 20 سال کار انسانی طول کشید تا تکمیل شود و شامل حدود 500000 خط اسکریپت اثبات است. برای سال‌ها، برای بسیاری از ما که در زمینه رسمی‌سازی کار می‌کنیم، یک رویا بوده است که راه‌هایی برای افزایش اتوماسیون به فرآیند بیابیم. Autoformalization تحقق این رویا است. Autoformalization رسمی کردن ریاضیات توسط هوش مصنوعی است.

هوش مصنوعی مقاله را می خواند (مثلا یک فایل pdf یا متنی) و اثبات رسمی را در Lean یا برخی از دستیارهای اثبات دیگر خروجی می دهد.

رسمی سازی خودکار در سال 2026 به یک واقعیت عملی تبدیل شده است. از اواخر بهار و تابستان سال 2025، محققان به طور فزاینده ای نسبت به خودکارسازی خوش بین بودند. در اینجا برخی از نقاط عطف وجود دارد.

سپتامبر 2025، Math Inc. یک شبه خودکارسازی قضیه اعداد اول را تولید کرد. این فرآیند صرفا «شبه» بود، زیرا هر زمان که هوش مصنوعی گیر می‌کرد، انسان‌ها باید برای ارائه راهنمایی‌های بیشتر مداخله می‌کردند. ژانویه 2026، J. Urban پیش‌چاپ arXiv «130 هزار خط توپولوژی رسمی در دو هفته» را ارسال کرد که به صورت خودکار بخش‌های بزرگی از کتاب درسی توپولوژی Munkres را در یک دستیار اثبات بر اساس تئوری مجموعه‌ها، رسمی کرد. Mar 2026. تقریبا یک هفته پس از اعلام رسمی سازی کامل در 8 بعدی، Math Inc.

به دنبال اثبات ویازوفسکا و همکارانش، به صورت خودکار مشکل بسته بندی کره در 24 بعد را اعلام کرد. این پروژه حدود 500 هزار SLOC (خطوط کد منبع) تولید کرد که گلف (یا هرس کد) بعدا به حدود 200 هزار خط کاهش یافت. می 2026، گروهی در Meta/Facebook Research بخش بزرگی از 26 کتاب درسی ریاضی را در پروژه ای به نام ATLAS به صورت خودکار رسمی کردند.

از آنجا، قضایای متعددی به صورت خودکار رسمیت یافته اند. به ویژه قابل توجه، رسمی سازی خودکار آخرین قضیه فرما است که توسط Anthropic در 4 سپتامبر اعلام شد. این پروژه 13 میلیون خط ناب را در 11 روز تولید کرد. اعلام انفجار Navier-Stokes با اجبار در 8 سپتامبر توسط OpenAI با رسمی سازی خودکار قضیه در Lean همراه بود.

اوربان در ژانویه اظهار داشت: «ما معتقدیم که رسمی‌سازی (خودکار) ممکن است در سال 2026 بسیار آسان و فراگیر شود، صرف نظر از اینکه از کدام دستیار اثبات استفاده می‌شود.» پروژه‌های رسمی‌سازی خودکار در دستیارهای اثباتی مختلف با استفاده از LLM‌های مختلف تکمیل شده‌اند، اما ما روی Lean تمرکز می‌کنیم. «برای [جسی] هان، این نشان‌دهنده حتی بیشتر است: آغاز یک تحول انقلابی در ریاضیات، جایی که رسمی‌سازی‌های بسیار بزرگ در مقیاس معمولی رایج است» (IEEE Spectrum).

جارد لیختمن راه اندازی MAP (پروژه رسمی سازی خودکار ریاضیات) را در 8 سپتامبر 2026 اعلام کرد که هدف آن ترجمه "همه ریاضیات شناخته شده به کد رسمی" است. او از ما می خواهد که یک تریلیون خط کد بعدی را تصور کنیم.

ناب بر اساس نظریه نوع است. در واقع، گویش خاصی از نظریه نوع به نام CIC، حساب ساختارهای استقرایی. این پست برای آموزش تئوری نوع نیست و مختصر خواهم بود. پارادوکس معروف راسل در سال 1901 (مجموعه همه مجموعه هایی که عنصری از خودشان نیستند...) به بحرانی در پایه های ریاضی منجر شد. دو راه حل در اواخر آن دهه پیشنهاد شد. (1) بدیهیات زرملو در نظریه مجموعه ها که ایجاد مجموعه های ناامن را ممنوع می کند. (2) نوع نظریه که آن را به یک خطای نحوی برای ایجاد موجودیت های پارادوکس مانند راسل تبدیل می کند.

نظریه تیپ توسط خود راسل در سال 1903 در کتاب اصول ریاضیات معرفی شد و بخشی از سیستم بنیادی اصول راسل و وایتهد شد.

برای ریاضیدانانی که به نظریه مجموعه‌ها عادت دارند، مقاله ب. ورنر (1997) «مجموعه‌ها در انواع، انواع در مجموعه‌ها» اطمینان خاطر می‌دهد که هر کاری که در نظریه مجموعه‌ها انجام داده‌اند، می‌تواند به نظریه نوع ترجمه شود، و هر کاری که در نظریه تیپ انجام شود می‌تواند دوباره به نظریه مجموعه‌ها ترجمه شود. به‌طور دقیق‌تر، این مقاله نشان می‌دهد که نظریه مجموعه‌های ZFC را می‌توان در CIC رمزگذاری کرد، و یک گویش خاص از CIC را می‌توان به ZFC (با سلسله مراتبی از کاردینال‌های غیرقابل دسترسی) رمزگذاری کرد.

در خطر ساده‌سازی مسائل تا حدی مضحک، ممکن است بگوییم که «انواع مانند مجموعه‌های مجزا هستند». هر عنصر در تئوری نوع "عنصر" دقیقا یک نوع است. نوع عدد طبیعی 2 نوع عدد طبیعی است. نوع e، پایه لگاریتم طبیعی، نوع عدد واقعی است و غیره. نوع اعداد طبیعی از نوع اعداد حقیقی جدا است و یک اجبار صریح (ارسال 2 به 2.0) از نوع اعداد طبیعی به نوع اعداد حقیقی ساخته می شود.

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

یکی از بخش های سیستم Lean یک زبان برنامه نویسی همه منظوره است (که به طور مناسب زبان برنامه نویسی ناب نامیده می شود). برنامه های کامپیوتری معمولی، مانند برنامه ای برای مرتب سازی لیست، می توانند به این زبان نوشته شوند، سپس کامپایل و اجرا شوند. سیستم ناب همچنین یک زبان ریاضی را ارائه می دهد که در آن می توان تعاریف را نوشت، قضایا را بیان کرد و اسکریپت های اثباتی را نوشت. زبان برنامه نویسی و زبان ریاضی موجودیت های مستقلی نیستند. بلکه یک زبان واحد است که هر دو را انجام می دهد.

کد برنامه را می توان با قضایای مربوط به درستی الگوریتم ها مخلوط کرد. اثبات های ریاضی را می توان با استفاده از برنامه ها تولید کرد. اسکریپت‌های اثبات در Lean تجزیه می‌شوند و فرآیندی به نام elaboration (نوعی فرآیند جمع‌آوری برای ریاضیات) را طی می‌کنند، سپس اثبات‌ها توسط هسته ناب بررسی می‌شوند. این وظیفه هسته است که خروجی تفصیل را بررسی و تأیید کند.

هسته ناب چندین هزار خط کد C++ است. هسته به دقت مهندسی شده است اما بسیار پیچیده است. ما در بالا به mathlib اشاره کردیم که شامل حدود 2.5M SLOC است که به زبان Lean نوشته شده است. کتابخانه به تفصیل شرح داده شده است، سپس توسط هسته بررسی شده است. اگر در هر جایی از این 2.5 میلیون خط کد، یک اثبات نادرست بدون قید و شرط وجود داشته باشد، این تقصیر هسته یا زمان اجرا است که نتوانسته است یک اثبات نادرست را رد کند. هر نقصی در نظریه نوع اساسی یک نقص جدی هسته است، اگر در کد پیاده سازی شود.

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

برای مثال، برای Navier-Stokes، یک انسان باید بررسی کند که عبارت Lean با بیانیه Fefferman در مورد مسئله جایزه هزاره مطابقت دارد، و به طور خاص مفاهیمی مانند میدان اعداد واقعی، مشتقات جزئی و اندازه گیری به درستی در Lean تعریف شده اند. ابزار مقایسه در Lean به این کار کمک می کند. این ابزار همچنین می‌تواند بررسی‌های اضافی مانند بازرسی برای بدیهیات غیرمجاز احتمالی را انجام دهد.

یک اشکال سالم، یک اشکال در هسته است که اجازه اثبات "نادرست" و در نتیجه اثبات هر گزاره را می دهد. یک اشکال سالم فاجعه‌بارترین اشکال در دستیار اثبات است و باید زنگ خطری را برای ریاضیدانانی که عمیقا به قابلیت اطمینان ریاضیات اهمیت می‌دهند به صدا درآورد. گاهی اوقات، اشکالات سلامت در دستیارهای اثبات مختلف یافت می شود. در سال 2003، من یک اشکال سالم را در دستیار اثبات HOL Light یافتم که در آن زمان به عنوان قابل اعتمادترین هسته‌ها در نظر گرفته شد. آن هسته کوچک است و فقط از چند صد خط کد کامپیوتری تشکیل شده است.

برای من، این یک نشان افتخار است که این باگ سلامت را پیدا کردم، که اولین باگ سلامتی بود که از سال 1996 در آن دستیار اثبات یافت شد. (به گزارش تغییر نور HOL، ژوئیه 2003 مراجعه کنید.)

Lean 4 در سپتامبر 2023 منتشر شد. قبل از انتشار، دو باگ سالم پیدا و اصلاح شدند. در ماه مه 2025، یکی دیگر از اشکالات سلامت گزارش شد که ناشی از سرریز بود. همه جهنم ها در بهار و تابستان 2026 از بین رفت که اکنون به آن "تابستان اشکالات صدا" می گویند. چندین باگ سلامت در Lean در جولای و آگوست کشف شد. جنون تابستانی دستیاران اثباتی مختلفی را تحت تاثیر قرار داد، اما تمرکز من روی ناب است. یک اشکال ناب منجر به رد غیرقانونی حدس کولاتز شد. من در تابستان امسال هنگامی که یک اثبات غیرقانونی کوتاه از حدس کپلر در Lean ارائه کرد، از این اشکال مطلع شدم.

همه این اشکالات به سرعت تعمیر شدند و mathlib توسط هسته تعمیر شده تأیید شده است. تجزیه و تحلیل اشکالات سلامت در پس از مرگ دو مورا یافت می شود.

«تابستان اشکالات سلامت ناب» ممکن است مانند یک فاجعه به نظر برسد، اما بررسی دقیق تر نشان می دهد که تشخیص این اشکالات سلامتی یک پیشرفت مثبت است. اشکالات تابستانی توسط هوش مصنوعی مدل مرزی در دستان محققان امنیتی علاقه مند به هسته های قابل اعتماد شناسایی شدند، نه توسط هکرهای کلاه سیاه. باگ Collatz توسط رامانا کومار، یکی از نویسندگان "CakeML: پیاده سازی تایید شده ML" پیدا شد، که یک ML تایید شده سرتاسر (زبان برنامه نویسی کاربردی) ایجاد می کند. چندین باگ توسط دن سلسام پیدا شد.

طبق گزارش دی مورا، «دانیل سلسام در OpenAI به Lean FRO با یک هوش مصنوعی متخصص در امنیت سایبری کمک کرد و اشتباهات برنامه‌نویسی دیگری را در هسته ناب پیدا کرد. همه آنها برطرف شده‌اند.» همکاری با سلسام "زمانی که هوش مصنوعی داخلی گزارش داد که نمی تواند مشکلات اضافی پیدا کند" پایان یافت. دن سلسام از روزهای اولیه به Lean کمک کرده است و یکی از خالقان چالش بزرگ IMO با هدف دستیابی به حل مسئله در سطح IMO تأیید شده در Lean بود. او اخیرا به دلیل هشدار خود در مورد ایمنی هوش مصنوعی (14 سپتامبر) که در یک پست ویروسی در X.com گزارش شده است، در اخبار بوده است.

پیشنهادهای مختلفی در مورد نحوه جلوگیری از اشکالات سلامت در Lean ارائه شده است. من در مورد سه بحث خواهم کرد.

1. سایر هسته های ناب را توسعه دهید و اثبات های رسمی را بررسی کنید.

حدود 25 هسته برای Lean نوشته شده است. "Lean Kernel Arena" آنها را فهرست می کند.

همه کسانی که به ترکیب فعلی هسته ها اعتماد ندارند، می توانند کرنل خود را برای Lean بنویسند. من گاهی اوقات با ایده نوشتن یک هسته بازی کرده ام و پروژه را بدون موفقیت به دانش آموزان پیشنهاد داده ام. به نظر من این یک راه عالی برای یادگیری کامل Lean است. من دن سلسام را از سال 2016 می شناسم، زمانی که در مورد پروژه فارغ التحصیل-دانشجوی او در استنفورد شنیدم که یک هسته ناب را در هاسکل ایجاد کرد. یکی دیگر از هسته های اولیه ناب در اسکالا توسط گابریل ابنر در سال 2017 نوشته شد.

رسمی شدن Navier-Stokes قبلا توسط بیش از دوجین بررسی کننده اثبات تایید شده است. بررسی متقاطع اثبات توسط هسته های مختلف، همه شک را برطرف نمی کند. باگ Collatz با بررسی متقابل هسته نانودا که تا حدودی قدیمی شده بود، کشف نشد، هسته ای که رد غیرقانونی Collatz را به دلیل باگ نامرتبط خود پذیرفت. تراشه های کامپیوتری ممکن است دارای اشکالات طراحی و نقص های تولید باشند. خطاهای نرم، اشکالات سیستم عامل و اشکالات کامپایلر وجود دارد. هسته های مختلف ممکن است نقص های یکسانی داشته باشند.

برخی از این خطاها را می توان با اجرای هسته های مختلف که به زبان های برنامه نویسی مختلف بر روی سخت افزارها و سیستم عامل های مختلف پیاده سازی شده اند، کاهش داد.

در حالت ایده‌آل، ما می‌خواهیم یک طراحی اتاق تمیز از هسته ناب داشته باشیم - یک پیاده‌سازی هسته که به کد منبع هسته Lean 4 نگاه نمی‌کند تا از کپی کردن اشکالات از یک هسته به هسته دیگر جلوگیری شود.

ناقص بودن گودل ما می خواهیم یک مدرک رسمی داشته باشیم که نشان دهد هسته Lean 4 هیچ اشکالی ندارد. با این حال، قضیه ناقص بودن دوم گودل محدودیت های شدیدی را برای این تعهد ایجاد می کند. بیشترین امیدی که ممکن است داشته باشیم اثبات سازگاری نسبی است. اگر فلان سیستم سازگار باشد، ناب 4 سازگار است. هیچ اشکال سلامتی ندارد. دلیلی مبنی بر نادرستی ارائه نخواهد کرد.

یک سنت طولانی برای تأیید رسمی هسته ها وجود دارد. در اصل، تأیید رسمی می‌تواند هم مشخصات منطقی یک هسته و هم اجرای دقیق آن را در کد بررسی کند. اما برخی از تأییدیه ها ممکن است یکی را بررسی کنند اما دیگری را بررسی نکنند. سال ها پیش، جان هریسون به طور رسمی هسته هسته دستیار ضد نور HOL را در نسخه تقویت شده HOL Light تأیید کرد. این یک اثبات مفهوم ارائه داد. پیشرفت بیشتر، اجرای HOL Light در CakeML است که در بالا ذکر شد، که یک زبان برنامه نویسی با معنایی رسمی و یک کامپایلر تایید شده است.

این کاری است که پروژه Candle انجام می دهد.

پروژه های اصلی تأیید هسته دیگری برای دستیاران اثبات وجود دارد.

یواخیم برایتنر در یک پست آنلاین در 10 سپتامبر نوشت: "من به طرز کودکانه ای افتخار می کنم که به تازگی یک بررسی ناب با یک اثبات سازگاری رسمی منتشر کردم. من اعلام می کنم تابستان باگ های پیاده سازی هسته یافت شده با هوش مصنوعی به پایان رسیده است!" ( @nomeata ). من فراتر می روم و این پروژه را به عنوان یکی از مهم ترین نقاط عطف در تاریخ Lean توصیف می کنم.

Breitner یک هسته ناب تایید شده به نام Con-Leche ایجاد کرده است. پیاده سازی در Lean است و سازگاری در Lean با کد و اثبات های تولید شده توسط Claude رسمیت یافته است. اثبات سازگاری رسمی یک رمزگذاری ناب نظریه مجموعه ZF را فرض می‌کند که توسط سلسله مراتبی از کاردینال‌های غیرقابل دسترس تقویت شده است. جالب توجه است که معناشناسی Con-Leche برای اصطلاحات Lean به‌جای نظری نوع، مستقیما تئوری مجموعه‌ای است. Con-Leche mathlib را بررسی کرده است. این پروژه شامل سلب مسئولیت‌های معمول است که تأیید هسته مفروضاتی را درباره کامپایلر، زمان اجرا و محیط رایانه ایجاد می‌کند.

اثبات سازگاری Con-Leche توسط بیش از ده ها اثبات کننده دیگر بررسی شده است. ادعای سازگاری Con-Leche ممکن است برای همه اهداف عملی کافی باشد، حتی اگر در جزئیات فنی با ادعای سازگاری نظریه نوع ناب متفاوت باشد.

یکی از جنبه‌های بسیار مثبت کار برایتنر این است که برخی از نامفهوم‌ترین بخش‌های Lean، مانند ماشین‌های عمومی انواع استقرایی متقابل با تودرتو، اکنون دارای ضمانت‌های سازگاری هستند که توسط یک مدل تئوری مجموعه‌ها پشتیبانی می‌شود.

3. درک نظری خود را از نظریه هسته و نوع Lean (گویش خاصی از حساب ساختارهای استقرایی که دارای جهان‌های غیر تجمعی و بی‌ربط بودن اثبات است) بهبود ببخشیم.

سند اساسی برای نظریه نوع ناب، پایان نامه کارشناسی ارشد ماریو کارنیرو در کارنگی ملون (2019) است. لهجه‌های CIC که توسط Rocq و Lean استفاده می‌شود به اندازه کافی متفاوت هستند که نتایج مستقیما از یکی به دیگری منتقل نمی‌شوند. متأسفانه خطایی در پایان نامه مشاهده شد. این پایان نامه نیز قدیمی است، زیرا سیستم قدیمی Lean 3 را هدف قرار داده است. کار برای تعمیر و گسترش پایان نامه ادامه دارد.

به عنوان یکی از اعضای کمیته پایان نامه او، وقتی او ثابت کرد که برابری تعریفی در Lean غیرقابل تصمیم گیری است، شوکه شدم. در عمل، این بدان معناست که الگوریتم ناب نمی تواند برابری تعریفی برخی از اصطلاحات را که در واقع از نظر تعریفی برابر هستند، ایجاد کند. این نتیجه منفی با خطا کاهش پیدا نکرد. هنوز یک قضیه است.

برخی از ویژگی های مورد نظر نظریه نوع لین و وضعیت فعلی اثبات ها را ذکر می کنیم.

در بالا، در ساده‌سازی «مضحک» نظریه نوع، بیان کردیم که هر اصطلاح یک نوع منحصر به فرد دارد. به طور دقیق تر، تایپ منحصر به فرد این ویژگی است که اگر یک اصطلاح دارای هر دو نوع A و B باشد، A و B قطعا برابر هستند. تایپ منحصربفرد یک ویژگی در منطق Lean نیست. این یک حدس پیچیده است که هنوز ثابت نشده است. سوالات بسیار اساسی دیگر در مورد نظریه نوع لین بی پاسخ مانده است، از جمله Pi-injectivity، ویژگی اصلاح شده Church-Rosser، و sort injectivity.

این ویژگی بیان می کند که در سیستم Lean با بدیهیات داده شده، با فرض سازگاری نظریه مجموعه ها (با بدیهیات مناسب) اشتقاقی از False وجود ندارد. البته، سازگاری منطقی تنها مهم‌ترین ویژگی است که باید از نظریه نوع لین بخواهیم. از اکتبر 2026، من هیچ اثبات کامل و عمومی برای سازگاری نسبی که نظریه نوع انتزاعی ناب را پوشش دهد، نمی شناسم.

ماریو کارنیرو در پایان نامه و در سخنرانی های خود ادعا کرده است که یک مسیر جایگزین برای ایجاد ثبات وجود دارد که از خطای پایان نامه جلوگیری می کند، اما تا آنجا که من می دانم، این مسیر جایگزین هرگز نوشته نشده است، فراتر از بیان مختصری در مقدمه پایان نامه او. به نظر من، نتیجه ای با چنین اهمیت اساسی باید قبل از پذیرش به طور کامل ارائه شود. Con-Leche، که در بالا مورد بحث قرار گرفت، یک ادعای سازگاری نزدیک مرتبط با نظریه مجموعه ها را مطرح و به طور رسمی تأیید می کند.

پیشرفت در این مشکلات تحقیقاتی در حال انجام است (arXiv:2607.13662، arXiv:2403.14064، Carneiro/AITP2026).

در صحبت‌های خود، ماریو کارنیرو بارها از سایر محققان درخواست کرده است که در فرانظریه بنیادی Lean مشارکت کنند، "نیم دوجین نفر روی MetaCoq کار می‌کنند، اما Lean نظریه‌پردازان نوع کافی را درگیر نمی‌کند. اگر شما را به عنوان چنین شناسایی می‌کنید، بیایید کمک کنید!" (اسلایدهای بحث بن، 24/07/2024). من درخواست او را دوم می کنم.

ارزیابی کلی من این است که درک نظری ما از تئوری تیپ Lean آن چیزی نیست که می‌خواهیم باشد و جامعه ریاضی به طور کلی به سؤالات نظری نوع بسیار مهم مربوط به Lean اشاره کوتاهی می‌کند. اگر به عنوان یک حرفه به طور کلی از نظریه مجموعه ها به نظریه نوع مهاجرت کنیم، باید حتی بیشتر برای تحکیم فرانظریه بنیادی تلاش کنیم.