mineproof

name

mineproof

description

Extract reusable proof assets from curated theoretical papers and use them for project-level theorem planning, Level 3 proof-module extraction, human-in-the-loop proof repair, and paper-level proof drafting. Use when Codex needs to process theory papers, build paper/theorem maps, select proof modules for a research idea, extract proof modules, adapt proof logic to a target theorem, or construct proof plans, proof work units, proof state, gap notes, and LaTeX proof drafts.

MineProof

Purpose

MineProof extracts reusable proof assets from curated theoretical papers and uses them to support project-level theorem planning and proof construction.

Do not use MineProof as a generic literature-review tool. Use it to convert human-collected theoretical papers into structured, searchable proof assets, then use those assets to design, adapt, repair, and draft proofs for new research projects.

Core goal:

Curated theoretical papers
  -> reusable proof assets
  -> project-specific proof modules
  -> human-in-the-loop paper-level proof construction

MineProof should move toward paper-usable proofs while never pretending an unresolved gap has been proved.

Workflows

Use the workflow files for detailed procedure:

workflows/coarse_extract_paper.md
workflows/select_for_project.md
workflows/fine_extract_proof_module.md
workflows/draft_proof_from_modules.md

Use the templates under templates/ for generated artifacts.

Stage 1: Coarse Paper Extraction

Use workflows/coarse_extract_paper.md when the user provides papers but no concrete project proof task yet.

Inputs may include a paper PDF, extracted text, LaTeX source, notes, or a folder of curated theoretical papers.

Outputs:

paper_map.md
theorem_map.md

Use:

templates/paper_map.md
templates/theorem_map.md

Identify mathematical setting, assumptions, main results, proof architecture, theorem-level entry points, reusable proof assets, candidate proof modules, and recommended extraction depth when visible.

Do not reconstruct full proofs or extract every appendix lemma during coarse extraction.

Stage 2: Project Selection and Proof-Module Planning

Use workflows/select_for_project.md when the user provides a project idea, model setup, target theorem, candidate claims, or existing coarse paper assets.

Outputs:

theory_target_map.md
claim_triage.md
selected_theorems.md
fine_extraction_plan.md

Use:

templates/theory_target_map.md
templates/claim_triage.md
templates/selected_theorems.md
templates/fine_extraction_plan.md

This stage should formalize project-level theory targets, decompose broad theorem goals into claims, triage proof difficulty, match claims to paper assets, select entry results and candidate proof modules, define proposed module boundaries, and assign extraction depth.

Important distinction:

Theorem / proposition / lemma = entry point.
Proof module = fine extraction unit.

Do not treat a selected theorem as the automatic boundary of fine extraction.

Stage 3: Level 3 Proof-Module Extraction

Use workflows/fine_extract_proof_module.md when the user provides fine_extraction_plan.md, asks to extract a selected entry result, or needs proof assets detailed enough for later proof drafting.

Outputs:

proof_module_card.md
proof_component_map.md
proof_dependency_notes.md

Use:

templates/proof_module_card.md
templates/proof_component_map.md
templates/proof_dependency_notes.md

Default extraction depth:

Level 3: Paper-Draft Proof Module

A Level 3 proof module should preserve exact statements and assumptions, minimal connected module boundary, included and excluded dependencies, proof skeleton, bottleneck lemma details, nonstandard proof moves, event/probability/rate/inequality assembly, transferable proof components, compatibility notes, transfer risks, and remaining gaps.

Routine algebra, standard inequalities, and local notation-only appendix details may stay at Level 2 or be omitted with reasons. Use Level 4 only when near-complete reconstruction is explicitly needed or when Level 3 is not enough to support drafting.

Stage 4: Human-in-the-Loop Proof Construction

Use workflows/draft_proof_from_modules.md when the user provides a target theorem and extracted proof modules, or wants to continue an existing proof state.

Inputs may include:

