소개
Rosen 교재 전 범위를 Lean4 증명으로 연습할 수 있는 AI 튜터를 Google Gemini의 Gem 기능으로 만들었습니다. 별도의 서버나 코딩 없이, 프롬프트 하나로 동작하는 소크라테스식 튜터링 시스템입니다.
이 글에서는 구축 과정과 운영 노하우를 공유합니다.
전체 구조
20단원 (Rosen 챕터 기반)
└ 20레벨 (난이도 상승)
└ 5스캐폴딩 (도움 수준 조절)
20단원
Rosen의 「Discrete Mathematics and Its Applications」를 기준으로 논리, 집합, 수론, 귀납법, 조합론, 관계, 그래프 이론까지 전 범위를 20개 단원으로 나눴습니다.
20레벨(난이도)
각 단원 안에서 레벨 1~20으로 올라가며 난이도가 상승합니다.
레벨 난이도 성격
| 1~4 | 워밍업 | 단일 tactic, 기본 문법 |
| 5~8 | 기본 | 2~3 tactic 조합, Rosen 예제 수준 |
| 9~12 | 응용 | 전략적 조합, 연습문제 수준 |
| 13~16 | 심화 | 복합 증명, 보조 정리 활용 |
| 17~19 | 고급 | 여러 정리 결합, 창의적 접근 |
| 20 | 보스 | 단원 전체 통합 종합 증명 |
5단계 스캐폴딩
각 레벨에서 도움의 양을 5단계로 조절합니다.
단계 이름 제공되는 것
| S1 | 유사 예제 따라하기 | 모범 코드 + 유사 문제 |
| S2 | 빈칸 채우기 | 거의 완성된 코드, 핵심 1~3곳만 빈칸 |
| S3 | sorry 뼈대 | 구조 + import + sorry |
| S4 | sorry만 | 정리 선언 + sorry 한 줄 |
| S5 | 완전 자력 | 수학적 서술만, 코드 없음 |
핵심 설계 원칙
소크라테스식 디버깅
AI가 답을 바로 주지 않고 질문으로 유도합니다. 예를 들어 학생이 Type mismatch 에러를 보여주면, "이 에러가 난 이유는 A와 B 사이에 논리적 비약이 있기 때문입니다. 어떤 tactic으로 이 틈을 메울 수 있을까요?"라고 물어봅니다.
단, 학생이 계속 막히면 점진적으로 구체적인 힌트를 제공하고, 최종적으로는 정답과 줄별 해설을 줍니다. 좌절시키지 않는 것이 중요합니다.
자동 승급/강등
3문제 연속 정답이면 다음 스캐폴딩(또는 레벨)으로 승급을 제안하고, 3문제 연속 오답이면 이전 스캐폴딩으로 자동 강등합니다. 학생의 실력에 맞춰 난이도가 자동 조정되는 적응형 학습입니다.
자유 이동
학생이 지루해하지 않도록, 언제든 다른 단원, 다른 레벨, 다른 스캐폴딩으로 자유롭게 이동할 수 있게 했습니다. "단원 ⑤로", "레벨 10으로", "S3으로" 같은 자연어 명령을 지원합니다.
저장 코드
Gem은 대화가 끝나면 진행 상황이 사라지는 한계가 있습니다. 이를 해결하기 위해 U3-L8-S3-streak1 형태의 저장 코드를 도입했습니다. 학생이 "저장"이라고 입력하면 현재 상태가 코드로 발급되고, 다음 접속 시 코드를 붙여넣으면 이어서 진행합니다.
Gem 등록 방법
- https://gemini.google.com 접속, Google 계정으로 로그인
- 왼쪽 메뉴에서 "Gem 관리자"(Gem Manager) 클릭
- "새 Gem 만들기"(New Gem) 클릭
- 이름, 설명을 입력하고, "지침"(Instructions) 칸에 시스템 프롬프트를 붙여넣기
- 저장 후 "공유" 버튼으로 링크 생성
- 학생들에게 링크 배포
시스템 프롬프트는 직접 설계하셔야 합니다. 위의 구조(단원/레벨/스캐폴딩)와 설계 원칙을 참고하여 본인 수업에 맞게 작성하시면 됩니다.
비용
항목 비용
| Gem 호스팅 | 무료(Google Gemini 내장) |
| Gemini 무료 플랜 | 무료(일일 사용량 제한 있음) |
| Gemini Advanced | 월 $20/인(무제한, 더 좋은 모델) |
학생이 각자 Gemini 계정을 사용하므로 교수자에게 API 비용이 발생하지 않습니다.
학생 진행 관리
Google Sheets 활용
학생들에게 주기적으로 저장 코드를 제출하게 하면 진행 상황을 파악할 수 있습니다.
학번 이름 저장 코드 단원 레벨 스캐폴딩 제출일
| 2024001 | 김OO | U3-L8-S3-streak1 | 증명 방법론 | 8 | S3 | 3/15 |
| 2024002 | 이OO | U5-L12-S2-miss1 | 집합론 | 12 | S2 | 3/15 |
Google Forms로 제출 폼을 만들면 Sheets에 자동 기록됩니다.
과제 활용 예시
- "이번 주까지 단원 1~4에서 레벨 5 이상 도달하세요. 저장 코드를 제출하세요."
- "중간고사 전까지 단원 1~10 레벨 10 이상 달성"
- "기말 프로젝트: 단원 20 보스 문제 풀이 제출"
운영 시 주의사항
AI의 Lean4 코드가 항상 정확하지는 않습니다. 학생들에게 반드시 실제 Lean4 환경(VS Code + Lean4 확장)에서 코드를 실행해서 검증하라고 안내하는 것이 좋습니다. AI 튜터는 사고 과정을 훈련하는 도구이지, Lean4 컴파일러를 대체하는 것이 아닙니다.
Gem의 한계를 인지하세요. 대화가 길어지면 앞부분 맥락을 잊을 수 있고, 저장 코드도 학생이 직접 관리해야 합니다. 본격적으로 운영하려면 웹앱(로그인 + DB)으로 업그레이드하는 것을 고려할 수 있습니다.
Rosen 교재 PDF를 Gem에 넣을 필요는 없습니다. Gemini가 Rosen 교재 내용을 이미 학습 데이터로 알고 있습니다. 다만 Lean4의 Mathlib 라이브러리 관련 참고 자료가 있으면 정확도가 올라갑니다.
향후 업그레이드 방향
Gem으로 시작한 뒤, 필요에 따라 다음 단계로 확장할 수 있습니다.
- 웹앱 배포: Google 로그인 + 자동 진행 저장 + 대시보드
- Lean4 실시간 검증 연동: 학생 코드를 실제 Lean4 서버에서 실행하여 정답 여부를 자동 판별
- 학습 분석: 단원별/레벨별 정답률, 취약 tactic 분석, 학생 간 비교
Gem은 MVP(최소 기능 제품)로서 빠르게 시작하고, 학생 반응을 보면서 점진적으로 발전시키는 접근이 가장 현실적입니다.
'IT잡동사니좌충우돌경험기' 카테고리의 다른 글
| 오픈 카카오톡 개인 채팅만들기 (0) | 2026.05.17 |
|---|---|
| 글쓰기 루틴 만들기: 생명줄 같았던 아침 1시간을 블로그에 투자해봤다 (0) | 2025.07.03 |
| 나만의 다락방이 된 내 블로그 (0) | 2025.07.03 |
| AI 글처럼 보이지 않게 쓰는 법: 블로그 초보가 자주 하는 5가지 실수 (0) | 2025.07.03 |
| AI가 쓰는 글과 내가 쓰는 글의 콜라보 (2) | 2025.07.03 |