테렌스 타오, 코딩 에이전트로 논리 퍼즐 게임 'Lean Grimoire' 재구축
테렌스 타오가 2018년 JavaScript로 만든 대화형 논리 교재 'QED'를 코딩 에이전트로 다시 만들었다. 명제 논리와 1차 논리를 '제작 게임' 방식으로 익히는 이 게임은 이제 진행 중인 Lean 증명을 화면에 보여주는 기능을 갖췄고, 수학 명제는 '물약', 수학 표현식은 '두루마리'로 표현되는 판타지 모드도 추가됐다. 그는 논리 증명과 Lean 교육 도구로서의 유용성을 높이기 위한 플레이 테스트 참가자를 찾고 있다.
재미 삼아 '판타지 모드'로 플레이하는 옵션도 추가했는데, 여기서는 여러 게임 요소가 판타지 분위기의 문구로 묘사된다. 예를 들어 수학적 명제는 '물약'이 되고, 수학적 표현식은 '두루마리'가 되는 식이다.
HN 토론
11- torben-friis
정말 엉망인 교육용 게임이네요.
이렇게 부정적으로 말해서 죄송하지만, LLM스러운 도입부는 겨우겨우 읽을 수 있는 수준이고, 그 조작 방식이라는 것도 미완성된 개인 obsidian 문서 같아 보입니다.
tao가 만들었다고 생각하면 좀 이상하네요. 그의 수학 노트는 꽤 접근하기 쉽고 잘 쓰여 있었던 걸로 기억하는데.