Reason ATP
Autonomous Theorem Proving & Symbolic Regression

---

Reason ATP discovers, validates, and formalizes mathematical theorems autonomously. It combines multi-agent reasoning, symbolic regression (SciPy + PySR), formal verification (Lean 4), and LLM-guided analysis into a single pipeline — from raw numerical data to publication-ready proofs.

Built at Artifact Virtual. Used in production to analyze GLADIUS/WYRM neural kernel training dynamics — predicting loss trajectories, specialist emergence, and phase transitions from live training telemetry.

What It Does

Input: numerical data, training logs, time series, raw observations.

Output: discovered equations, validated theorems, formal proofs, LaTeX papers.

Data → Multi-Agent Reasoning → Symbolic Regression → Theorem Generation → Formal Verification → Paper

Core Capabilities

• Symbolic Regression — SciPy curve fitting engine with 15+ functional forms (power law, sigmoid, log-decay, double exponential, piecewise, etc.). Scores fits by R², AIC, BIC. Fast — runs in seconds on CPU.
• Multi-Agent Reasoning — Hypothesis generator, validator, meta-reasoner, hallucination detector, consensus builder. Agents cross-validate independently before any claim propagates.
• Formal Verification — Lean 4 interface for proof checking. Simulation fallback when Lean isn't available.
• Autonomous Research Loop — Generate conjecture → validate → refine → abandon/publish. Up to 10 iteration cycles per theorem.
• Paper Generation — LaTeX/PDF output with professional structure, equations, and diagrams.

Real-World Application: GLADIUS Training Analysis

Reason ATP's primary deployment is analyzing GLADIUS (cognitive kernel) training runs:

• Loss trajectory prediction — fit training curves to functional forms, predict convergence
• Specialist scale dynamics — model how Synthase specialist weights evolve across depth bands
• Phase transition detection — identify critical points where training behavior shifts
• Depth profile analysis — characterize self-organizing depth spread via PUP uncertainty

Results from Day 52+ analysis: predicted v5 BPE loss plateau at ~10.37 (random chance), confirmed by actual training data. Identified dead specialist scales (S0/S3 grad=0) before manual inspection caught them.

Quick Start

git clone https://github.com/amuzetnom02/reasonatp.git
cd reasonatp
pip install -r requirements.txt

Run Symbolic Analysis (fast, no LLM needed)

from search.scipy_regressor import ScipyRegressor

regressor = ScipyRegressor()
x = [100, 500, 1000, 2000, 5000, 10000]
y = [8.2, 6.1, 5.3, 4.8, 4.5, 4.3]

results = regressor.fit_all(x, y)
for r in results[:3]:
    print(f"{r.name}: {r.equation}  (R²={r.r_squared:.4f})")

Run Full ATP Pipeline

python run_system.py              # Complete analysis
python run_research.py            # Autonomous theorem discovery

API Server

uvicorn main:app --reload         # FastAPI on :8000

import httpx
r = httpx.post("http://localhost:8000/reason", json={
    "data": [1, 4, 9, 16, 25, 36],
    "context": "Perfect squares"
})

Architecture

reasonatp/
├── core/                          # Reasoning engines
│   ├── reasoning_orchestrator.py  # Main orchestration pipeline
│   ├── research_orchestrator.py   # Autonomous research loop
│   ├── multi_agent_system.py      # Agent coordination
│   ├── theorem_generator.py       # Conjecture generation
│   ├── iteration_engine.py        # Validate/refine cycles
│   ├── paper_generator.py         # LaTeX output
│   ├── symbolic_regressor.py      # PySR integration
│   ├── abductive_engine.py        # Abductive reasoning
│   ├── analogical_engine.py       # Analogical reasoning
│   ├── meta_reasoner.py           # Meta-cognitive analysis
│   └── specialized_math/          # Calculus, optimization, physics
├── search/                        # Regression backends
│   ├── scipy_regressor.py         # SciPy curve fitting (15+ forms)
│   ├── scoring_engine.py          # R², AIC, BIC scoring
│   └── candidate_space.py         # Search space management
├── llm/                           # LLM integration
│   ├── llm_service.py             # Provider abstraction
│   ├── gpt_wrapper.py             # OpenAI/compatible API
│   ├── autoformalizer.py          # Natural language → formal logic
│   └── prompt_templates.py        # Structured prompts
├── proofs/                        # Formal verification
│   └── lean_interface.py          # Lean 4 bridge
├── cli/                           # CLI commands
├── utils/                         # Config, logging, exceptions
├── data/                          # Analysis outputs
├── run_system.py                  # Full pipeline runner
├── run_research.py                # Autonomous research
└── main.py                        # FastAPI server

Regression Engine

The SciPy regressor fits 15+ functional forms simultaneously and ranks by information criteria:

Form	Equation	Use Case
Power Law	a·x^b + c	Loss decay
Log Decay	a·ln(x+1) + b	Diminishing returns
Exponential Decay	a·e^(-bx) + c	Convergence
Double Exponential	a·e^(-bx) + c·e^(-dx) + e	Two-phase dynamics
Sigmoid	a/(1+e^(-b(x-c))) + d	Phase transitions
Piecewise Linear	a·x + b (x<c), d·x + e (x≥c)	Regime changes
Tanh Growth	a·tanh(b(x-c)) + d	Bounded growth
Logistic	K/(1+e^(-r(x-x₀)))	Capacity-limited
Stretched Exponential	a·e^(-(x/τ)^β) + c	Anomalous relaxation
Rational	(a·x+b)/(x+c)	Asymptotic
Sqrt Decay	a/√(x+b) + c	Sublinear decay
Polynomial (2-4)	Σ aᵢxⁱ	Local fitting

Each fit returns R², AIC, BIC, residual std, and predicted values at arbitrary future points.

Performance

Operation	Time	Hardware
SciPy regression (15 forms)	< 1s	CPU
Conjecture generation	~50ms	CPU
Full iteration cycle	~100ms	CPU
Paper generation (LaTeX)	~3ms	CPU
End-to-end research	< 1s	CPU
GLADIUS training analysis	< 30s	CPU

Testing

pytest tests/ -v                          # All tests
pytest tests/ --cov=core --cov=search     # With coverage

23/23 tests passing.

Citation

@software{reasonatp2026,
  title   = {Reason ATP: Autonomous Theorem Proving and Symbolic Regression},
  author  = {Artifact Virtual},
  year    = {2026},
  version = {1.2.0},
  url     = {https://github.com/amuzetnom02/reasonatp}
}

License

MIT. See license.md.

---

_{Artifact Virtual — commit.}