TPT Syntaxis

AI-optional, 100% Rust mathematical discovery engine powered by Lean 4.

TPT Syntaxis automatically discovers, verifies, minimizes, and publishes novel mathematical theorems. It combines formal verification (Lean 4 kernel as the sole source of truth) with high-performance Rust computation and optional heuristic AI search via OpenRouter.

Conjecture Generation → Proof Search → Lean Kernel Verification → Minimize + Audit → Publication
       (AI Compass)      (Symbolic +       (Absolute)            (Compression)     (Mathlib PR /
                         Compass)                                                  arXiv / Journal)

Getting Started
Prerequisites
Installation
First Run
Three Modes
Using the CLI
Using the Dashboard
Architecture
Workspace Crates
Configuration
Examples
How It Works
For Developers
License

Getting Started

5 minutes from zero to discovering your first theorem.

Prerequisites

Tool	Version	Purpose	Install
Rust	1.85+	Core language	rustup.rs
Lean 4	v4.12+	Proof verification	Elan
Just	latest	Command runner	`cargo install just`

For AI mode only:

Tool	Purpose	Install
OpenRouter API key	LLM access	openrouter.ai

Installation

# 1. Clone the repository
git clone https://github.com/tpt-solutions/tpt-syntaxis.git
cd tpt-syntaxis

# 2. Install Rust toolchain (pinned in rust-toolchain.toml)
rustup toolchain install stable

# 3. Install Lean via Elan (pinned in lean-toolchain)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# 4. Install Just command runner
cargo install just

# 5. Build everything
# NOTE: this project depends on Mathlib (see lakefile.lean). The first build
# fetches Mathlib and its prebuilt .olean cache via `lake exe cache get` — a
# multi-gigabyte download. Subsequent builds are incremental and much faster.
just build

First Run

# Run in symbolic mode (zero API cost, fully deterministic)
just run

# Output: TPT Syntaxis starts, discovers theorems using symbolic search
# The symbolic backend tries tactics like norm_num, simp, ring over goals

# Start the review dashboard
just dashboard

# Open http://127.0.0.1:3000 in your browser
# Review discovered theorems, accept/reject/flag for submission

Using AI Mode

# Set your OpenRouter API key
export OPENROUTER_API_KEY="your-key-here"

# Edit config.toml to enable AI mode
# Set backend = "hybrid" in [discovery] section

# Run with AI-guided search
just run

Three Modes

Mode	How It Works	When to Use	Cost
Symbolic	Beam search over simp-lemma matches + power tactics (`norm_num`, `ring`, `omega`, `linarith`, `aesop`), kernel-verified before recording	Laptop, offline, deterministic	Zero
AI	LLM guesses tactics based on semantic understanding	Abstract, creative leaps	API calls
Hybrid	AI compass suggests strategy; symbolic engine grinds subgoals	Default for serious discovery	API calls

Key insight: Even in AI mode, the Lean kernel is the sole source of truth. The AI can hallucinate freely — if it suggests a non-existent lemma, Lean rejects it and the engine moves on. The AI never writes trusted proof code.

Using the CLI

The tpt command provides full access to all capabilities:

# Install the CLI
cargo install tpt-syntaxis-cli

# Solve a theorem goal
tpt solve --goal "1 + 1 = 2" --mode symbolic
tpt solve --goal "a + b = b + a" --mode hybrid

# Search for similar theorems
tpt search "commutativity" --mode hybrid --top-k 5

# Minimize a proof (compress verbose proofs)
tpt minimize --file proof.lean

# Audit a proof for safety
tpt audit "add_zero" --axioms "Nat.add_zero"

# Manage sorry bounties
tpt bounties --file bounties.json

# Show version
tpt version

CLI Examples

$ tpt solve --goal "1 + 1 = 2" --mode symbolic
Solving: 1 + 1 = 2
Mode: symbolic

Suggested tactics:
  1. norm_num
  2. simp [Nat.add_zero]
  3. omega
  4. ring
  5. linarith

$ tpt minimize --file proof.lean
Minimizing proof in: proof.lean

Original: 8 steps
Minimized: 2 steps
Compression: 75%

Minimized proof:
theorem add_zero (a : Nat) : a + 0 = a := by
  simp [Nat.add_zero]
  done

Using the Dashboard

The dashboard provides a web-based review interface for discovered theorems.

# Start the dashboard
just dashboard

# Open http://127.0.0.1:3000

