세미나 심층 연구은(는) 무엇을 하나요?
한 편의 논문을 심층 연구하여 준비한 세미나 발표입니다. 먼저 에이전트는 증거에 기반한 대화형 토론을 통해 사용자가 논문을 선택하도록 돕습니다. 그런 다음 논문을 모든 주장에 검증 상태가 표시된 digest로 다시 작성합니다. 컴퓨터 대수 시스템(CAS)으로 계산을 재수행하고, Lean에서 논리를 형식화하며, 논문에서 발견한 내용을 기록합니다. 마지막으로 이 단일 진실 공급원에서 발표 자료를 구축합니다. 사용자가 결정하고, 에이전트는 증거를 제시하며 자신이 진술하는 모든 것을 확인합니다.
번들 파일은 이 스킬의 기본 디렉토리(스킬이 로드될 때 표시됨)를 기준으로 하며, 아래에서는 $SKILL이라고 합니다. 프로젝트 파일은 사용자의 프로젝트 디렉토리로 이동하며, 절대 $SKILL 안으로 들어가지 않습니다.
단계 및 읽을 사항
| 단계 | 먼저 읽을 것 | 남기는 것 |
|---|---|---|
| 0 접수 | references/intake.md | MEMORY.md의 답변, PLAN.md의 미결정 사항 |
| 1 주제 발굴 | references/ideation.md | 선택된 논문; 모든 후보는 JOURNAL.md에 |
| 2 출처, 스캐폴드, digest | references/digest.md | 저장소, source/SOURCE.md, 발견 등록부가 포함된 digest |
| 3 검증 | references/verification.md, references/lean-palomar.md, references/compute.md | CAS 기록, 수치 화면, Lean 라이브러리, 감사, 로그 |
| 4 자료 | references/materials.md, templates/briefs/ | 노트, 슬라이드, 칠판 계획, Verso 문서, 랜딩 페이지, 볼트 |
| 5 라이브 데모 | references/live-demo.md | 리허설된 데모 파일 및 대비책 |
| 6 문서화 | references/documentation.md | 저널, 계획, 메모리, 볼트 노트, 커밋 |
| 7 게시 | references/publishing.md | 없음(사용자가 이 세션에서 요청하지 않는 한) |
| 모든 단계 | references/traps.md | Lean, 클러스터, CAS 또는 사이트 작업 전에 읽을 것 |
| CS 논문 | references/computer-science.md | 1~5단계의 컴퓨터 과학 관점에서의 독서 |
단계는 메뉴이지, 강제적인 순서가 아닙니다. 읽기 전용 발표는 0~2단계와 필요한 자료만으로 충분합니다. 이미 논문을 가지고 온 사용자는 0단계에서 시작하여 1단계를 건너뜁니다.
원칙
- 사용자가 선택하고, 당신은 증거를 제시합니다. 논문, 깊이 또는 게시 대상을 조용히 결정하지 마십시오. 방향 전환("확신이 안 서요", "좀 더 최신 것이요")은 정상입니다: 이는 프로필을 세분화하는 것이므로, 마지막 제안을 방어하는 대신 새로운 라운드를 시작하십시오.
- 1차 출처만 사용합니다. 제목, 저자, 날짜, 버전, 페이지 수 및 코드 가용성을 출처에서 확인하십시오: arXiv 초록 페이지 또는 API, PDF 자체, 저장소. 회사나 언론의 발표는 주장으로 표시하십시오.
- 표시되는 모든 숫자는 기억된 것이 아니라 계산된 것입니다. 슬라이드, 페이지 및 노트의 숫자는 실행된 노트북, CAS 기록, Lean 출력 또는 빌드 로그에서 가져옵니다.
- 하나의 진실 공급원. digest는 수학적 진실의 근원입니다. 각 주장에는
[Lean],[CAS],[num],[exp]또는[paper]태그가 지정됩니다. 노트, 슬라이드, Verso 문서 및 페이지는 이것에서 파생되며 결코 모순되지 않습니다. - CAS는 찾고, 증명 보조자는 확인합니다. 인증서는 CAS 기록에서 생성기(
tools/cert2lean.py)를 통해 Lean으로 전달됩니다. 생성된 파일은 재구축되며, 수동으로 편집되지 않습니다. - 어렵지만 표준적인 사실은 명시적 가설이 되며, 공리가 아닙니다. 각각을 digest와 형식화 메타데이터에 기록하십시오.
- 발견 사항은 기본적으로 기밀입니다. 타인의 미게재 논문에 대한 발견 사항은 사용자가 결정할 때까지 프로젝트 내에 남아 있습니다. 실제 오류인 경우, 먼저 저자에게 알릴 것을 제안하십시오.
- 머신과 공유 리소스를 보호하십시오. 툴체인을 설치하기 전에 여유 디스크 공간을 확인하고,
MATHLIB_NO_CACHE_ON_UPDATE=1없이lake update를 실행하지 말며, 사용자의 다른 프로젝트 내부에서 빌드하지 마십시오.references/compute.md의 클러스터 에티켓을 따르십시오. - 파일당 한 명의 소유자. 각 하위 에이전트는 자신의 디렉토리만 작성합니다. 당신은 통합, 검토 및 커밋합니다.
- 외부 지향 작업은 현재 세션에서 명시적인 요청이 필요합니다. 여기에는 배포, 푸시, 원격 저장소 생성 및 아티팩트 게시가 포함됩니다. 비밀번호, 토큰, 개인 키를 어떤 파일에도 절대 작성하지 마십시오.
- 사용자의 전문 용어는 먼저 사용자의 파일에서 찾으십시오. 익숙하지 않은 용어("register class", 세미나 약어)는 종종 사용자의 노트나 프로젝트에 정의되어 있습니다. 거기서 검색하고, 그 다음 웹에서, 그 다음 질문하십시오.
0단계: 접수
먼저 읽기 전용으로 환경을 조사하여 질문이 구체적인 옵션을 제공할 수 있도록 하십시오. 여유 디스크 공간(df -h ~), 설치된 Lean 툴체인, 사용 가능한 CAS(로컬 또는 원격), Python 및 uv, 그리고 사용자가 복사할 형식으로 명명한 프로젝트를 확인하십시오. 그런 다음 질문 도구(Claude Code의 AskUserQuestion)를 사용하여 질문하십시오: 호출당 최대 4개의 질문, 각 질문당 2~4개의 옵션, 권장 옵션을 먼저 표시하고 "(권장)"이라고 표시하십시오. 질문 은행은 references/intake.md에 있습니다. 발표, 주제 및 깊이, CAS 및 컴퓨팅, 산출물, 대시보드 전달 방식(로컬 전용 또는 온라인, 위치, 지금 또는 나중), 그리고 git을 다룹니다. 사용자의 첫 메시지가 이미 답변한 내용은 건너뛰고 한 줄로 확인하십시오. 답변을 날짜가 있는 결정으로 MEMORY.md에 기록하고, 미해결 사항은 ❓로 PLAN.md에 기록하십시오.
1단계: 주제 발굴 (논문이 주어지지 않은 경우)
사용자가 선택할 때까지 라운드를 진행합니다(references/ideation.md):
- 사용자의 arXiv 기록(
tools/arxiv_scan.py author), 현재 프로젝트의 README 및 사용자가 말한 내용에서 관심 프로필을 구축합니다. 사용자가 수정할 수 있도록 세 줄로 표시합니다. - 병렬로 검색합니다: 뉴스 웹 검색; 카테고리 × 주제 × 최근성 기간에 대한 arXiv API(
tools/arxiv_scan.py scan, 이어서rank); GitHub API 및 스크래치패드의 얕은 클론을 통한 코드 저장소(Lean 코드의 경우tools/tactic_census.py). - 제시할 모든 후보(ID, 제목, 저자, 날짜, 버전, PDF 페이지, 코드 링크)를 확인합니다. 비용이 저렴할 때는 직접 화려한 주장을 재확인합니다.
- 최종 후보를 산문으로 제시합니다: 사용자와 형식에 적합한 이유와 함께 한 가지 추천, 장단점이 있는 두세 가지 대안, 필터 바로 바깥의 논문, 5분 가치가 있는 뉴스, 그리고 출처. 하나의 직접적인 질문으로 끝냅니다. 질문 도구는 명확한 최종 선택을 위한 편의 기능입니다. 사용자가 이를 거절하고 명확히 하려는 경우, 대화를 원하는 것이므로 무엇을 변경할지 물어보십시오.
- 모든 후보와 그 이유를 기록합니다. 스캐폴드 시간에
JOURNAL.md에 들어갑니다.
2단계: 출처, 스캐폴드, digest
PDF와 LaTeX 소스를 source/로 가져옵니다(git에서 무시됨). 버전과 SHA-256 체크섬을 source/SOURCE.md에 기록합니다. LaTeX에서 수식과 목록을 전사하며, PDF 텍스트 레이어에서는 절대 전사하지 않습니다. tools/scaffold.py로 프로젝트 스캐폴드를 생성합니다(문서 템플릿, digest, 선택적으로 Lean, CAS, 클러스터, 사이트, 슬라이드, 책, Verso 및 볼트 스켈레톤). 그런 다음 digest(templates/digest/digest.md)를 작성합니다: 세 줄의 결과, 배경, 설정, 정리별 섹션(증명 구조 및 상태 태그 포함), 발견 등록부(심각도: 확인됨 / 표현 / 암시적 가설 / 강화 / 오류), 연습 문제. 자세한 내용은 references/digest.md를 참조하십시오.
3단계: 검증
모든 계산적 주장과 모든 "하나를 확인한다"를 PLAN.md의 검증 표의 행으로 변환한 다음, 이를 통해 작업합니다:
- 먼저 수치 화면(고정밀도, 전사 오류를 잡아내지만 아무것도 증명하지 않음);
CHECK라인이 참이어야 하는 커밋된 기록이 있는 CAS 스크립트; 불일치는 발견 등록부로 이동합니다(references/verification.md);- 인증서: CAS는
CERT블록을 출력하고,tools/cert2lean.py는 Lean 파일을 작성하며,linear_combination또는ring이 각 항등식을 확인합니다.grind는 인증서 없이 동일한 단계를 재증명할 수 있으며, 이를 보여줄 가치가 있습니다. - Lean: 먼저 명제, 그 다음 증명; 경량 또는 Palomar 클래스(
Challenge.lean/Solution.lean/comparator.json, 표준 공리만,import all을 통한 공리 감사,lake comparator --paranoid, 경고 없는 빌드, 로그).references/lean-palomar.md및references/compute.md(로컬 대 클러스터 빌드 및 디스크 공간 규칙)를 참조하십시오.
린터 경고는 가능한 발견으로 취급하십시오: 사용되지 않은 인수는 정리가 논문에서 진술한 것보다 더 일반적으로 성립함을 의미할 수 있습니다.
4단계: 병렬 하위 에이전트에 의한 자료
산출물당 하나의 백그라운드 에이전트를 시작하고, 각각 자체 디렉토리를 소유합니다: CAS 재검증, Verso 문서, 노트(Jupyter Book), 칠판 계획이 포함된 슬라이드, 히어로 이미지와 볼트가 포함된 랜딩 페이지. templates/briefs/의 브리핑을 작성합니다. 각 브리핑은 진실 공급원(digest, Lean 파일, 기록), 명시할 수 있는 사실, 실행할 수 있는 명령, 절대 숫자, 이름, 시간 또는 방을 만들어내지 않아야 함을 지정합니다. 실행 중에도 계속 검증하십시오. 사실이 변경되면(새로운 결과, 새로운 개수, 새로운 데모) SendMessage를 통해 각 실행 중인 에이전트에게 짧고 독립적인 업데이트를 보냅니다: 변경된 사항, 위치, 추가할 사항, "선택 사항, 현재 계획 유지". 에이전트는 숫자를 재유도하므로, digest도 심사합니다: 불일치를 보고하도록 요청한 다음, digest를 수정하고(날짜 기입) 다른 에이전트에게 알립니다. 여러 에이전트가 실행되는 동안 여유 디스크를 모니터링하십시오. 에이전트가 완료되면 출력을 검토하고(빌드, 열기, 헤드리스 스크린샷 찍기), 산출물을 서로 연결하고 커밋합니다. 생성된 자료는 소스에서 재구축됩니다: 슬라이드는 축어적 인용이 아닌 코드를 거부하며, 발표가 오프라인에서도 작동하도록 벤더드 라이브러리를 휴대합니다. 자세한 내용은 references/materials.md를 참조하십시오.
5단계: 라이브 데모
몇 초 안에 실행되는 하나의 데모 파일을 구축합니다: 주요 정리의 #check 및 #print axioms, linear_combination으로 확인된 하나의 인증서, grind로 증명된 동일한 사실, 주석 처리된 "고장내기" 변형(가시적으로 실패). 로컬로 실행하거나 클러스터 드라이버의 demo 명령을 통해 원격으로 실행합니다. 두 번 리허설하고 대비책(렌더링된 Verso 문서 또는 스크린샷)을 유지합니다. 자세한 내용은 references/live-demo.md를 참조하십시오.
6단계: 문서화 및 세션 종료
프로젝트는 CLAUDE.md(운영 지침), MEMORY.md(날짜가 있는 사실 및 결정), JOURNAL.md(날짜가 있는 항목), PLAN.md(✅ 완료 · 🟡 진행 중 · ⬜ 할 일 · ❓ 사용자 결정), MAINTENANCE.md(런북), README.md 및 볼트를 포함합니다. 각 세션 종료 시: 저널 항목을 추가하고, 계획을 업데이트하고, 새 개념과 결정에 대한 볼트 노트를 추가하고, 커밋합니다(Conventional Commits). 클라이언트 메모리 파일은 프로젝트보다 오래 지속되어야 하는 사실만 보관합니다. 자세한 내용은 references/documentation.md를 참조하십시오.
7단계: 게시 (명시적 요청 시에만)
먼저 모든 것을 로컬에서 빌드합니다. 사용자가 요청한 것만, 이 세션에서, 0단계에서 선택한 대상에 게시합니다: 비공개 Claude 아티팩트, GitHub Pages, 또는 화이트리스트 배포 스크립트를 통한 웹 서버(드라이 런, 링크 검사 및 누출 검사(tools/leak_scan.py) 포함). 공개 저장소는 사용자가 푸시하기 전에 새로운 히스토리와 누출 검사를 받습니다. 자세한 내용은 references/publishing.md를 참조하십시오.
시작 체크리스트
- 0단계 질문에 답변하고 결정이 기록되었습니다.
- 논문이 선택되었거나(1단계) 주어졌습니다. 출처를 가져오고 체크섬을 확인했습니다.
python3 "$SKILL/tools/scaffold.py" <project> ...;git init; 첫 번째 커밋.- digest 작성, 주장 태그 지정,
PLAN.md에 검증 표 작성. - 검증 및 형식화 시작; digest가 안정되면 자료 에이전트 실행.
- 세션 종료: 저널, 계획, 볼트, 커밋.