Lean Machine-Checked Mathematics and Verified Programming, Past and Future (Leonardo de Moura)

Leonardo de Moura, AWS

Z3에 불평이 많다 - whole-program 할 때, minor code edit이 solver trace를 깨뜨린다

Lean은 모르는 사람들끼리도 협업이 가능하게 됐으며,

extensible하고, own system을 구현할 수 있다.

types, systems = first-class objects

• Lean에서는 타입과 시스템(예: 모나드, 리라이트 규칙 등)을 프로그램 값처럼 다룬다. 즉, 함수의 인자로 넘기거나 리스트에 담고, 런타임에 생성·조작할 수 있어 메타프로그램 작성과 도메인 특정 확장이 쉬워진다.

dependent type theory

• Lean은 종속 타입 이론(dependent type theory)을 기반으로 하며, X는 “CIC(Calculus of Inductive Constructions)” 같은 구체적 변형을 가리킨다. 종속 타입 덕분에 프로그램과 증명이 같은 언어에서 작성·검증되며, 복잡한 사전 조건·후조건을 타입 수준에서 표현할 수 있다.

수학자들이 constructive class든지 뭐든지, Lean개발자들도 모르는 것들 때문에 Lean을 좋아하고 있다.

A Lean proof of Fermat’s Last Theorem

https://imperialcollegelondon.github.io/FLT/blueprint.pdf -> https://pitmonticone.github.io/FLT3/blueprint/dep_graph_document.html (n=3) -> https://pitmonticone.github.io/FLT3/docs/FLT3/FLT3.html#Solution'.multiplicity_lambda_c_finite (specific lemma)

Lean in software verification

Cedar - https://aws.amazon.com/ko/blogs/opensource/lean-into-verified-software-development/ Cedar는 개발자가 애플리케이션의 권한을 정의하고 적용하는 데 사용할 수 있는 권한 부여 정책을 작성하는 오픈 소스 언어 입니다 .

“Maintaining the proofs” 에서 Lean이 매우 좋음.

SampCert

Geometrics가 CompCert에 기여했듯이. Mathlib 덕분에, Lean으로 SampCert를 만들 수 있었다 - 푸리에 분석, 정수론, 위상수학

Lean is extensible - can build own proofs

https://techcommunity.microsoft.com/blog/microsoft-security-blog/microsofts-quantum-resistant-cryptography-is-here/4238780 https://www.microsoft.com/en-us/research/publication/aeneas-rust-verification-by-functional-translation/

https://github.com/phlippe/Lean_hammer

• https://www.themoonlight.io/ko/review/premise-selection-for-a-lean-hammer Lean에서 “hammer”는 복잡한 증명 목표를 자동화된 외부 정리 증명기(예: Z3, Vampire)나 SMT 솔버에 넘겨 대신 증명하도록 한 뒤, 그 결과를 다시 Lean 내부의 증명 체계로 끌어오는 도구입니다.

1. 역할

   • 사용자가 수동으로 작성하기 어려운 복잡한 증명 의무(goal)를 외부 ATP(Automated Theorem Prover)에 맡깁니다.

   • ATP가 찾은 증명 스텝을 Lean의 정리나 전술(tactic) 형태로 재구성하여, 사용자는 단순히 한 줄의 명령으로 강력한 자동 증명 기능을 활용할 수 있습니다. 1(https://github.com/phlippe/Lean_hammer)

2. 이름 유래

   • Isabelle/HOL에서 제공하는 “Sledgehammer” 전술에서 영향받았습니다. “Sledgehammer”가 못을 박듯, 어렵게 느껴지는 증명 목표를 강력하게 타격(해결)해 준다는 의미를 담고 있습니다. 5(https://www.themoonlight.io/ko/review/premise-selection-for-a-lean-hammer)

3. 장점

   • 증명 시간을 크게 단축
   • 복잡한 논리 구조도 외부 솔버의 탐색 능력으로 처리
   • Lean 안팎의 도구를 결합해 증명 자동화 환경을 확장

이처럼 Lean hammer는 “무거운 망치”처럼 강력한 자동 증명 지원을 제공하여, 증명 개발 속도를 높이고 사용자 부담을 줄여 줍니다.

🌐 Sources

1. github.com - Development repository of a hammer for Lean.

2. github.com - Lean_hammer/leanhammer.lean at master

3. leanprover-community.github.io - Lean projects

4. leanprover-community.github.io - Duper

5. themoonlight.io - [논문 리뷰] Premise Selection for a Lean Hammer

6. openreview.net - LeanAgent: Lifelong Learning for Formal Theorem Proving

grind

Grind는 SMT 솔버 구조를 본뜬 자동화 프레임워크다. 다음 네 단계로 동작한다.

1. 제약 수집 및 기재

   • 입력 문제에서 나타나는 등식·부등식을 탐색해 “검사판(board)”에 기록

   • 각 제약을 목록화해 전체 컨텍스트를 구성

2. 동치류 병합(Equivalence Merging)

   • 기록된 등식들을 통해 변수나 표현식을 동일 클래스에 묶음

   • Congruence closure 기법으로 유도 가능한 모든 동치 관계를 효율적으로 통합

3. 협력 엔진(Cooperating Engines)

   • Case Analysis Engine: 분기별 가능한 케이스(예: x>0, x≤0)를 나눠 각각 독립 해결

   • E-Analysis Engine: 등식 및 함수 결합 특성을 사용해 추가 동치·부등식 유도

   • Theory Solvers: 선형산술, 부동소수점, 배열 등 각 이론 전용 하위 솔버와 연동

4. 충돌 탐지 및 해소(Conflict Resolution)

   • 서로 모순되는 제약이 발견되면 간단한 학습(clause learning)으로 원인 기록

   • 모순을 일으키는 경로를 차단해 더 깊은 탐색으로 유도

이 과정을 반복하며, 모든 제약이 만족되거나 모순이 증명될 때까지 자동으로 증명·해결을 수행한다. SMT 솔버의 핵심 요소인 제약 전파(constraint propagation), 분기(case splitting), 동치 추론(equivalence reasoning)을 체계적으로 결합함으로써 매우 확장 가능하고 효율적인 자동화 환경을 제공한다.

🌐 Sources

1. arxiv.org - SMT-Solving Induction Proofs of Inequalities

2. arxiv.org - SMT(LIA) Sampling with High Diversity

3. researchgate.net - Efficient E-Matching for SMT Solvers

4. sat-smt-ar-school.gitlab.io - SAT/SMT/AR Summer School 2024

Verified AI(-generated proof)

AlphaProof, AlphaGeometry, ChatGPT 그리고 신경-기호적 AI의 미래 2024-07

자연어를 formal language로 변환하면서 lean으로 검증