This is an independent PEFT LoRA checkpoint in the Kakeya OProver training journey. It is a proof-advisor research artifact, not an autonomous proof or mathematical truth claim.

Training Data

Public data config: dpo-2000. Artifact SHA-256: 2de80cfbb1c5e14c89611810e02b9f432ec2643a203e4c983cd48b1e6ad919a3. Only Mathlib Apache-2.0 material and explicitly derived training negatives are included; provenance-incomplete OProofs mixtures were excluded.

Method

DPO on 1,400 training pairs and 200 validation pairs; 400 holdout pairs were excluded from training.

Strict Lean Evaluation

All matched Stage2–Stage4 evaluations used 22 tasks (18 holdout + 4 canary), one frozen task order, seed, temperature, token budget, and context policy. Parser rate was 22/22 and unsafe generations were 0 for matched evaluations.

json

{
  "status": "NO-GO",
  "all22": {
    "corrected_exact": 4,
    "n": 22,
    "parser": 22,
    "unsafe": 0
  },
  "holdout18": {
    "corrected_exact": 1,
    "n": 18
  },
  "canary4": {
    "corrected_exact": 3,
    "n": 4
  },
  "audit_sha256": "aeb63952d78a132cbe24f4c9238b1c305737c243a51e337c67d5ec08150fe391",
  "comparison_payload_sha256": "837360593b1fdee9205166cf59d7d091b5992c33a8488d013b3283f6da5b7b8d",
  "comparison_signature": {
    "algorithm": "Ed25519",
    "public_key_base64": "VEQy27ukhgP7vMlIFwRBVYBgXM0RvFXPrOmQ2cnLOmU=",
    "signature_base64": "ZEVKmswS+H8sLkrVO3ZFi/OftAUACZNn7h4qH7F2EK2cGzniGMisvAtH/n8wziW5xf40/HylwBEh4HqNGrcmDg=="
  },
  "paired_stage2": {
    "all22_mcnemar_exact_two_sided_p": 0.0625,
    "holdout18_mcnemar_exact_two_sided_p": 0.125,
    "interpretation": "Practically material and directionally strong regression, but not conclusive at alpha 0.05."
  }
}

Safety

No private chain-of-thought, production prompts, Jensen candidate proof bodies, credentials, or raw candidate-bearing signed audits are published. Stage status constrains use; Stage4 is PROOF-ADVISOR-ONLY.

Known Failures

Corrected strict validity regressed to 4/22 overall and 1/18 holdout. The paired Stage2 comparison was directionally strong but not significant at alpha 0.05.

Intended Use

Research on Lean proof suggestion, evaluation, and repair. Every generated proof must be compiled and independently reviewed. Not intended for unsupervised theorem claims or production deployment without separate authorization.

Reproducibility

Base: m-a-p/OProver-8B at cd9ffd383b584d95bf00e04b88b35b05928b211c
Immutable source revision: c3b684ce7729ec94305deac4fbc5fd506c7f79a6
Adapter SHA-256: 064fb996230352ae12fd326944e8c5696edc22c36d34fc710805cb5aa2a3f9e3
Dataset artifact SHA-256: 2de80cfbb1c5e14c89611810e02b9f432ec2643a203e4c983cd48b1e6ad919a3
Sanitized machine-readable files: evaluation/results.json, training/metrics.jsonl, training/trainer_state.json, provenance/manifest.json
Evaluation/audit digest references are in evaluation/results.json; raw candidate-bearing artifacts remain private.

Limitations

Small, single-seed strict suites cannot establish broad theorem-proving capability. Exact Lean rates have wide confidence intervals. Stage4 did not significantly outperform Stage2 in the matched paired test. Jensen remained SEARCH_EXHAUSTED with 0/6 Lean-valid candidates. RH PROVED: NO.

Attribution

Base model: m-a-p/OProver-8B (Apache-2.0). Training data derives from Mathlib at 360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56 (Apache-2.0). See NOTICE.

Release Manifest

The content-addressed public/private boundary and immutable asset references are in release-manifest.json.

FluffyAIcode/Kakeya-OProver-Stage3-DPO

Kakeya OProver Stage 3 — DPO

Summary