Зад сухите прес съобщения на компанията PSI и шумните заглавия за тридневния пробив стои един доста по-прозаичен и физически труден за преглъщане факт. В продължение на почти две десетилетия математици и теоретични физици се блъскаха в една конкретна математическа стена, формулирана през 2008 година от Скот Ааронсън и Андрис Амбаинис. Залогът никога не е бил просто академична престижност или точки за цитиемост в научните списания. Залогът бяха милиардите долари, излети в изграждането на криогенни охладителни среди, вакуумни камери и свръхпроводящи вериги. Големият въпрос на тази хипотеза беше дали определен клас сложни изчислителни проблеми всъщност изискват квантова архитектура, за да бъдат решени бързо, или класическите силициеви чипове могат да ги счупят с обикновено полиномиално увеличение на ресурсите. Когато една система смила алгоритмичните възможности за броени часове, това не е просто научен триумф, а пробойна в теорията за безграничното квантово превъзходство.
Архивното гробище на теоретичната информатика е пълно с хипотези, които изглеждаха елегантни на хартия, но се сринаха при сблъсъка с физическите лимити на хардуера. Хипотезата на Ааронсън-Амбаинис засягаше именно тези функции, които притежават специфична математическа симетрия и ниска степен на влияние на отделните променливи. Простият извод от доказателството, генерирано от модела на Anthropic в инфраструктурата на PSI, е неудобен за инвеститорите: за целия този специфичен клас задачи класическият компютър не се нуждае от експоненциално нарастващ ресурс от памет и време. Времето за процесинг тук не се умножава само по себе си до безкрайност, а расте предвидимо и овладяемо. Това срязва сериозна част от надеждите, че квантовият процесор ще бъде универсална панацея за всеки труден алгоритмичен казус.
Автоматизираната проверка чрез системата Lean дава абсолютна логическа съгласуваност на вътрешните структури на доказателството. Средата Lean не се вълнува от научен авторитет, нито от корпоративния пиар на PSI. Тя работи като стриктен и неумолим асистент, който проверява всяка стъпка от аксиомите до финалното заключение, изключвайки възможността за скрити субективни грешки. Тук обаче се появява един съществен изследователски проблем, който далеч не е затворен. Потвърждаването на вътрешната логика в Lean показва само, че символната верига е безгрешна спрямо заложените в програмата правила. То не гарантира автоматично, че формализираният код отразява едно към едно оригиналната физическа и математическа идея, заложена от Ааронсън и Амбаинис през 2008 година. Поради тази причина процесът по независим академичен преглед от Станфордския университет и широк кръг теоретици остава задължителен филтър.
