소개Rosen 교재 전 범위를 Lean4 증명으로 연습할 수 있는 AI 튜터를 Google Gemini의 Gem 기능으로 만들었습니다. 별도의 서버나 코딩 없이, 프롬프트 하나로 동작하는 소크라테스식 튜터링 시스템입니다.이 글에서는 구축 과정과 운영 노하우를 공유합니다.전체 구조20단원 (Rosen 챕터 기반) └ 20레벨 (난이도 상승) └ 5스캐폴딩 (도움 수준 조절)20단원Rosen의 「Discrete Mathematics and Its Applications」를 기준으로 논리, 집합, 수론, 귀납법, 조합론, 관계, 그래프 이론까지 전 범위를 20개 단원으로 나눴습니다.20레벨(난이도)각 단원 안에서 레벨 1~20으로 올라가며 난이도가 상승합니다.레벨 난이도 성격1~4워밍업단일 tactic,..