오픈소스 컨트리뷰션에서 lean 언어를 배우고, 현재까지 스터디를 진행하고 있다. 내가 이 언어에 대해 흥미를 가지게 된 과정을 기록하고, lean 언어에 대해 정리해놓으려 한다.
1. lean?
2. lean 언어의 사용 용도
3. 나는 왜 lean을 공부하게 되었을까?
4. lean 학습 자료
5. 후기
1. lean?
lean은 대화형 방식을 사용해 수학적 정리를 증명하는 정리 증명기이자, 실제로 실행 가능한 프로그램을 작성가능한 함수형 프로그래밍 언어이다.
2. lean 언어의 사용 용도
주로 수학계의 문제 해결, 특정 문제에 대한 검증, 수학적 논리 학습 등에 사용한다.
* Liquid Tensor Experiment
= lean을 사용해 Condensed Mathematics(응집 수학)의 불완전한 부분을 증명해냈다.
링크 : https://www.youtube.com/@leanprovercommunity5485/videos (프로젝트 공식 깃허브)
https://www.nature.com/articles/d41586-021-01627-2 (nature 기사)
* 구글 딥마인드의 AlphaProof
= 국제수학올림피아드 문제를 푸는 ai인 AlphaProof에서 답을 도출하는 증명 엔진에 사용되었다.
링크 : https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/ (google deepmind 블로그)
* 수학 라이브러리 mathlib
= ai 모델이 수학적 논리를 학습할 때 사용하는 수학 라이브러리로, lean으로 정리되어 있다.
* 자연수 게임을 활용한 교육의 게임화
= 덧셈, 곱셈의 성질을 증명하는 자연수 게임을 구성했다.
링크 : https://adam.math.hhu.de (플레이 사이트)
그 외에도 현재 aws에서 클라우드 인프라 검증 도구로써의 가능성을 연구하고 있다.
3. 나는 왜 lean을 공부하게 되었을까?
처음 프로그램에 참여를 지원할 때는 처음 보는 언어라는 흥미때문에 시작하게 되었다. 하지만 내가 이전에 사용하던 c#, cpp와 사고를 다르게 한다는 느낌을 받았다. c#, cpp은 코드를 과정을 순서대로 작성한다면, lean은 해당 문제의 논리를 증명하고, 작성한 코드들의 관계를 이해하는 게 더 핵심이 되었다. 그리고 c계열 언어들은 내가 코드를 작성하면서 발생할 수 있는 예외 상황을 미리 고민한다면 lean은 해당 코드라는 사실을 현재 존재하는 코드의 증명에 적합한 근거가 되는가?에 대한 고민을 하게 되었다.
그래서 증명하는 과정이 재밌어서 계속 하다보니 프로그램이 끝나도 계속 해당 언어를 배우게 되었다.
4. lean 학습 자료
4.1) 공식 교재
https://lean-lang.org/theorem_proving_in_lean4/
lean 커뮤니티에서 정리한 공식 자료 링크이다. 필자는 해당 자료를 기반으로 공부하고 있다.
4.2) 웹사이트
2.1) lean 공식 사이트
위 사이트에 설치 방법, 문서, 블로그, 논문 등 전반적인 자료를 확인할 수 있다.
4.2.2) lean community
https://leanprover-community.github.io
lean 공식 커뮤니티 사이트로 라이브러리, 적용되는 수학적 정리, 개발에 기여하는 방법이 소개되어 있다.
4.2.3) lean zulip chat
https://leanprover.zulipchat.com
slack 형태로 이루어진 커뮤니티 사이트로, 채팅을 통해 핵심 개발진과 공식적으로 소통할 수 있다.
4.3) 유튜브
4.3.1) lean community
https://www.youtube.com/@leanprovercommunity5485/videos
린 커뮤니티 채널로, 유튜브를 통해 증명 과정을 확인할 수 있다.
4.3.2) 한국어 lean 교재 해설
https://www.youtube.com/watch?v=dYOpahCit2s&list=PLOj4iIbJ1k6YH4A_qxeJPQa-bPHT0fM7x
4.1을 한국어로 해설한 내용으로, 교재에 대해 자세한 설명이 되어있어서 교재를 공부하다가 어려운 부분이 있으면 참고하기 좋다.
5. 후기
글을 작성해보니 lean이 활용되는 산업군에 대해 자세히 알게 되었고, 내가 lean을 사용할 때 다른 프로그래밍 언어와 다르다고 느낀 부분에 대해 명확히 알게 되었다. 이 글을 읽은 사람들이 lean 언어에 대해 알게 되고, 궁금증을 갖게 되길 바란다.