• 제나 프로젝트: https://xenaproject.wordpress.com/
• 제나 프로젝트 유튜브 채널: https://www.youtube.com/channel/UCtdYf-CsDI215SqaQ3XYx1A/
• 2022년 수학 형식화하기 임피리얼 강좌: https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Formalising.20Mathematics.202022.20Imperial.20course/near/279388036
제나 프로젝트(Xena Project)는 임피리얼 칼리지 런던(Imperial College London)의 케빈 버저드(Kevin Buzzard) 교수님이 학생들과 함께 진행하는 '증명 보조기 린(Lean)으로 수학 형식화하기' 프로젝트예요. 해당 유튜브 채널의 재생 목록 가운데 '런던 린 배우기(London Learning Lean)'는 상급 학부, 석사, 연구 수준의 수학을 다루는 세미나이고, '2022년 수학 형식화하기[Formalising Mathematics 2022]'는 올해 학부생과 석사 과정생을 대상으로 진행한 강좌입니다. 이 대학은 학사 과정이 3년제이니 아마 4학년이 석사 과정생인 듯해요.
학생들이 직접 형식화한 주제에는 정수론, 힐베르트 공간, 범주론, 그래프 이론, 람다 계산 등이 있었다는군요. 이 강좌는 시험을 치르지 않은 대신에 각 학생의 세 가지 프로젝트를 평가했어요. 1학년 때 배운 것, 2학년 때 배운 것, 올해 배운 것을 형식화한 프로젝트에 각각 20%, 30%, 50%의 비중을 두고 성적을 매겼다고 하네요.
