Lean이 왜 독특한 도구인지, 구현, 확장성, 건전성, 사용자 중심 설계의 관점에서 Leonardo de Moura가 설명합니다.
Leonardo de Moura- [x] homeabout mepublicationsblognotespresentations
2026-04-02
Markus de Medeiros는 garbled circuits를 이해하고 싶어 했습니다. 그는 암호학에 대한 정규 교육을 받은 적이 없었습니다. 그는 Lean으로 오후 한때를 보냈습니다. 함수형 스타일의 회로 평가기, 메타프로그래밍을 통한 커스텀 DSL, FFI를 통한 OpenSSL 바인딩, 자신의 serializer에 대한 정당성 증명, 그리고 명령형 스타일의 가변 garbling 알고리즘까지. 모두 하나의 도구 안에서 말입니다.
그의 결론은 이랬습니다. "이 모든 것을 할 수 있는 다른 도구를 저는 정말로 알지 못합니다." 그리고 이어서 말했습니다. "이거 정말 미치도록 좋습니다."
이런 반응은 계속해서 반복됩니다. 이 글은 그 이유에 관한 것입니다.
하나의 결정. 그리고 그 밖의 모든 것이 거기서 따라 나옵니다. 컴파일러, 정교화기, 증명 자동화, 파서, pretty printer, 빌드 시스템, 문서화 시스템까지 모두 Lean입니다. 임시방편은 없습니다. OCaml과 Ltac 사이를 잇는 glue도 없습니다. 죽은 언어를 위한 난해한 컴파일러도 없습니다.
똑똑한 사람들이 Lean 자체를 사용해 Lean의 내부로 파고들 수 있기 때문에, 그들은 우리가 전혀 계획하지 않았던 것들을 만들어 냅니다. Mathlib 커뮤니티는 우리와의 별도 조율 없이 50,000줄이 넘는 확장 기능들(커스텀 tactics, linters, 자동화)을 작성했습니다. 우리의 문서화 시스템인 Verso 역시 Lean 위에 구축되어 있습니다. Ilya Sergey의 NUS 학생들은 Lean의 메타프로그래밍 계층 위에 Veil과 Velvet을 구축했습니다.
이 중 어느 것도 계획된 것이 아니었습니다. 우리는 그저 그것이 가능하도록 만들었을 뿐입니다.
Mathlib에는 200,000개가 넘는 정리와 220만 줄의 코드가 있습니다. 그리고 계속 성장하고 있습니다. 빌드 시간은 계속 줄어들고 있습니다.
우리는 작동하지 않는 설계를 과감히 버릴 의지가 있습니다. 우리는 타입 클래스 해결 시스템, simplifier 인프라, 옛 컴파일러, 새로운 증명 자동화에 있는 canonicalizer를 교체했습니다. 그것들이 망가졌기 때문이 아니라, 확장되지 않았기 때문입니다.
Lean FRO가 2023년 8월에 출범한 이후로, 확장성은 우리 사명의 핵심적인 일부였습니다.
Lean에는 작고 신뢰할 수 있는 커널이 있습니다. 서로 독립적인 여러 구현체가 존재합니다. 증명은 내보내져 그 어떤 구현체로도 검증될 수 있습니다. 우리는 커널 구현들 사이에서 증명을 교차 검증하는 도구인 Comparator를 만들었습니다. 누구나 자신만의 커널을 만들고 arena.lean-lang.org에 제출할 수 있습니다.
이것이 여러분에게 주는 것은 두려움 없이 해킹할 수 있는 자유입니다. 과감한 메타프로그램을 만드십시오. 자신도 거의 이해하지 못하는 방식으로 목표를 다시 쓰는 커스텀 tactics를 작성하십시오. 그래도 마지막에는 커널이 모든 것을 검사합니다. 여러분의 증명이 타입 검사를 통과하면, 그것은 올바릅니다. 통과하지 못하면 즉시 오류를 받습니다. 다른 도구들에서 건전성 문제로 고생했던 사용자들이 Lean으로 오는 이유는 커널이 실수를 잡아내기 때문입니다. 언제나 그렇습니다.
Terence Tao의 지적은 RL이 검증 파이프라인의 모든 뒷문을 찾아낼 것이므로 그런 뒷문이 있어서는 안 된다는 것입니다. "reinforcement learning is just so good at finding these backdoors." 커널의 건전성은 단지 이론적인 성질이 아닙니다. 그것은 AI 안전 인프라입니다.
하위 호환성입니다. 우리는 무언가를 깨뜨립니다. 그리고 그것을 의도적으로 합니다. 제대로 되지 않은 인터페이스의 안정성보다 확장성이 더 중요하기 때문입니다. 여러분이 2년 전에 Lean 코드를 작성했다면, 오늘날에는 수정 없이 컴파일되지 않을 가능성이 큽니다. 이것은 실제 비용이며, 우리는 그렇지 않은 척하지 않습니다.
2020년에 작성한 코드가 2026년에도 수정 없이 그대로 컴파일되는 시스템이 필요하다면, Lean은 그런 시스템이 아닙니다.
제가 Lean을 시작했을 때, 저는 HOL(higher-order logic)을 사용하고 싶었습니다. Jeremy Avigad와 저는 이 문제를 두고 여러 차례 의견을 주고받았습니다(그는 아직도 그 메시지들을 가지고 있고, 그 안에는 제가 dependent type theory에 강하게 반대하는 모습이 남아 있습니다). Higher-order logic은 자동화하기 더 단순하고, 커널은 훨씬 더 작을 수도 있습니다. 저는 복잡성을 싫어합니다.
하지만 dependent type theory는 사용자에게 필요한 것이었습니다. 프로젝트 초기에 constructivism의 아름다움을 느꼈고 그것을 배우는 일도 즐거웠지만, 그것은 실용적이지 않습니다. Aeneas 팀이 무엇이 느린지 말해 주면, 여러분은 그것을 고칩니다. 소프트웨어 검증 팀이 여러분의 tactics가 어떻게 확장되어야 하는지 설명해 주면, 여러분은 재설계합니다.
저는 더 순수한 시스템을 만들 수도 있었습니다. 대신 유용한 시스템을 만들었습니다.
Leonardo de Moura
AWS의 Senior Principal Applied Scientist
Lean FRO의 Chief Architect 겸 공동 창립자
