Skip to content

Latest commit

 

History

History
163 lines (123 loc) · 7.56 KB

leanprover-mentorship.md

File metadata and controls

163 lines (123 loc) · 7.56 KB
Raw

깃 버전 관리 시스템과 린 정리 증명기

프로젝트 개요

  • 프로젝트명: Git 활용 및 Lean
  • 프로젝트 분야: 깃 심화, 정리 증명
  • 활용 기술: 깃(Git), 린(Lean)
  • 프로젝트 난이도: ★★★★★(매우 어려움)

활용 언어: 린

프로젝트 소개

린 정리 증명기

  • 린(Lean): 상호 작용 정리 증명기 겸 순수 함수형 프로그래밍 언어
    • 상호 작용 정리 증명기: 사람이 형식 증명을 작성하도록 돕는 컴퓨터 프로그램
    • 형식 증명: 증명 검증기라는 컴퓨터 프로그램으로 검증할 수 있는 증명
  • 린의 활용
    • 형식 검증: 컴퓨터 프로그램이 그 명세에 맞게 동작함을 증명하기
    • 수학 인공 지능의 개발: 린이 검증할 수 있는 수학 증명을 생성하는 언어 모형 만들기
    • 학술 이론의 형식화: 수학·컴퓨터 과학·물리학·철학 이론을 재서술하고 검증하기

증명 지향 프로그래밍

  • 증명 지향 프로그래밍: 개발자가 프로그램과 증명을 함께 설계해 프로그램 동작의 여러 측면을 수학적으로 보장하는 패러다임
    • 기능 정확성: 프로그램이 입력값마다 명세에 맞는 출력값을 산출하는 성질
    • 보안 성질: 프로그램이 특정 비밀을 절대로 유출하지 않는 성질
    • 그 밖의 성질: 자원 이용의 한계에 관한 성질 등
  • 증명 지향 프로그래밍 언어: F*, 다프니(Dafny) 등
    • 라이브러리와 도구가 충분히 개발되고 나면, 린으로 증명 지향 프로그래밍을 하기가 지금보다 수월할 것임.

린의 활용 사례 1: 시더

린의 활용 사례 2: 샘프서트

  • 샘프서트(SampCert): 차등 프라이버시를 위한 이산 가우스 샘플러
    • 린과 그 수학 라이브러리 매스리브(Mathlib)를 이용해 검증한 구현물임.
    • 린으로 작성한 이 구현물은 계산 가능하지 않지만, 린 코드에서 다프니 코드를 추출할 수 있음.
  • 다프니-VMC: 검증된 몬테카를로 알로리듬을 위한 다프니 라이브러리
    • 샘프서트 코드에서 추출한 다프니 코드가 이 라이브러리에 포함돼 있음.
  • 참고 자료

린의 활용 사례 3: 구글 딥마인드의 알파푸르프

컨트리뷰션 운영 방안

활동 목표

  • 프로젝트 관리
    • 깃(Git) 버전 관리 시스템으로 프로젝트 관리하기
    • 깃허브(GitHub)에서 프로젝트 개발에 기여하기
  • 정리 증명
    • "린 4로 하는 정리 증명" 교재의 연습 문제 다 풀기
    • 자연수 게임 한국어로 번역하기

첫째 주(9월 9~15일)

  • "린 4로 하는 정리 증명" 교재: 1~3장 읽기, 3장 연습 문제 풀기
  • 프로젝트 관리: 자신의 연습 문제 풀이를 모은 깃 저장소를 만들고 깃허브에서 공유하기

둘째 주(9월 16~22일)

  • 추석 연휴: 16~18일
  • "린 4로 하는 정리 증명" 교재: 4장 읽고 연습 문제 풀기
  • 프로젝트 관리: 매깃(Magit) 등의 이용자 친화적인 깃 인터페이스로 커밋 이력 관리하기

셋째 주(9월 23~29일)

  • "린 4로 하는 정리 증명" 교재: 5~6장 읽기, 5장 연습 문제 풀기
  • 프로젝트 관리: 오메가T를 이용해 프로젝트 번역하기
  • 자연수 게임: 튜토리얼·덧셈 세계 번역하기

넷째 주(9월 30일~10월 6일)

  • "린 4로 하는 정리 증명" 교재: 7~8장 읽고 연습 문제 풀기
  • 프로젝트 관리: 연습 삼아 풀 요청하기(PR)
  • 자연수 게임: 곱셈·거듭제곱 세계 번역하기

다섯째 주(10월 7~13일)

  • "린 4로 하는 정리 증명" 교재: 9~11장 읽기
  • 프로젝트 관리: 연습 삼아 풀 요청 병합하기
  • 자연수 게임: 함의·알고리듬 세계 번역하기

여섯째 주(10월 14~20일)

  • "린 4로 하는 정리 증명" 교재: 12장 읽기
  • 프로젝트 관리: 린 웹 게임 관리자에게 풀 요청하기
  • 자연수 게임: 상급 덧셈·부등식 세계 번역하기

남은 5일(10월 21~25일)

  • "린 4로 하는 정리 증명" 교재: 복습하기
  • 프로젝트 관리: 자신이 만든 저장소 정돈하기
  • 자연수 게임: 상급 곱셈 세계 번역하기

학습 모임

  • 매주 최소 2회, 매회 최소 2시간 진행할 듯합니다.
  • 아마 대면 모임에서는 주로 제가 멘토분들에게 기술 지원을 할 듯합니다.

"린 4로 하는 정리 증명" 교재의 난이도

  • 6주 동안 "린 4로 하는 정리 증명" 교재를 완독하고 모든 연습 문제를 푸신 멘티분은 저보다 학습 속도가 7배 이상 빠릅니다.
  • 제가 다른 자료를 참고하면서 이 교재를 찬찬히 읽었다는 점을 감안하면, 멘티분들이 저보다 적어도 3배 빨리 이 교재를 읽고 연습 문제를 풀어내실 수 있을 듯합니다.
  • 멘티분들이 이 교재를 7장까지 읽고 연습 문제를 다 푸시기만 해도 이 체험형 프로젝트는 성공한 셈입니다.

린에 관한 첨언

  • 제가 멘티분들에게 가르칠 다음 개념은 린의 이용법을 이해하는 데 꼭 필요합니다.
    • 명제 논리: 논리 연결어(부정, 논리곱, 논리합, 함의, 동등)
    • 술어 논리: 양화사(보편 양화사, 존재 양화사)
  • 자연수 게임
    • 수학적 귀납법에 대한 배경지식이 필요합니다.
    • 한국어로 번역할 텍스트가 그리 많지는 않습니다.

멘토 소개: 차불휘(Bulhwi Cha)

  • 2024년 6~7월: 시네레라 GG 인피니티 문서 개정 기여
  • 2024년 1~6월: 린 배터리 라이브러리 개발 기여
  • 2023년 4~8월
    • 매스리브 포팅 기여
    • 린 표준 라이브러리 개발 기여