Primary evidence
- miniCTX: Neural Theorem Proving with (Long-)ContextsS1 · Primary research · Paper · 2024-08-05
- miniCTX evaluation repositoryS1 · Primary research · Repository
miniCTX tests theorem provers on long, unseen project context
The benchmark draws theorems from real Lean projects and textbooks and includes tooling for extracting new project contexts.
What happened?
miniCTX introduced Lean theorem-proving tasks with repository context spanning up to tens of thousands of tokens and showed that context-aware methods outperform state-only baselines.
Why it matters
It better approximated the conditions faced by practical proof agents operating inside large formal codebases.
Significance rationale: miniCTX moved evaluation toward repository-scale theorem proving where definitions and lemmas live in long, previously unseen context.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Computation only
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Models must retrieve and use relevant definitions and lemmas from long project context while proving.
- Human contribution
- Researchers constructed the benchmark and ntp-toolkit for context-aware theorem-proving data extraction.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- minictx, ntp-toolkit, lean
- Organizations
- carnegie-mellon-university
- Problems
- repository-level-theorem-proving
- Methods
- long-context, retrieval, benchmarking
Sources & artifacts
- miniCTX: Neural Theorem Proving with (Long-)ContextsS1 · Primary research · Paper · accessed 2026-09-10
- miniCTX evaluation repositoryS1 · Primary research · Repository · accessed 2026-09-11
- miniCTX benchmark and evaluation resourcesArtifact · Dataset
Verification history
- 2024-08-05 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
Corrections
No corrections recorded.