1/ AxiomProver는 수치 반군(numerical semigroup)의 시지기(syzygie)에 관한 Fel의 미해결 추측을 해결했으며, 사람의 개입 없이 Lean 언어로 형식적인 증명을 자율적으로 생성했습니다.

인공지능 시스템이 이론 구축 수학 분야의 미해결 연구 문제를 해결하고 스스로 검증한 것은 이번이 처음입니다.

2/ 저희는 이 문제를 의도적으로 선택했습니다. 이는 복잡한 계층적 분해, 역추적 능력, 그리고 정의의 자동 형식화 능력 등 심오한 역량을 요구하는 이론 구축 수학 연구이기 때문입니다.

퍼트넘 만점 이후, AxiomProver는 연구 수학을 생성했습니다.

3/ AxiomProver는 검증된 AI 시스템(개발 중)으로, 처음에는 AI 수학자가 되는 것을 목표로 합니다. 지금 바로 질문을 제출하세요!

이 과정은 문제에 대한 자연어 설명 입력으로부터 AxiomProver가 처음부터 끝까지 처리합니다. 출력은 올바른 Lean 파일입니다.

4/ 펠은 덧셈 정수론과 가환 대수학의 교차점, 즉 연구 수학의 핵심 영역에서 수치 반군의 시지기 불변량에 대한 닫힌 공식을 제시합니다. 이 공식에는 라마누잔의 잃어버린 노트에도 등장하는 보편 다항식 Tₙ이 포함됩니다.

5/ 이것은 앞으로 발표될 일련의 논문 중 첫 번째일 뿐입니다. arXiv를 매일 구독하신다면 (오늘 밤에도 구독하실 수 있겠죠?), 저희의 더 많은 연구 결과를 그곳에서 확인하실 수 있습니다!

arXiv 링크(출판을 위해 제출된 사전 출판물): https://arxiv.org/abs/2602.03716

GitHub 링크 (간결한 코드): https://github.com/AxiomMath/fel-polynomial