discuss

Read and discuss proofs, strategies, or math concepts without making any edits.

Repository: jeffrey-dot-li/lean-homology
Last source activity: February 10, 2026 at 22:25
Detected SKILL.md language: English
Stars: 2
Forks: 0

Install options

The review-first prompt is selected by default. You can switch to a direct command or download a local copy.

Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.

A direct command skips the review prompt. Inspect the source before running it.

npx skills add https://github.com/jeffrey-dot-li/lean-homology --skill discuss

The command stays on one line. Scroll horizontally to inspect it before copying.

Prefer a local copy? Download the files currently available to SkillsMP.

Review the source files

Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.

SKILL.md

Source instructions · Read-only preview

Back to search Back to installation

fill-sorry

Prove a specific sorry'd lemma iteratively using Lean LSP tools.

2026-03-20

improve-workflow

Improve Claude Code workflow by updating assistants.md, skills, memory, or CLAUDE.md.

2026-03-20

clean

Fix warnings line by line and bring code into compliance with Mathlib style standards.

2026-03-16

View all from this repository

name	discuss
description	Read and discuss proofs, strategies, or math concepts without making any edits.

Discuss Mode

Read and discuss proofs, strategies, or mathematical concepts. No file edits in this mode.

Topic: $ARGUMENTS

What this mode is for

Reading a proof and suggesting whether it could be simplified or refactored
Discussing alternative proof strategies before committing to one
Explaining what a proof or definition does
Comparing approaches (e.g., "would it be simpler to use X instead of Y?")
Answering mathematical questions about the formalization

Procedure

Read the relevant code using Read, lean_goal, lean_hover_info, etc.
Use search tools (lean_leansearch, lean_loogle, etc.) as needed to inform the discussion.
Give a clear, direct answer or analysis.
Do not edit any files. If the discussion leads to a concrete action, ask the user if they want to switch modes (e.g., to /refactor or /fill-sorry).

Rules

Read-only. No Edit, Write, or file modifications.
If the user asks you to make a change, confirm mode switch first.

discuss

Source facts

Install options

Review the source files

More from this repository

Discuss Mode

What this mode is for

Procedure

Rules

More from this repository

Discuss Mode

What this mode is for

Procedure

Rules