seminário-estudo-profundo

Seminário de estudo profundo

Uma apresentação de seminário preparada como um estudo aprofundado de um artigo. Primeiro o agente ajuda o usuário a escolher o artigo em uma discussão interativa baseada em evidências. Em seguida, reescreve o artigo como um resumo onde cada afirmação carrega seu status de verificação. Refaz os cálculos com um sistema de álgebra computacional (CAS), formaliza a lógica em Lean e registra o que encontra no artigo. Por fim, constrói os materiais da apresentação a partir dessa única fonte de verdade. O usuário decide; o agente propõe com evidências e verifica tudo o que afirma.

Os arquivos fornecidos são relativos ao diretório base desta habilidade (mostrado quando a habilidade é carregada); abaixo é chamado de $SKILL. Os arquivos do projeto vão para o diretório do projeto do usuário, nunca para $SKILL.

Fases e o que ler

fase	ler primeiro	deixa para trás
0 tomada	references/intake.md	respostas em MEMORY.md, decisões em aberto em PLAN.md
1 ideação do tópico	references/ideation.md	o artigo escolhido; cada candidato em JOURNAL.md
2 fonte, arcabouço, resumo	references/digest.md	repositório, source/SOURCE.md, resumo com registro de descobertas
3 verificação	references/verification.md, references/lean-palomar.md, references/compute.md	transcrições CAS, telas numéricas, biblioteca Lean, auditoria, logs
4 materiais	references/materials.md, templates/briefs/	notas, slides, plano de quadro, documento Verso, página de destino, cofre
5 demonstração ao vivo	references/live-demo.md	um arquivo de demonstração ensaiado e um plano de contingência
6 documentação	references/documentation.md	diário, plano, memória, notas do cofre, commits
7 publicação	references/publishing.md	nada, a menos que o usuário peça nesta sessão
qualquer	references/traps.md	leia antes de trabalhar com Lean, cluster, CAS ou site
artigo de CC	references/computer-science.md	a leitura de ciência da computação das fases 1–5

As fases são um menu, não uma marcha. Uma apresentação só de leitura são as fases 0–2 mais os materiais de que precisa; um usuário que chega com um artigo começa na fase 0 e pula a fase 1.

Princípios

1. O usuário escolhe; você propõe com evidências. Nunca escolha o artigo, a profundidade ou o alvo de publicação silenciosamente. Um redirecionamento ("não convencido", "algo mais recente") é normal: refina o perfil, então comece uma nova rodada em vez de defender a anterior.
2. Apenas fontes primárias. Verifique o título, autores, datas, versão, número de páginas e disponibilidade do código na fonte: a página de resumo ou API do arXiv, o PDF em si, o repositório. Rotule anúncios de empresas ou da imprensa como afirmações.
3. Todo número mostrado é calculado, nunca lembrado. Números em slides, páginas e notas vêm de cadernos executados, transcrições CAS, saída do Lean ou logs de construção.
4. Uma única fonte de verdade. O resumo é a fonte matemática de verdade. Cada uma de suas afirmações é marcada como [Lean], [CAS], [num], [exp] ou [paper]. As notas, slides, documento Verso e página derivam dele e nunca o contradizem.
5. O CAS encontra, o assistente de prova verifica. Certificados vão de transcrições CAS através de um gerador (tools/cert2lean.py) para Lean. Arquivos gerados são reconstruídos, nunca editados manualmente.
6. Fatos difíceis, mas padrão, tornam-se hipóteses explícitas, nunca axiomas. Registre cada um no resumo e nos metadados de formalização.
7. Descobertas são confidenciais por padrão. Descobertas sobre o artigo não publicado de outra pessoa permanecem no projeto até que o usuário decida. Para um erro real, sugira avisar os autores primeiro.
8. Proteja a máquina e os recursos compartilhados. Verifique o espaço livre em disco antes de instalar toolchains, nunca execute lake update sem MATHLIB_NO_CACHE_ON_UPDATE=1, e nunca construa dentro de outros projetos do usuário. Siga a etiqueta do cluster em references/compute.md.
9. Um proprietário por arquivo. Cada subagente escreve apenas seu próprio diretório; você integra, revisa e faz commit.
10. Ações voltadas para fora precisam de uma solicitação explícita na sessão atual. Isso cobre implantar, fazer push, criar um repositório remoto e publicar um artefato. Nunca escreva um segredo (senha, token, chave privada) em nenhum arquivo.
11. Consulte o jargão do usuário nos arquivos do próprio usuário primeiro. Um termo desconhecido ("classe de registro", uma sigla de seminário) muitas vezes está definido em suas notas ou projetos. Pesquise lá, depois na web, depois pergunte.