Dashboard Features

Page	What It Shows
Home (`/`)	Stats cards + theorem list with accept/reject/flag buttons, search panel with a 🎲 "Surprise Me" random-goal action
Theorem Detail (`/theorems/:id`)	Statement, original proof, minimized proof, Mathlib diff
Tactic Profile (`/theorems/:id/profile`)	Timing breakdown per tactic step
Proof Tree (`/theorems/:id/tree`)	ASCII visualization of proof structure
Suggestions (`/theorems/:id/suggest`)	Recommended tactics + similar theorems
Discover Goals (`/discover`)	Category cards (Arithmetic, Number Theory, Topology, etc.) — pick one to run a random search scoped to that category
Sorry Hunt (`/sorry-hunt`)	Lists `sorry`s found in the Lean sources; pick one to use its statement as a search goal
Coverage (`/coverage`)	Mathlib coverage statistics
Stats (`/stats`)	Overall dashboard statistics
Settings (`/settings`)	Configure the OpenRouter API key for AI/Hybrid mode

Dashboard Actions

Accept — Mark theorem as verified and ready for submission
Reject — Discard (not significant enough, incorrect, etc.)
Flag for Submission — Queue for Mathlib PR / arXiv / journal

Architecture

┌──────────────────────────────────────────────────────────────┐
│                        TPT Syntaxis                          │
├──────────────────────────────────────────────────────────────┤
│                                                              │
│  ┌──────────────┐    ┌──────────────┐    ┌──────────────┐   │
│  │  Conjecture   │───▶│ Proof Search │───▶│ Lean Kernel  │   │
│  │  Generator    │    │ (Symbolic +  │    │ Verification │   │
│  │  (AI Compass) │    │  Compass)    │    │ (Absolute)   │   │
│  └──────────────┘    └──────────────┘    └──────┬───────┘   │
│         ▲                                        │          │
│         │          ┌──────────────┐    ┌─────────▼────────┐ │
│         └──────────│  Mathlib PR  │◀───│ Minimize + Audit │ │
│                    │  / Journal   │    └──────────────────┘ │
│                    └──────────────┘                          │
└──────────────────────────────────────────────────────────────┘

The Trust Stack

┌─────────────────────────────────────────────────────────────┐
│  Human Interpretation                                        │  Subjective
│  "Is this theorem interesting?"                              │
├─────────────────────────────────────────────────────────────┤
│  Statement Correctness                                       │  Human must verify
│  "Does the Lean code say what we think it says?"             │  definitions match
├─────────────────────────────────────────────────────────────┤
│  Lean Kernel Verification                                    │  Machine-checked
│  "Is the proof logically valid?"                             │  GUARANTEED
├─────────────────────────────────────────────────────────────┤
│  Lean Kernel Source Code (~6,000 lines)                      │  Heavily audited
│  "Is the kernel itself trustworthy?"                         │  by the community
└─────────────────────────────────────────────────────────────┘

Discovery Pipeline

Stage	Actor	Output
1. Conjecture Generation	AI Compass + Symbolic Generator	List of candidate theorems
2. Proof Search	Hybrid backend (Symbolic + Compass)	Raw proof (possibly ugly)
3. Kernel Verification	Lean 4	Binary: accepted or rejected
4. Proof Minimization	`tpt-syntaxis-minimize`	Clean, compressed proof
5. Significance Filter	`tpt-syntaxis-audit`	Rating: Trivial → OpenProblem
6. Proof Audit	`tpt-syntaxis-audit`	Axiom list + warnings
7. Human Review	Dashboard	Accept / Reject / Submit
8. Publication	`tpt-syntaxis-publish`	Mathlib PR / arXiv / Journal

Workspace Crates

