Lean4

타입 이론과 커리-하워드 동형대응: 명제=타입, 증명=프로그램의 심오한 조화