Lean 정리 증명기
수학적 정리를 공식화하고 논리적 엄밀성을 검증하는 대화형 정리 증명 도구이다. AI 모델이 생성한 수학적 추론의 오류를 즉각적으로 확인하고 수정할 수 있는 환경을 제공하여 수학 자동화 연구의 핵심 도구로 활용된다.