Crate	Purpose	Key Types
`tpt-syntaxis-bridge`	Lean 4 LSP/JSON-RPC interface	`LeanServer`, `LeanTacticState`
`tpt-syntaxis-core`	Orchestrator, Search Compass, algorithms	`MctsSearch`, `SearchCompass`, `DiscoveryBackend`
`tpt-syntaxis-forge`	Rust math FFI (SMT, linear algebra)	`SatSolver`, `Matrix`, `is_prime`
`tpt-syntaxis-extract`	Data pipeline, Mathlib extraction	`MathlibIndex`, `VectorIndex`, `LeanParser`
`tpt-syntaxis-minimize`	Proof compression	`Minimizer`, `TacticProof`, `TacticVerifier`
`tpt-syntaxis-audit`	Axiom checking, significance filtering	`Auditor`, `Significance`, `AxiomChecker`
`tpt-syntaxis-publish`	Mathlib PRs, arXiv, journal formatting	`MathlibPrCreator`, `ArxivFormatter`, `SorryBountyBoard`
`tpt-syntaxis-dashboard`	Web review UI (axum + HTMX)	Routes, handlers, templates
`tpt-syntaxis-cli`	Command-line interface (`tpt` binary)	`Cli`, `Commands`
`tpt-syntaxis-profile`	Tactic profiling, timing	`Profiler`, `ProofProfile`, `TacticStats`
`tpt-syntaxis-viz`	Proof tree SVG/ASCII/JSON	`ProofTree`, `ProofTreeNode`
`tpt-syntaxis-coverage`	Mathlib coverage analysis	`CoverageAnalyzer`, `DependencyGraph`
`tpt-syntaxis-suggest`	Tactic recommendation engine	`Recommender`, `Recommendation`
`tpt-syntaxis-crossprove`	Lean/Coq/Isabelle translation	`CrossProver`, `TacticTranslator`

Crate Dependency Graph

tpt-syntaxis-crossprove (standalone)
tpt-syntaxis-forge (standalone)
tpt-syntaxis-extract (standalone)
    ↓
tpt-syntaxis-minimize → tpt-syntaxis-bridge
tpt-syntaxis-audit → tpt-syntaxis-extract
tpt-syntaxis-profile → tpt-syntaxis-minimize
tpt-syntaxis-viz → tpt-syntaxis-minimize
tpt-syntaxis-coverage → tpt-syntaxis-extract
tpt-syntaxis-suggest → tpt-syntaxis-extract, tpt-syntaxis-core
    ↓
tpt-syntaxis-core → tpt-syntaxis-bridge, tpt-syntaxis-forge, tpt-syntaxis-extract,
                     tpt-syntaxis-minimize, tpt-syntaxis-audit
    ↓
tpt-syntaxis-publish → tpt-syntaxis-core, tpt-syntaxis-audit
tpt-syntaxis-dashboard → all above
tpt-syntaxis-cli → all above

Configuration

Edit config.toml to configure the system:

[discovery]
backend = "hybrid"  # "symbolic" | "ai" | "hybrid"

[ai.openrouter]
api_key = "${OPENROUTER_API_KEY}"
conjecture_model = "anthropic/claude-3.5-sonnet"
tactic_model = "meta-llama/llama-3.1-405b-instruct"
compass_model = "deepseek/deepseek-r1"
base_url = "https://openrouter.ai/api/v1"

[ai.parameters]
temperature = 0.7
max_tokens = 1024

[search]
max_branches = 16
beam_width = 5
timeout_seconds = 300

[publish]
mathlib_repo = "leanprover-community/mathlib4"
auto_pr_on_open_problem = true

[dashboard]
host = "127.0.0.1"
port = 3000

Environment Variables

Variable	Required	Description
`OPENROUTER_API_KEY`	For AI/Hybrid mode	API key from openrouter.ai

Examples

Run the examples to see each capability in action:

# Solve a simple theorem
cargo run --example solve_simple

# Build a Mathlib index and search
cargo run --example index_mathlib

# Minimize a verbose proof
cargo run --example minimize_proof

# Audit a proof for safety
cargo run --example audit_proof

# Render a proof tree
cargo run --example proof_tree

# Profile tactic execution
cargo run --example tactic_profile

# Get tactic recommendations
cargo run --example recommend_tactics

# Generate a coverage report
cargo run --example coverage_report

# Translate Lean proof to Coq/Isabelle
cargo run --example translate_proof

Example: Solving a Theorem

use tpt_syntaxis_core::backend::{SymbolicBackend, DiscoveryBackend};
use tpt_syntaxis_bridge::LeanTacticState;

#[tokio::main]
async fn main() {
    let backend = SymbolicBackend::new();
    let state = LeanTacticState {
        goals: vec![tpt_syntaxis_bridge::LeanGoal {
            name: None,
            hypothesis: vec![],
            target: "1 + 1 = 2".to_string(),
        }],
        messages: vec![],
        tactic_pos: None,
    };

    let suggestions = backend.suggest_tactics(&state, 5).await.unwrap();
    for (i, tactic) in suggestions.iter().enumerate() {
        println!("{}. {}", i + 1, tactic);
    }
    // Output:
    // 1. simp [Nat.add_zero]
    // 2. norm_num
    // 3. omega
    // 4. ring
    // 5. linarith
}

