| --- |
| license: apache-2.0 |
| base_model: m-a-p/OProver-8B |
| library_name: peft |
| pipeline_tag: text-generation |
| tags: |
| - lean |
| - lean4 |
| - theorem-proving |
| - lora |
| - peft |
| --- |
| |
| # Kakeya OProver Stage 2 — SFT1000 |
|
|
| > **Status: MATCHED BASELINE** |
|
|
| ## 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-1000`](https://huggingface.co/datasets/FluffyAIcode/Kakeya-OProver-Training). Artifact SHA-256: `5ebec3f7ed71d0af202924ea9d5ca12a857c5363b89b028dbf74268bf2e32f24`. 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 700 Mathlib examples, with 100 validation and 200 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. |
|
|
| ```json |
| { |
| "status": "MATCHED BASELINE", |
| "all22": { |
| "exact": 9, |
| "n": 22, |
| "parser": 22, |
| "unsafe": 0 |
| }, |
| "holdout18": { |
| "exact": 5, |
| "n": 18 |
| }, |
| "canary4": { |
| "exact": 4, |
| "n": 4 |
| }, |
| "audit_sha256": "5e0f757353ffe17315c9b78c60bb46de9ae34e736f9460e69ec26ca1d6213f9c", |
| "protocol_root": "6047aa9e4f3ff9594f7913e943cf40dc050b49328b7a42a80a72beefe5c641d7" |
| } |
| ``` |
|
|
| ## 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 |
|
|
| 5/18 holdout tasks failed exact Lean validation. Warning-bearing outputs and one length stop were observed; unsafe outputs were zero. |
|
|
| ## 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`](https://huggingface.co/m-a-p/OProver-8B) at `cd9ffd383b584d95bf00e04b88b35b05928b211c` |
| - Immutable source revision: `8eead931f4b090bca2421fead7d0c64191bea116` |
| - Adapter SHA-256: `5e5399518c0741140a14d2cca2fade8ec3eb95fb587139c5c9894d5e297a3b55` |
| - Dataset artifact SHA-256: `5ebec3f7ed71d0af202924ea9d5ca12a857c5363b89b028dbf74268bf2e32f24` |
| - 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`](./blob/main/release-manifest.json). |
|
|
