제가 올해 가을에 진행한 린(Lean) 멘토링 프로그램의 공식 기간은 지났지만, 현재 멘티 세 분이 린 정리 증명기의 이용법을 계속 배우고 계세요. 새해부터 "린 4로 하는 정리 증명(Theorem Proving in Lean 4)" 교재로 린을 학습하려는 분을 추가로 모집합니다.
수학 인공 지능의 개발이나 수학의 형식화에 관심 있는 수학 전공자, 형식 철학에 관심 있는 철학 전공자 그리고 소프트웨어 검증에 관심 있는 프로그래머를 비롯한 여러분의 많은 참여를 바랍니다.
학습 모임의 진행 방식은 간단해요. 제 유튜브 채널이나 네이버 치지직 채널에 있는 린 교재 해설 영상을 보신 뒤, 제가 만든 퀴즈와 린 교재 연습 문제의 답안을 제게 제출하시면 됩니다. 영상이 너무 많은 게 흠이지만요.
린을 배우다가 궁금한 점이 생기면, 이규환 수학 교수님이 개설하신 린 한국 줄립 챗에서 저나 다른 분에게 질문해 주세요. 원하시면 화상 통화도 할게요.
2개의 좋아요
린 한국 줄립 챗에 가입하려면 초대 링크를 받아야 한다고 들었습니다. 링크를 원하시는 분은 제게 알려 주세요.