Lean으로 수학 증명을 작성하는 방법: 소프트웨어 엔지니어를 위한 안내
Anatomy of a Lean proof for software engineers
소프트웨어 엔지니어가 Lean 정리 증명기를 사용해 형식 증명을 작성하는 과정을 설명한다. 계산 이론 문제를 예로 들어 DFA를 구성하고, 덧셈기의 상태 전이를 정의한 뒤, Mathlib의 정리를 활용해 정규 언어의 역폐쇄성을 증명한다. 형식 증명이 프로그램 검증과 어떻게 연결되는지, 그리고 실제 증명 코드가 어떻게 구성되는지 보여준다.
“형식 증명을 마친 후, 나는 이것이 소프트웨어 엔지니어들에게 시스템의 속성을 형식적으로 증명하는 데 무엇이 필요한지에 대한 좋은 통찰을 제공한다고 생각했기 때문에 글을 쓰기로 결정했다.”