Fase 0: tomada

Examine o ambiente primeiro como somente leitura, para que as perguntas ofereçam opções concretas. Verifique o espaço livre em disco (df -h ~), os toolchains Lean instalados, o CAS disponível (local ou remoto), Python e uv, e qualquer projeto que o usuário tenha nomeado como formato a ser copiado. Em seguida, pergunte com a ferramenta de pergunta (AskUserQuestion no Claude Code): no máximo quatro perguntas por chamada, duas a quatro opções cada, a opção recomendada primeiro e marcada "(Recomendado)". O banco de perguntas está em references/intake.md; ele cobre a apresentação, o tópico e profundidade, o CAS e computação, os entregáveis, como o dashboard é entregue (apenas local ou online, e onde; agora ou depois) e git. Pule o que a primeira mensagem do usuário já responde e confirme em uma linha. Registre as respostas como decisões datadas em MEMORY.md; as em aberto vão para PLAN.md como ❓.

Fase 1: ideação do tópico (quando o artigo não é dado)

Execute rodadas até o usuário escolher (references/ideation.md):

1. Construa um perfil de interesses a partir do registro arXiv do usuário (tools/arxiv_scan.py author), dos READMEs de seus projetos atuais e do que ele disse. Mostre-o em três linhas para que ele possa corrigir.
2. Pesquise em paralelo: pesquisa na web por notícias; API do arXiv sobre categorias × tópicos × uma janela de recência (tools/arxiv_scan.py scan, depois rank); repositórios de código através da API do GitHub e clones rasos no scratchpad (tools/tactic_census.py para código Lean).
3. Verifique cada candidato que você apresentará (id, título, autores, datas, versões, páginas do PDF, link do código). Reavalie uma afirmação espetacular você mesmo quando for barato.
4. Apresente a lista curta em prosa: uma recomendação com por que se encaixa no usuário e no formato, duas ou três alternativas com trade-offs, artigos logo fora dos filtros, notícias que valem cinco minutos e as fontes. Termine com uma pergunta direta. A ferramenta de pergunta é uma conveniência para uma escolha final nítida; se o usuário recusar para esclarecer, ele quer conversar, então pergunte o que ele quer mudar.
5. Registre cada candidato e o motivo pelo qual foi descartado; isso vai para JOURNAL.md no momento da criação do arcabouço.

Fase 2: fonte, arcabouço, resumo

Baixe o PDF e o código-fonte LaTeX para source/ (ignorados pelo git). Registre a versão e as somas de verificação SHA-256 em source/SOURCE.md. Transcreva fórmulas e listas do LaTeX, nunca da camada de texto do PDF. Crie o arcabouço do projeto com tools/scaffold.py (modelos de documentação, o resumo e opcionalmente os esqueletos Lean, CAS, cluster, site, slides, livro, Verso e cofre). Em seguida, escreva o resumo (templates/digest/digest.md): o resultado em três linhas, antecedentes, configuração, uma seção por teorema com sua arquitetura de prova e etiquetas de status, o registro de descobertas (severidades: confirmado / redação / hipótese implícita / fortalecimento / erro) e exercícios. Detalhes: references/digest.md.

Fase 3: verificação

Transforme toda afirmação computacional e todo "um verifica" em uma linha de uma tabela de verificação em PLAN.md, então trabalhe nela:

