| --- |
| title: Conjecture Lean+AI Lab |
| sdk: gradio |
| sdk_version: "6.6.0" |
| python_version: "3.10" |
| app_file: app.py |
| pinned: false |
| emoji: "🔬" |
| --- |
| |
| # Conjecture Lean+AI Lab |
|
|
| This Space is tailored for conjecture-focused math research workflows that |
| combine: |
|
|
| - AI-assisted reasoning and strategy generation |
| - dataset-grounded retrieval from `NorthernTribe-Research/math-conjecture-training-corpus` |
| - model execution using `NorthernTribe-Research/math-conjecture-model` (with fallback) |
| - explicit work trace emission on every run |
| - Lean-oriented verification stubs for formal follow-up |
| - alignment with the simple-to-intermediate-to-advanced-to-Lean response profile used in training and eval |
|
|
| ## What this Space does |
|
|
| 1. Accepts a conjecture statement and analysis mode. |
| 2. Lets you choose response depth (`Simple` to `Lean formalization`, including progressive simple-to-Lean mode). |
| 3. Retrieves relevant examples from the dataset (validation/test splits). |
| 4. Builds a transparent prompt with evidence context. |
| 5. Runs model inference (preferred repo, then fallback). |
| 6. Displays: |
| - full work log, |
| - retrieved evidence table, |
| - exact prompt sent to the model, |
| - model answer with explicit work sections, |
| - generated Lean theorem skeleton for formal verification. |
|
|
| ## Runtime secrets |
|
|
| Set at least one token secret in Space settings: |
|
|
| - `HF_TOKEN` or `HUGGINGFACE_HUB_TOKEN` |
|
|
| Optional: |
|
|
| - `HF_USERNAME` |
|
|
| ## Notes |
|
|
| - The app is intentionally designed for auditability and reproducibility. |
| - Every run should expose intermediate work artifacts in the UI. |
|
|
