README.md

metadata

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.