| --- |
| 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 1 — SFT90 |
|
|
| > **Status: NO-GO 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-90`](https://huggingface.co/datasets/FluffyAIcode/Kakeya-OProver-Training). 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. |
|
|
| ```json |
| { |
| "status": "NO-GO", |
| "note": "Initial strict baseline did not qualify for deployment." |
| } |
| ``` |
|
|
| ## 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`](https://huggingface.co/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`](./blob/main/release-manifest.json). |
|
|
