Primary evidence
- Proof Artifact Co-training for Theorem Proving with Language ModelsS1 · Primary research · Paper · 2021-02-11
- PACT LeanStep proof-artifact extraction codeS1 · Primary research · Repository
PACT uses proof artifacts to scale language-model theorem proving
The method extracts self-supervised objectives from kernel-level proof terms and trains them alongside tactic prediction.
What happened?
PACT co-trained a Transformer theorem prover on Lean proof artifacts and improved held-out theorem-proving success from 32% to 48%.
Why it matters
It helped establish that formal libraries contain much more learnable signal than only the next tactic labels exposed at the surface.
Significance rationale: PACT established proof-term-derived self-supervision as a practical way to alleviate data scarcity in neural theorem proving.
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
- Substantive AI support
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- The language model predicts proof tactics using representation learned from both tactic labels and proof-artifact objectives.
- Human contribution
- Researchers designed the artifact objectives, instrumented Lean, and curated the evaluation setting.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- pact, lean
- Organizations
- openai
- Problems
- —
- Methods
- proof-artifact-cotraining, transformer, tactic-prediction
Sources & artifacts
- Proof Artifact Co-training for Theorem Proving with Language ModelsS1 · Primary research · Paper · accessed 2026-09-10
- PACT LeanStep proof-artifact extraction codeS1 · Primary research · Repository · accessed 2026-09-11
- LeanStep proof-artifact extraction code used for PACTArtifact · Code
Verification history
- 2021-02-11 · 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.