Argument Validator

2. Extract Argument Structure

Restate the argument as a numbered list:

• Separate explicit premises from implicit assumptions
• Label each premise as logical, definitional, or empirical
• Note any ambiguous terms or scope shifts

3. Formalize the Logic

Translate into a precise formal representation:

• Choose the smallest logic that fits (propositional or first-order)
• Define symbols and predicates explicitly
• Encode the argument as premises → conclusion
• Flag quantifier order and scope changes

4. Check Logical Validity

Attempt a derivation from premises to conclusion:

• Identify the first point where the proof fails
• Produce the minimal additional assumption needed for validity
• Provide a counterexample model when possible

5. Formalize in Lean (Optional)

When the user wants machine-checking, offload to a Lean formalizer:

• Check for Lean availability (lean --version or ~/.elan/bin/lean --version)
• Use lean --stdin for quick checks when no project exists
• Ask the formalizer to return a compilable Lean snippet plus missing lemmas

6. Validate Assumptions with Research Agents

For each empirical or contestable assumption:

• Spawn one research subagent per assumption
• Provide the exact assumption and desired standard of evidence
• Require a summary, sources, and a confidence rating
• Run subagents in parallel when there are multiple assumptions

7. Synthesize the Final Analysis

Deliver a structured summary:

• Validity verdict (valid / invalid) with justification
• Soundness verdict (supported / unsupported / unknown)
• List of key assumptions and their evidence status
• Suggested revisions that would strengthen the argument

Subagent Prompts

Formalizer Agent (Logic + Lean)

Use a general subagent to formalize the argument:

You are a FORMALIZER agent.

INPUT:
- Argument text
- Extracted premises + conclusion
- Draft formalization (symbols and formulas)

TASK:
1. Tighten the formalization (minimal logic).
2. Identify missing premises or implicit assumptions.
3. Attempt a Lean formalization.
4. If proof fails, explain where and why.

OUTPUT:
- Refined formalization
- Lean theorem statement
- Lean proof sketch or error explanation
- List of missing assumptions

Assumption Research Agents

Use one general subagent per assumption:

You are a RESEARCHER agent.

ASSUMPTION:
[insert assumption]

TASK:
1. Use available web tools to find supporting or refuting sources.
2. Summarize evidence with citations.
3. Rate confidence (low/medium/high).

OUTPUT:
- Evidence summary
- Source list with URLs
- Confidence rating
- Notes on conflicts or gaps

Output Format

Provide results in this order:

1. Restated argument (premises → conclusion)
2. Formalization (symbols + formulas)
3. Validity analysis (proof gap or confirmation)
4. Lean check results (if performed)
5. Assumptions table (premise, type, evidence, status)
6. Recommendations or questions to resolve uncertainty