• telas numéricas primeiro (alta precisão; pegam erros de transcrição, não provam nada);
• scripts CAS com transcrições commitadas, cujas linhas CHECK devem ser verdadeiras; divergências vão para o registro de descobertas (references/verification.md);
• certificados: o CAS imprime blocos CERT, tools/cert2lean.py escreve o arquivo Lean, e linear_combination ou ring verificam cada identidade; grind pode reprovar os mesmos passos sem certificado, o que vale a pena mostrar;
• Lean: afirmações primeiro, depois provas; leve ou classe Palomar (Challenge.lean/Solution.lean/comparator.json, apenas axiomas padrão, auditoria de axiomas com import all, lake comparator --paranoid, construção livre de avisos, logs). Veja references/lean-palomar.md e references/compute.md para construções locais versus em cluster e as regras de espaço em disco.

Trate avisos de linter como possíveis descobertas: um argumento de instância não utilizado pode significar que o teorema vale mais genericamente do que o artigo afirma.

Fase 4: materiais, por subagentes paralelos

Lance um agente em segundo plano por entregável, cada um dono de seu diretório: re-verificação CAS, o documento Verso, notas (Jupyter Book), slides com um plano de quadro e a página de destino com sua imagem herói e o cofre. Preencha os briefs em templates/briefs/. Cada brief nomeia as fontes de verdade (o resumo, os arquivos Lean, as transcrições), os fatos que pode afirmar, os comandos que pode executar e que nunca deve inventar números, nomes, horários ou salas. Continue verificando enquanto eles rodam. Quando um fato mudar (um novo resultado, uma nova contagem, uma nova demonstração), envie a cada agente em execução uma atualização curta e autocontida com SendMessage: o que mudou, onde está, o que adicionar, "opcional, mantenha seu plano atual". Agentes rederivam números, então também arbitram o resumo: peça-lhes que relatem qualquer divergência, então corrija o resumo (datado) e avise os outros. Monitore o disco livre enquanto vários agentes rodam. Quando um agente terminar, revise sua saída (construa-a, abra-a, tire capturas de tela headless), vincule os entregáveis uns aos outros e faça commit. Materiais gerados são reconstruídos de suas fontes: os slides recusam código que não é um excerto textual, e carregam bibliotecas empacotadas para que a apresentação funcione offline. Detalhes: references/materials.md.

Fase 5: demonstração ao vivo

Construa um arquivo de demonstração que roda em segundos: #check e #print axioms do teorema principal, um certificado verificado por linear_combination, o mesmo fato provado por grind e uma variante "quebrar" comentada que falha visivelmente. Execute-o localmente ou remotamente através do comando demo do driver do cluster. Ensaie duas vezes e mantenha um plano de contingência (o documento Verso renderizado ou capturas de tela). Detalhes: references/live-demo.md.

Fase 6: documentação e fim da sessão

O projeto carrega CLAUDE.md (instruções operacionais), MEMORY.md (fatos e decisões datados), JOURNAL.md (entradas datadas), PLAN.md (✅ concluído · 🟡 em andamento · ⬜ a fazer · ❓ decisão do usuário), MAINTENANCE.md (runbook), README.md e o cofre. Ao final de cada sessão: anexe uma entrada no diário, atualize o plano, adicione notas ao cofre para novos conceitos e decisões e faça commit (Commits Convencionais). Os arquivos de memória do cliente contêm apenas fatos que devem sobreviver ao projeto. Detalhes: references/documentation.md.

Fase 7: publicação (apenas com solicitação explícita)

Construa tudo localmente primeiro. Publique apenas o que o usuário pediu, nesta sessão, para o alvo escolhido na fase 0: um artefato privado do Claude, GitHub Pages ou um servidor web através de um script de deploy com lista de permissões, com uma simulação, uma verificação de links e uma varredura de vazamentos (tools/leak_scan.py). Um repositório público recebe um histórico limpo e uma varredura de vazamentos antes de o usuário fazer push. Detalhes: references/publishing.md.

Lista de verificação inicial

1. Perguntas da fase 0 respondidas, decisões registradas.
2. Artigo escolhido (fase 1) ou dado; fonte baixada e soma de verificação calculada.
3. python3 "$SKILL/tools/scaffold.py" <projeto> ...; git init; primeiro commit.
4. Resumo escrito, afirmações marcadas, tabela de verificação em PLAN.md.
5. Verificação e formalização iniciadas; agentes de materiais lançados assim que o resumo estiver estável.
6. Fim da sessão: diário, plano, cofre, commit.