دومین آزمایشگاه پیشروی هوش مصنوعی هم اکنون می‌گوید سامانه‌اش یکی از فرض‌های کاری نظریه پیچیدگی را فرو ریخته است. Anthropic روز ۲۷ اکتبر پوشه‌ای را به مخزن عمومی formal-math خود در GitHub افزود که شامل مقاله‌ای به نام Claude و یک توسعه Lean 4 است و به گفته شرکت، نادرستی فرضیه زمان نمایی (ETH) را اثبات می‌کند. این انتشار تنها چند ساعت پس از آن رخ داد که OpenAI ابطال ادعایی خود از همین حدس را منتشر کرد و هر دو گروه کار خود را مستقل از دیگری معرفی می‌کنند.
فرضیه زمان نمایی را راسل ایمپاگلیاتسو و راماموهان پاتوری در سال ۱۹۹۹ مطرح کردند. طبق این فرضیه، حل 3-SAT، یعنی تشخیص اینکه آیا یک فرمول بولی با بندهای سه‌لیترالی جواب دارد یا نه، برای یک ثابت مشخص به زمانی نمایی بر حسب تعداد متغیرها نیاز دارد. مقاله Anthropic الگوریتمی قطعی را شرح می‌دهد که از تصمیم‌گیری فراتر می‌رود و تعداد مقداردهی‌های برآورنده را می‌شمارد، آن هم در زمان ۲ به توان O(n log log n تقسیم بر جذر log n). چون این توان کندتر از هر مضرب ثابتی از n رشد می‌کند، نتیجه این است که 3-SAT در زمان 2^o(n) حل‌شدنی است.
روایت شکل‌گیری این نتیجه غیرعادی است. بنا بر یادداشت منشأ در صفحه مقاله در Hexagon، یک مدل پژوهشی داخلی Claude هسته الگوریتم را ۱۶ اکتبر و با تولید حدود ۱۴ میلیون توکن خروجی، بدون هیچ دخالت انسانی، پیدا کرده و پس از آن پژوهشگران Anthropic همراه با مدل متن را آماده کرده‌اند. همان صفحه مقاله را عمدتاً تولیدشده با هوش مصنوعی معرفی می‌کند. فایل README مخزن هم می‌افزاید که Claude Opus 5.5 با سطح تلاش بالا می‌تواند نسخه تصمیم‌گیری این ابطال را از روی یک راهنمای فشرده که در همان‌جا آمده دوباره به دست آورد.
بخش صوری طوری طراحی شده که دیگران بتوانند آن را بررسی کنند. فایلی کوتاه به نام MainResults.lean دو قضیه را روی مدل ماشین تورینگ کتابخانه Mathlib بیان می‌کند: نادرستی ETH و کران اصلی شمارش در مقاله. طبق README، هر دو فقط بر سه اصل موضوعه استاندارد Lean تکیه دارند، ساخت پروژه روی ۲۴ پردازنده مجازی حدود هشت دقیقه طول می‌کشد و بررسی خودکار مخزن با ابزار Comparator اثبات‌ها را با هسته دومی به نام nanoda که جداگانه نوشته شده، دوباره وارسی می‌کند. کد با مجوز Apache 2.0 منتشر شده است.
Anthropic صریحاً می‌گوید وارسی ماشینی چه چیزی را پوشش نمی‌دهد. Lean تأیید می‌کند که اثبات‌ها از تعریف‌های داده‌شده نتیجه می‌شوند، اما هیچ نرم‌افزاری تضمین نمی‌کند که MainResults.lean همان چیزی را بگوید که مقاله می‌گوید. تحلیلی در SXZ.io با استناد به خود مقاله یادآور می‌شود که تا جایی که معلوم است هیچ انسانی کد Lean نوشته‌شده توسط هوش مصنوعی را بازبینی نکرده است. همین تحلیل اشاره می‌کند که قضیه فقط وجود یک ثابت را تضمین می‌کند و بر پایه محاسبات خود مقاله، این کران در حالت پنج بند برای هر متغیر، تنها برای فرمول‌هایی با بیش از 10^10000 متغیر از جست‌وجوی کامل بهتر است.
مقایسه با کار OpenAI هم آغاز شده است. SXZ.io گزارش می‌دهد که گزاره Lean در کار Anthropic کل کران مقاله را در بر می‌گیرد و نادرستی ETH را مستقیماً بیان می‌کند، در حالی که قضیه صوری OpenAI توانی ضعیف‌تر از دست‌نوشته‌اش را پوشش می‌دهد؛ افزون بر این، پیکربندی Anthropic هسته دوم را فعال کرده و پیکربندی OpenAI آن را خاموش گذاشته است. TechCrunch که هر دو انتشار را پوشش داد، از رایان ویلیامز، استاد MIT، نقل کرد که اگر این ادعاها درست باشند، بسیاری از مقاله‌هایی که بر ETH تکیه دارند باید بازنگری شوند و جامعه علمی باید احتمال برابری P و NP را کمی جدی‌تر بگیرد.
داوری تخصصی تازه شروع شده است. ویلیامز، ایمپاگلیاتسو و پاتوری واکنش جامعه علوم رایانه به ادعای OpenAI را سازمان می‌دهند و نوشته‌اند که مشارکتشان به معنای تأیید ادعا نیست؛ برای مقاله Anthropic هنوز بررسی مشابهی اعلام نشده است. اثر عملی این یافته فعلاً محدود است. Anthropic تأکید می‌کند که نتیجه کاملاً مجانبی است و حل فرمول‌های واقعی را سریع‌تر نمی‌کند؛ بنابراین اهمیت آن در نظریه و در نشانه‌ای است که از توان سامانه‌های هوش مصنوعی برای تولید ریاضیات قابل‌وارسی به دست می‌دهد.