Skip to content

factory.md

Latest commit

 

History

History
45 lines (31 loc) · 1.38 KB

factory.md

File metadata and controls

45 lines (31 loc) · 1.38 KB
Raw

Factory Configuration — ProofPartner

Project

  • Name: ProofPartner
  • Description: Interactive agentic tool for math research using Lean 4 — transforms rough mathematical ideas into formal Lean 4 conjectures and discovers proofs through an explore-conjecture-prove loop
  • Language: Python 3.11+
  • Framework: Custom orchestrator (state machine)
  • Target branch: master

Goal

Expand ProofPartner's proof discovery capabilities through improved formalization accuracy, conjecture generation diversity, and proof search effectiveness.

Eval Dimensions

  • tests: Unit and integration test pass rate (pytest tests/ -v)
  • lint: Code style and static analysis (ruff check agentic_research/ tests/)
  • type_check: Type safety verification (mypy agentic_research/)
  • capability_surface: Fraction of core pipeline stages implemented and functional
  • observability: Structured logging coverage and cost tracking instrumentation

Threshold

0.45

Eval Command

pytest tests/ -v

Modifiable

  • agentic_research/ — all source code
  • tests/ — test suite
  • pyproject.toml — project configuration
  • factory.md — this file
  • CLAUDE.md — project conventions
  • README.md — documentation

Fixed Surfaces

  • .factory/ — factory infrastructure
  • data/benchmarks/ — downloaded benchmark data (read-only after download)