proof_module_card.md
proof_component_map.md
proof_dependency_notes.md
theory_target_map.md
claim_triage.md
proof_plan.md
proof_work_units.md
proof_state.md
proof_gap_notes.md

Outputs:

proof_plan.md
proof_work_units.md
proof_state.md
proof_gap_notes.md
proof_draft.tex

Use:

templates/proof_plan.md
templates/proof_work_units.md
templates/proof_state.md
templates/proof_gap_notes.md
templates/proof_draft.tex

Default rule:

Plan first.
Adapt explicitly.
Work one proof unit at a time.
Use human review for research choices.
Draft only with gap labels.

Do not attempt to finish all theoretical results in one pass. Formalize the target theorem, build proof architecture, match proof modules, perform adaptation checks, create a proof plan, decompose the proof into work units, choose the next unit, work one unit at a time, update proof state, generate repair options, and integrate established units into a partial or full proof draft.

Proof work units may include lemma proofs, event constructions, rate assembly, assumption checks, transfer-gap repairs, theorem refinements, or proof draft paragraphs.

Dispatch Logic

When the user provides papers but no project idea:

1. Use workflows/coarse_extract_paper.md.
2. Generate paper_map.md and theorem_map.md.
3. Mark candidate proof modules and recommended extraction depth when visible.

When the user provides papers plus a project idea or target theorem:

1. Ensure coarse paper assets exist.
2. Use workflows/select_for_project.md.
3. Generate theory_target_map.md, claim_triage.md, selected_theorems.md, and fine_extraction_plan.md.

When the user provides existing coarse assets and a project context:

1. Use workflows/select_for_project.md.
2. Select entry results and proof modules.
3. Prepare fine-extraction tasks.

When the user provides fine_extraction_plan.md or asks to extract a selected theorem, lemma, proposition, proof section, or component:

1. Treat the selected item as an entry point.
2. Use workflows/fine_extract_proof_module.md.
3. Extract the minimal Level 3 proof module needed for paper-level drafting.

When the user provides a target theorem and extracted proof modules:

1. Use workflows/draft_proof_from_modules.md.
2. Generate or update proof_plan.md.
3. Generate or update proof_work_units.md and proof_state.md.
4. Advance one work unit at a time unless the user explicitly asks for a broad integrated draft.
5. Generate proof_draft.tex only as an accurate reflection of established, conditional, and gap-labeled proof state.

Research Continuation Logic

Do not stop merely because a proof gap is found. Use gaps to continue research.

Classify gaps:

Definition gap
Assumption gap
Transfer gap
Rate gap
Event gap
Lemma gap
Theorem-too-strong gap
Source-extraction gap

Then propose repair options, such as adding or modifying assumptions, weakening the theorem, introducing intermediate lemmas, re-proving missing lemmas, switching proof modules, deepening extraction to Level 4, changing proof route, or producing a conditional proof draft.

Never fabricate closure. Unresolved gaps must remain visible in proof_gap_notes.md, proof_state.md, and any generated proof_draft.tex.

Core Principles

1. Treat papers as sources of proof assets, not as literature-review objects.
2. Prefer theorem structure, assumptions, proof dependencies, proof modules, and reusable proof components over background narrative.
3. Distinguish paper-level framework relevance from local component reuse.
4. Distinguish entry results from proof modules.
5. Do not extract all appendix lemmas by default.
6. Default fine extraction to Level 3: Paper-Draft Proof Module.
7. Preserve assumptions, quantifiers, rates, probability events, dependency chains, and failure modes.
8. Never silently generalize a source-paper result to a target setting.
9. Do not present unresolved gaps as completed proof.
10. Continue research after gaps by proposing repair options.
11. Work one proof unit at a time during proof construction.
12. Use human review for research choices such as adding assumptions, weakening the theorem, accepting a conditional claim, or changing proof route.
13. Keep outputs structured so later sessions can resume from artifacts.