Example: Minimizing a Proof

use tpt_syntaxis_minimize::{TacticProof, Minimizer};

let code = r#"theorem add_zero (a : Nat) : a + 0 = a := by
  have h : a + 0 = a := by simp [Nat.add_zero]
  exact h
  done"#;

let proof = TacticProof::parse(code);
let minimizer = Minimizer::new();
let result = minimizer.minimize(&proof).unwrap();

// Original: 4 steps → Minimized: 2 steps (50% compression)

How It Works

1. Conjecture Generation

The system generates candidate theorems using:

Symbolic patterns: Commutativity, associativity, identity elements
AI Compass (hybrid mode): LLM suggests strategy metadata — never tactic code
Mathlib gaps: Targets unresolved sorry statements

2. Proof Search

Two search algorithms explore the tactic space:

Production MCTS: PUCT selection, transposition tables, time budgets, progressive widening, heuristic rollouts
Beam Search: Top-K branch exploration with heuristic scoring

The DiscoveryBackend trait provides tactic suggestions:

#[async_trait]
pub trait DiscoveryBackend: Send + Sync {
    async fn suggest_tactics(&self, state: &LeanTacticState, n: usize)
        -> Result<Vec<String>>;
    fn estimate_value(&self, state: &LeanTacticState) -> f64;
    fn state_hash(&self, state: &LeanTacticState) -> u64;
}

3. Kernel Verification

The search backends propose candidate tactic sequences using cheap heuristics — they never touch the real elaborator. Before a candidate is ever recorded as a discovery, tpt-syntaxis-core::verify compiles it as a real theorem (lake env lean against the project's Mathlib dependency) and only accepts it if the Lean 4 kernel actually checks it. A heuristic "success" that doesn't survive this step is discarded, never recorded — the kernel is the sole source of truth, not the search's own opinion of itself.

4. Proof Minimization

Raw proofs (often hundreds of brute-forced steps) are compressed:

Parse into individual tactic steps
Try replacing N-step windows with single power tactics
Verify each replacement via TacticVerifier
Recurse until no further compression

5. Significance Classification

Discoveries are classified into five tiers:

Tier	Criteria	Action
Trivial	≤ 2 steps, standard tactics	Log only
KnownVariant	Slight rewording of existing theorem	Log only
NovelButSimple	New, follows from known results	Dashboard review
NovelAndDeep	New, non-obvious strategy required	Priority review
OpenProblem	Resolved a known Mathlib `sorry`	Priority submission

6. Publication

Approved discoveries are formatted and submitted:

Mathlib PR: GitHub API integration with standard PR template
arXiv preprint: LaTeX formatted for cs.LO / math.LO
Journal submission: Templates for JFR, LMCS, JAR

For Developers

Development Setup

# Clone and build
git clone https://github.com/anthropics/tpt-syntaxis.git
cd tpt-syntaxis
just build

# Run all tests (100+ tests)
just test

# Lint
just clippy
just fmt-check

Build Commands

Command	Description
`just build`	Build everything (Lean + Rust)
`just build-rust`	Build Rust workspace only
`just build-lean`	Build Lean project only
`just test`	Run all Rust tests
`just test-lean`	Run Lean tests
`just clippy`	Run clippy with warnings as errors
`just fmt`	Format all code
`just fmt-check`	Check formatting without modifying
`just run`	Run the discovery engine
`just dashboard`	Start the review dashboard
`just publish-dry-run`	Verify crates.io publishing
`just clean`	Clean build artifacts

Architecture Principles

100% Rust — no Python, no Node.js anywhere in the toolchain
AI is optional — symbolic mode runs with zero API calls, zero cost, fully deterministic
Lean kernel is the sole source of truth — no component bypasses it
AI never writes proof code — only tactic suggestions or compass metadata
Human-in-the-loop — no auto-publish bypass; dashboard gates all publication

CI/CD

GitHub Actions runs on every push:

cargo fmt --all -- --check
cargo clippy --workspace -- -D warnings
cargo test --workspace
lake build + lake env lean --run lean-src/Main.lean
cargo publish --dry-run (PRs only)

Tag-triggered release workflow publishes to crates.io in dependency order.

License

MIT OR Apache-2.0

tpt-syntaxis

Languages