안녕하세요? 저는 수학 교육용 게임을 개발하고자 프로그래밍을 배우고 있는 예비 창업자이고, 이름은 차불휘입니다.
정보통신산업진흥원 산하에 있는 오픈소스 소프트웨어 통합지원센터(오픈업) 에서 2024 오픈소스 컨트리뷰션 아카데미(OSSCA) 의 2차 체험형 프로그램을 9월부터 10월까지 운영할 예정입니다.
이번에 드디어 저도 컨트리뷰션 아카데미의 멘토로 뽑혔습니다. 저는 멘티분들에게 린 정리 증명기를 가르치면서 자연수 게임 을 멘티분들과 함께 한국어로 번역할 계획입니다.
[2024 OSSCA_체험형 2차_멘티 모집_공고문]
위의 링크에서도 확인하실 수 있는 제 프로젝트 'Git 활용 및 Lean'의 안내문을 아래에 옮겨 적었습니다.
제가 올해 가을에 진행한 린(Lean) 멘토링 프로그램의 공식 기간은 지났지만, 현재 멘티 세 분이 린 정리 증명기의 이용법을 계속 배우고 계세요. 새해부터 "린 4로 하는 정리 증명(Theorem Proving in Lean 4)" 교재로 린을 학습하려는 분을 추가로 모집합니다.
수학 인공 지능 의 개발이나 수학의 형식화에 관심 있는 수학 전공자, 형식 철학 에 관심 있는 철학 전공자 그리고 소프트웨어 검증에 관심 있는 프로그래머를 비롯한 여러분의 많은 참여를 바랍니다.
학습 모임의 진행 방식은 간단해요. 제 유튜브 채널이나 네이버 치지직 채널에 있는 린 교재 해설 영상을 보신 뒤, 제가 만든 퀴즈 와 린 교재 연습 문제의 답안을 제게 제출하시면 됩니다. 영상이 너무 많은 게 흠이지만요.
린을 배우다가 궁금한 점이 생기면, 이규환 수학 교수님이 개설하신 린 한국 줄립 챗 에서 저나 다른 분에게 질문해 주세요. 원하시면 화상 통화도 할게요.
2개의 좋아요
린 한국 줄립 챗에 가입하려면 초대 링크를 받아야 한다고 들었습니다. 링크를 원하시는 분은 제게 알려 주세요.
Lunah
2월 10, 2025, 9:27오후
3
안녕하세요. guuoul000@gmail.com 으로 주소 주시면 감사하겠습니다. 제가 당장 시간 상의 어려움으로 참가는 어렵겠지만, 현재 자연과학대 학부 재학생들 중 이런 강좌를 원하는 학생들에 전달은 가능할 듯 해서요. 그럼 답변 기다리겠습니다. 다시 한 번 글 남겨주셔서 감사합니다. 늦었지만 새해 복 많이 받으시구요.
1개의 좋아요