증명 보조기 학습 모임을 구상하고 있어요

올빼미의 일상
1

증명 보조기 학습 모임에 대한 구상

증명 보조기를 이용해 수학·논리학·이론 컴퓨터 과학·철학을 비롯한 여러 분야의 이론을 배우거나 형식화하고 싶은 분들을 위해 나중에 학습 모임을 운영하고자 합니다. 가능하면 추가로 교육 영상도 제작하고 인터넷 방송도 하고 싶어요.

아쉽게도 현재로서는 고교·대학 수준의 논리학을 모르는 초보자가 증명 보조기와 논리학을 동시에 배울 수 있는 학습 자료가 없는 듯해요. 간단히 말해, 쉬운 교재가 없습니다.

제가 구상한 학습 모임은 다음과 같습니다. 아래의 내용은 나중에 바뀔 수 있으며, 아직 참가자를 모집하는 것이 아닙니다. 본격적으로 학습 모임을 시작하기 전에 음성 및 영상 편집을 더 배우고 싶어요.

호모토피 유형론 배우기

이용할 증명 보조기와 라이브러리

  • 코크(Coq) 증명 보조기
  • Coq-HoTT: 호모토피 유형론[HoTT]을 위한 코크 라이브러리

읽을 자료

참고 사항

  • 호모토피 유형론 교재의 연습 문제를 푸는 데 코크를 이용할 계획입니다.
  • 저를 포함한 모임 참여자는 "소프트웨어 기초론" 1권을 먼저 읽어서 코크를 익혀야 합니다.

안셀무스의 신 존재 증명 형식화하기

이용할 증명 보조기와 라이브러리

읽을 자료

참고 사항

  • 이저벨로 작성한 형식화 코드를 린으로 옮길 계획입니다.
  • 모임 참여자는 이저벨만 배울 수도 있습니다. 이럴 분들은 형식화 코드를 린으로 옮기는 일에 참여하지 않을 것입니다.
4개의 좋아요
2

사실 @chabulhwi 님의 글을 꾸준히 봐왔지만 전혀 무슨 내용인지 이해가 안가는(ㅠㅠ) 내용들도 많아 속상했는데, 이런 모임을 생각하고 계신다니 기대됩니다! 말씀하신대로 막상 증명 보조기... 린... 등등 계시글에 올라온 내용들 중 생소한 내용들을 더 알아보려 할때마다 깔끔하게 정리된 자료가 없어 찾아보기 어려웠는데, 좋은 기회인것 같습니다!

2개의 좋아요
3

입문자에게 최소한의 배경지식과 숙련도만 요구하면서 증명 보조기를 활용하는 학습 자료를 만드는 것이 궁극의 목표입니다. 아직 그런 자료가 없다 보니 입문자가 증명 보조기를 배우기가 어렵다고 생각해 왔습니다.

그리고 증명 보조기를 이용하려는 입문자는 소프트웨어 관리를 위한 여러 프로그램도 함께 배워야 되고, 이 점이 입문자에게 큰 부담이 될 듯해요. 텍스트 편집기는 비교적 이용하기 쉬운 비주얼 스튜디오 코드(VS Code)를 고르면 되지만, 깃(Git) 버전 관리 시스템이 좀 다루기 어렵습니다.

불행인지 다행인지는 모르겠지만, 제가 지난해 12월부터 시작한 문자열 정리 증명을 계속 진행할 필요가 없어져서 린 학습 자료를 한국어로 번역할 시간이 생겼어요. 저는 오늘부터 음성 및 영상 편집, 프로그래밍, 교재 번역에 몰두하려고 합니다.

1개의 좋아요
4

흥미롭네요.

최근 New Foundations (정확히는 NFU)의 consistency를 LEAN을 통해 증명하여 화제(??)가 되고있는 듯 하여 증명보조기에 대한 관심이 많은 듯 합니다.

좋은 계획입니다. 많은 분들이 참여해주시면 좋겠네요.

3개의 좋아요