MathlibLemma: 형식 수학을 위한 민속 정리 생성 및 벤치마크

MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics

Lean 및 Mathlib 생태계는 대규모 언어 모델(LLM)의 도움으로 형식적 수학적 추론 분야에서 큰 성공을 거두었지만, Mathlib에 많은 민속 정리가 부족하다는 점은 여전히 Lean의 실용성을 제한하는 주요 장애물입니다. 이러한 문제를 해결하기 위해, 우리는 수학적 민속 정리를 자동으로 발견하고 형식화하는 최초의 LLM 기반 다중 에이전트 시스템인 MathlibLemma를 소개합니다. 이 프레임워크는 수학의 핵심 연결 고리를 적극적으로 발굴하는 우리의 주요 기여입니다. 이 시스템의 효과는 검증된 민속 정리 라이브러리 생성으로 입증되었으며, 이 중 일부는 이미 Mathlib의 최신 버전에 공식적으로 통합되어 시스템의 실제 유용성과 전문가 표준과의 일관성을 검증했습니다. 이러한 파이프라인을 활용하여, 우리는 4,028개의 타입 검사를 통과한 Lean 문장으로 구성된 MathlibLemma 벤치마크를 구축했습니다. 이 연구는 LLM의 역할을 수동적인 소비자에서 적극적인 기여자로 전환하여 형식적 수학 라이브러리의 자체 진화를 위한 건설적인 방법론을 제시합니다.

While the ecosystem of Lean and Mathlib has enjoyed celebrated success in formal mathematical reasoning with the help of large language models (LLMs), the absence of many folklore lemmas in Mathlib remains a persistent barrier that limits Lean's usability as an everyday tool for mathematicians like LaTeX or Maple. To address this, we introduce MathlibLemma, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas. This framework constitutes our primary contribution, proactively mining the missing connective tissue of mathematics. Its efficacy is demonstrated by the production of a verified library of folklore lemmas, a subset of which has already been formally merged into the latest build of Mathlib, thereby validating the system's real-world utility and alignment with expert standards. Leveraging this pipeline, we further construct the MathlibLemma benchmark, a suite of 4,028 type-checked Lean statements spanning a broad range of mathematical domains. By transforming the role of LLMs from passive consumers to active contributors, this work establishes a constructive methodology for the self-evolution of formal mathematical libraries.