Nowe otwarte wyzwanie matematyczne zaprasza zarówno ludzi, jak i agentów AI do udowodnienia ściślejszych granic, które pozwolą dowodom STARK wykonywać mniej sprawdzeń i zmniejszyć swój rozmiar — zgodnie z stroną wyzwania.

Projekt jest prowadzony jako warsztat provably.fast, a jego kod hostowany jest w organizacji GitHub starknet-innovation — co plasuje przedsięwzięcie w ekosystemie Starknet, gdzie dowody STARK służą do weryfikacji wymagających obliczeń za pomocą lekkich sprawdzeń.

STARKi to dowody o zerowej wiedzy, które opierają się wyłącznie na funkcji skrótu. Ponieważ każde zapytanie, które musi wykonać weryfikator, dodaje dane i pracę do każdego sprawdzenia, granice stojące za tymi zapytaniami są uważnie obserwowane w systemach dowodowych. Wyzwanie dotyczy liczby „złych challenge” w teście bliskości Reeda-Solomona, która określa, ile zapytań musi wykonać weryfikator. Obecnie znane granice pochodzą od Dao, Kominersa i Thalera (2026).

Trzy cele, weryfikowane w Lean

Strona wymienia trzy cele, w tym zastąpienie znanej granicy kwadratowej granicą liniową oraz udowodnienie granicy kwadratowej w szerszym zakresie. Każde twierdzenie jest zapisane w dowodzeniu twierdzeń Lean, a cel uznaje się za rozwiązany dopiero po zakończeniu niezależnie zrecenzowanego dowodu, z uznaniem dla osoby lub agenta AI stojącego za nim. Zapisanie twierdzeń w Lean eliminuje niejasności co do tego, co stanowi rozwiązanie, a rozszerzenie uznania na agentów AI czyni z wyzwania konkretny test tego, czy maszyny mogą wnosić wkład w matematykę na poziomie badawczym obok ludzkich uczestników.

Strona zaznacza, że sama ściślejsza granica niczego nie zmniejsza; rzeczywiste oszczędności wymagają również pełnej analizy protokołu. To zastrzeżenie wyznacza, na co zwracać uwagę: czy którykolwiek z trzech celów zostanie osiągnięty oraz czy późniejsza praca nad protokołem przełoży nową granicę na mierzalnie mniejsze dowody.

Źródło: CryptoBriefing