BEmYaOtNhDeER/math-book-notion-lean

math-book-notion-lean은(는) 무엇을 하나요?

Codex 스킬: 수학 서적의 Notion 노트 작성 및 Lean 형식화

개요

이 스킬은 Codex(예: Cursor, Codex CLI) 환경에서 수학 서적을 공부하거나 Lean 형식화를 수행할 때 사용합니다. 주요 기능은 다음과 같습니다:

• Notion 데이터베이스에 수학적 정의, 정리, 증명을 구조화된 노트로 저장
• Lean 코드 블록을 통해 정리와 증명을 형식화하고 검증
• Notion과 Lean 파일 간의 참조 연결 유지

사용 방법

1. Notion 통합 설정: Notion API 키와 데이터베이스 ID를 환경 변수로 설정합니다.

   export NOTION_API_KEY="your_notion_api_key"
   export NOTION_DATABASE_ID="your_database_id"
   

2. Lean 환경 설정: Lean 4가 설치되어 있어야 하며, lake 프로젝트가 초기화되어 있어야 합니다.

3. 스킬 호출: Codex 명령어를 통해 노트 작성 또는 형식화를 요청합니다.

   • 예: @math-book-notion-lean 정리 3.1을 Notion에 저장하고 Lean으로 증명해줘

지원 기능

• 노트 생성: 수학 정리, 정의, 증명을 마크다운 형식으로 Notion 페이지에 추가합니다.
• Lean 형식화: 주어진 수학 내용을 Lean theorem, def, lemma로 변환하여 .lean 파일에 저장합니다.
• 양방향 참조: Notion 페이지 링크를 Lean 주석에 포함하거나, Lean 코드 블록을 Notion 노트에 포함할 수 있습니다.

예시

Notion 노트 예시

# 정리 3.1: 피타고라스 정리
- 직각삼각형에서 빗변의 제곱은 다른 두 변의 제곱의 합과 같다.
- 증명: ...

Lean 코드 예시

theorem pythagorean (a b c : ℝ) (h : a^2 + b^2 = c^2) : a^2 + b^2 = c^2 :=
by
  rfl

주의 사항

• Notion API와 Lean 환경이 사전에 구성되어 있어야 합니다.
• Lean 형식화는 수학적 정확성을 보장하지 않으며, 사용자 검증이 필요합니다.

관련 리소스

• Notion API 문서
• Lean 4 공식 문서