---
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.