TL;DR

이 저장소는 Erdős 계열 수학 문제들의 증명을 모아 AI의 보조로 논리적 일관성을 검토하고 일부 항목을 Lean으로 형식화하여 기계적 검증을 병행하고 있다. AI는 자연어 증명의 초기 검토 단계에서 잠재적 오류와 누락을 식별하고 사람이 이를 보완한 뒤 형식화 가능한 증명은 Lean 코드로 옮겨 proof assistant이 각 단계를 확인하도록 구성되었다. 이미 형식화된 증명은 기계적 타당성을 확보한 상태이며 다른 항목의 형식화는 현재 진행 중이라 모든 증명이 아직 기계 검증을 통과한 것은 아니다. 따라서 증명 재현이나 형식화 사례 연구를 하려는 연구자에게는 유용한 출발점을 제공하지만 전체 데이터셋의 완전한 형식화 여부는 제한적이라는 점을 고려해야 한다.

핵심 포인트

• AI 보조를 증명 검토 초기 단계에 도입하여 인간 점검 전에 잠재적 논리적 불일치를 식별한 점이 특징이다. 이 방식은 전체 형식화 작업의 우선순위를 결정하는 데 활용되며 반복적인 발견-수정 과정을 줄이는 방향으로 설계되었다. 결과적으로 형식화 자원이 제한된 상황에서 효율적으로 Lean 형식화 대상을 선별할 수 있었다.
• 일부 증명을 이미 Lean으로 형식화하여 기계적 검증 결과를 공개한 점이 차별화 요소이다. 형식화 결과물은 증명의 각 단계를 타입 이론 기반으로 표현하고 proof assistant에서 통과되는 구체적 아티팩트를 제공한다. 이 아티팩트는 다른 연구자가 재현하거나 확장할 수 있는 기반 자료로 활용될 수 있다.
• Erdős 계열 문제들의 증명 텍스트를 수집하여 저장소에 정리하고 있다. 각 증명은 소스와 논거를 함께 보관하여 추적 가능하게 구성되어 있다. 저장소는 증명별로 형식화나 검증 상태를 표시하여 현재 작업 진행 상황을 파악할 수 있게 한다.
• AI의 도움을 받아 증명의 논리적 오류와 불일치를 확인하는 과정을 거쳤다. AI는 자연어로 된 증명의 논리적 연속성을 점검하는 보조 역할을 수행했으며 그 결과를 바탕으로 사람이 추가 점검을 진행했다. 이 결과 일부 증명은 기계적 검증을 위한 수정 또는 보완을 거쳐 형식화 대상으로 선정되었다.