Kakeya OProver Stage 1 — SFT90
Summary
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:
sft-90. Artifact SHA-256:
eacefeab327a0d8c4b66e90b9afe9f7b8eb1df62c87abc9a1166f6b3e5ba8ced. Only Mathlib Apache-2.0 material and explicitly derived training negatives are included; provenance-incomplete OProofs mixtures were excluded.
Method
QLoRA supervised fine-tuning on 63 Mathlib training examples, with 9 validation and 18 excluded holdout examples.
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.
1{
2 "status": "NO-GO",
3 "note": "Initial strict baseline did not qualify for deployment."
4}
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
The initial strict evaluation was a NO-GO. This checkpoint is retained as the small-data baseline.
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:
cd091e33bc57f6c0f664846c6681b26d1163e411
- Adapter SHA-256:
0b0770e31ad6e77b33742a5d68dfb48cc0fa67efae4c965aaa6309fd031a9b03
- Dataset artifact SHA-256:
eacefeab327a0d8c4b66e90b9afe9f7b8eb1df62c87abc9a1166f6b3e5ba8ced
- 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.
