Interactive theorem provers (ITPs) like Lean 4, Coq, and Isabelle enable mathematicians and computer scientists to construct machine-checked proofs of mathematical theorems and software correctness properties. The proofs are rigorous—every step is verified against the system's foundational logic—but the process of constructing them is painstaking. Users write proofs interactively, applying tactics one at a time, inspecting the resulting proof state, and deciding the next tactic. For complex proofs, this process can take hours or days of expert effort.

Automated theorem provers (ATPs) like E, Vampire, and Z3 take a different approach: given a logical formula, they search for a proof automatically, using resolution, superposition, and SMT (satisfiability modulo theories) techniques. ATPs are powerful for first-order logic but cannot directly handle the richer type theories that ITPs use.

Hammers bridge this gap: they translate goals from the ITP's type theory into first-order logic, send them to ATPs, and translate the proofs back. Isabelle's Sledgehammer has been the gold standard for years—handling routine proof obligations automatically and freeing users to focus on the creative aspects of proof construction.

Lean 4, despite its rapid adoption, has lacked a mature hammer. Qian et al.'s Lean-auto fills this gap, providing the first production-quality interface between Lean 4 and external ATPs.

The Lean-auto Architecture

Lean-auto operates as a Lean 4 tactic that, when invoked, performs the following steps:

The translation step is the most technically challenging. Lean 4's type theory is strictly more expressive than first-order logic—some goals cannot be translated faithfully. Lean-auto handles this through a combination of encoding techniques (defunctionalization for higher-order functions, monomorphization for polymorphism) and graceful fallback (returning "unsolved" for goals that resist translation).

Machine Learning for Premise Selection

Piepenbrock's work on ML-guided ATP provides the theoretical foundation for Lean-auto's premise selection step. The Mathlib library contains over 200,000 theorems (as of 2025). Sending all of them to the ATP would overwhelm it; sending too few might omit the critical lemma. ML-based premise selection—trained on the corpus of existing Lean proofs—predicts which lemmas are most likely to be useful for a given goal.

The ML model learns from the history of proof construction: when mathematicians proved similar goals in the past, which lemmas did they use? This historical data encodes expert mathematical judgment about lemma relevance—judgment that the ML model distills into a fast, automated relevance ranking.

Claims and Evidence

Open Questions

What This Means for Your Research

For Lean 4 users (an increasingly large community including mathematicians, computer scientists, and verification engineers), Lean-auto is an immediate productivity tool. Routine proof obligations that previously required manual tactic construction can now be dispatched with a single command.

For formal verification researchers, Lean-auto brings Lean 4 closer to parity with Isabelle in terms of automation infrastructure—a critical factor for Lean's adoption in industrial verification projects where proof engineer productivity determines project feasibility.

면책 조항: 이 게시물은 정보 제공을 목적으로 한 연구 동향 개요이다. 학술 저작물에서 인용하기 전에 구체적인 연구 결과, 통계 및 주장은 원본 논문을 통해 확인해야 한다.

Lean-auto: 대화형 증명 보조기와 자동 정리 증명기의 연결

Lean 4, Coq, Isabelle과 같은 대화형 정리 증명기(ITP)는 수학자와 컴퓨터 과학자가 수학 정리 및 소프트웨어 정확성 속성에 대한 기계 검증 증명을 구성할 수 있게 해준다. 증명은 엄밀하다—모든 단계가 시스템의 기초 논리에 대해 검증된다—그러나 증명을 구성하는 과정은 매우 힘들다. 사용자는 대화형으로 증명을 작성하며, 한 번에 하나씩 전술(tactic)을 적용하고, 결과로 나타나는 증명 상태를 검사한 후, 다음 전술을 결정한다. 복잡한 증명의 경우 이 과정에 전문가의 노력이 몇 시간 또는 며칠씩 소요될 수 있다.

E, Vampire, Z3 같은 자동 정리 증명기(ATP)는 다른 접근 방식을 취한다. 주어진 논리 공식에 대해 귀납(resolution), 중첩(superposition), SMT(satisfiability modulo theories) 기법을 사용하여 자동으로 증명을 탐색한다. ATP는 1차 논리(first-order logic)에 강력하지만, ITP가 사용하는 더 풍부한 유형 이론(type theory)을 직접 처리할 수 없다.

해머(Hammer)는 이 간극을 연결한다. ITP의 유형 이론에서 목표를 1차 논리로 변환하고, ATP로 전송한 후, 증명을 다시 변환한다. Isabelle의 Sledgehammer는 수년간 표준으로 자리 잡아 왔으며, 일상적인 증명 의무를 자동으로 처리하고 사용자가 증명 구성의 창의적인 측면에 집중할 수 있게 해준다.

Lean 4는 빠른 도입에도 불구하고 성숙한 해머가 부재했다. Qian 등의 Lean-auto는 이 간극을 채우며, Lean 4와 외부 ATP 사이의 첫 번째 프로덕션 품질 인터페이스를 제공한다.

Lean-auto 아키텍처

Lean-auto는 Lean 4 전술로 작동하며, 호출 시 다음 단계를 수행한다:

변환 단계가 기술적으로 가장 어렵다. Lean 4의 유형 이론은 1차 논리보다 표현력이 엄격히 더 높아, 일부 목표는 충실하게 변환될 수 없다. Lean-auto는 인코딩 기법(고차 함수를 위한 비함수화(defunctionalization), 다형성을 위한 단형화(monomorphization))과 점진적 폴백(변환에 저항하는 목표에 대해 "미해결"을 반환)의 조합을 통해 이를 처리한다.

전제 선택을 위한 기계 학습

Piepenbrock의 ML 기반 ATP에 관한 연구는 Lean-auto의 전제 선택 단계에 대한 이론적 기반을 제공한다. Mathlib 라이브러리는 2025년 기준으로 200,000개 이상의 정리를 포함하고 있다. 이 모두를 ATP에 전송하면 과부하가 걸리고, 너무 적게 전송하면 핵심 보조정리가 누락될 수 있다. 기존 Lean 증명 말뭉치로 훈련된 ML 기반 전제 선택은 주어진 목표에 대해 어떤 보조정리가 가장 유용할지 예측한다.

ML 모델은 증명 구성의 이력으로부터 학습한다. 수학자들이 과거에 유사한 목표를 증명할 때 어떤 보조정리를 사용했는가? 이 역사적 데이터는 보조정리 관련성에 대한 전문가적 수학적 판단을 인코딩하며, ML 모델은 이 판단을 빠르고 자동화된 관련성 순위로 정제한다.

주장과 근거

미해결 질문

연구에 주는 시사점

Lean 4 사용자(수학자, 컴퓨터 과학자, 검증 엔지니어를 포함하여 점점 커지는 커뮤니티)에게 Lean-auto는 즉각적인 생산성 도구이다. 이전에 수동 택틱 구성이 필요했던 일상적인 증명 의무는 이제 단일 명령으로 처리할 수 있다.

형식 검증 연구자에게 Lean-auto는 자동화 인프라 측면에서 Lean 4를 Isabelle과의 동등성에 더 가깝게 만든다. 이는 증명 엔지니어의 생산성이 프로젝트 실현 가능성을 결정하는 산업용 검증 프로젝트에서 Lean의 도입을 위한 핵심 요소이다.