모든 목표는 Lean에 고정되며, 독립적으로 검토된 증명이 있어야만 해결된 것으로 간주되고, 그 공로는 그 뒤에 있는 사람 또는 AI 에이전트에게 돌아간다.
2026년 10월 28일 수요일 · 12:15 EDT · 1분 읽기
교육 분야에서
공유
새로운 공개 수학 챌린지가 사람과 AI 에이전트를 대상으로, STARK 증명이 더 적은 검증을 수행하고 크기를 줄일 수 있게 해주는 더 엄밀한 한계를 증명하도록 요청한다고 해당 챌린지 웹사이트가 밝혔다. 이 프로젝트는 provably.fast 워크숍으로 운영되며, 코드는 starknet-innovation GitHub 조직 아래에 호스팅된다.
STARK는 해시 함수에만 의존하는 영지식 증명이다. 이 챌린지는 검증자가 필요로 하는 쿼리 수를 결정하는 리드-솔로몬 근접성 테스트에서의 "불량 챌린지" 수를 대상으로 한다. 알려진 경계는 Dao, Kominers, Thaler(2026)에서 비롯된다.
Lean에서 검증된 세 가지 목표
이 사이트는 알려진 이차 경계를 일차 경계로 대체하는 것과 더 넓은 범위에 걸쳐 이차 경계를 증명하는 것을 포함한 세 가지 목표를 제시한다. 각 명제는 Lean 정리 증명기에 고정되어 있으며, 독립적으로 검토된 증명에 의해서만 해결된다. 사이트는 경계만으로는 아무것도 축소되지 않으며, 실질적인 절감을 위해서는 완전한 프로토콜 분석도 필요하다고 지적한다.
공개: 이 기사는 Estefano Gomez가 편집했습니다. 콘텐츠 제작 및 검토 방식에 대한 자세한 내용은 편집 정책을 참조하세요.