pi-autocontext-erdos

Pi package for AutoContext-assisted Erdős-style formal math problem loops with Lean verification.

Latest published package: pi-autocontext-erdos@0.1.0. Release evidence is recorded in docs/RELEASE_0.1.0.md. Main is now preparing 0.1.1 with fixed-template handoff support.

This package is an orchestration layer. It does not replace Lean and does not claim to prove open problems. It helps structure a math exploration loop: problem intake, formalization, lemma planning, proof attempts, Lean-backed verification, and reporting.

Relationship to pi-autocontext-lean-verify

Use this package for the problem loop and research workflow:

pi-autocontext-erdos
  = problem intake + formalization + lemma ladder + attempt logs + reports

Use pi-autocontext-lean-verify as the verifier/proof-repair backend:

pi-autocontext-lean-verify
  = Lean oracle + fixed-template proof-body repair + guardrail checks

Install both when you want proof-repair automation:

pi install npm:pi-autocontext-lean-verify@0.1.17
pi install git:github.com/greyhaven-ai/pi-autocontext-erdos

From a local checkout:

pi install ./pi-autocontext-erdos

For local development, from this checkout:

npm install
npm run validate
npm run pack:dry-run
pi install ./pi-autocontext-erdos --local

Provided resources

• Extension tool: autocontext_erdos
• Skill: erdos-math-loop
• Prompt template: erdos-math-loop.md
• Domain notes: docs/DOMAIN.md
• Validation notes: docs/VALIDATION.md
• Example runs:
  • examples/erdos-ginzburg-ziv-n2
  • examples/erdos-ginzburg-ziv-n3

Example validation

The checked examples include the n = 2 and n = 3 finite instances of the Erdős–Ginzburg–Ziv theorem over natural numbers. The n = 2 example proves:

theorem egz_two_nat (a b c : Nat) :
    (a + b) % 2 = 0 ∨ (a + c) % 2 = 0 ∨ (b + c) % 2 = 0

The harder n = 3 example proves that among any five natural numbers, one of the ten triples has sum divisible by 3. The AutoContext repair smoke in docs/EGZ_N3_AUTOCONTEXT_REPAIR.md deliberately breaks that proof, repairs it back to a Lean-verified candidate with autocontext_erdos, and the compact repaired proof is now the canonical example.

Validate the package and examples with:

npm run validate
npm run typecheck
npm run validate:extension
npm run validate:example

AutoContext-backed tool

The package registers one consolidated Pi tool:

autocontext_erdos

Actions:

• preflight: check Lean and uvx autoctx improve availability.
• init_problem: create the run artifact layout.
• verify_file: run Lean on a formalization and write attempt artifacts.
• autocontext_improve: invoke autoctx improve with a Lean verifier command and save prompt/rubric/logs/best candidate/verdict.
• export_fixed_template: freeze a named theorem into a Theorem.template.lean fixture with a {{PROOF}} hole for pi-autocontext-lean-verify proof-body repair.
• summarize_run: summarize files and attempt verdicts under a run root.

The AutoContext action uses:

uvx --python 3.12 --from autocontext==0.5.1 autoctx improve ... --verify-cmd "<lean> {file}"

For whole-file repair, pass preserveTheorems to require exact normalized theorem-statement preservation before a Lean-verified candidate is accepted:

{
  "action": "autocontext_improve",
  "preserveTheorems": ["mod_three_eq_zero_or_one_or_two", "egz_three_nat"]
}

If Lean accepts a candidate but a preserved theorem statement changes, the verdict is theorem_statement_changed with Accepted: false.

For the compact EGZ n = 3 repair loop, current validation recommends timeoutSeconds=240; timeoutSeconds=120 is useful but budget-limited for this task.

When a theorem statement is ready to freeze, use export_fixed_template to hand off proof-body-only repair to pi-autocontext-lean-verify; see docs/LEAN_VERIFY_HANDOFF.md.

MVP workflow

A typical run creates a durable folder such as:

runs/<problem-slug>/
  problem.md
  source_notes.md
  formalization/
    Formalization.lean
    formalization_notes.md
  lemmas/
    lemma_plan.md
  attempts/
    0001/
      prompt.md
      candidate.lean
      lean.stderr.txt
      verdict.md
  reports/
    final_report.md

Every mathematical claim in the final report must be labeled as one of:

• Lean verified;
• formalization draft;
• conjecture;
• heuristic/proof sketch;
• failed attempt.

Guardrail posture

Never count a proof unless Lean verifies the exact theorem or unchanged template. Do not use sorry, admit, new axioms, unsafe, theorem weakening, proof-by-importing-answer, or hidden assumptions as success criteria.