Axiom Math, 수학에서 AI 슬롭을 몰아내기 위한 노력 발표

Axiom Math는 인간이 쓴 최대 규모의 수학 문헌 중 하나인 Stacks Project를 형식 검증했다고 발표했다. 이 회사의 AI 에이전트는 약 7,654페이지 분량의 내용을 약 1,600만 줄의 Lean 코드로 변환해 컴퓨터 검증을 수행했다. Stacks Project는 2005년 Johan de Jong이 오픈소스 참고 자료로 시작한 것으로, 대수기하를 포함한 분야를 다룬다. 이 회사는 3월에 2억 달러 규모의 시리즈 A 투자를 유치했으며, Menlo Ventures가 주도했다.