theorialabs.
TOOLS FOR THE NEXT DISCOVERY

Verifiable
research loops

A Lean-native coding agent for
mathematics and theoretical sciences.

Explore the unknown. Formalize your thinking.
Build on results you can verify.

Meet Theoria-CLI
THE SHAPE OF AN IDEAFIG. 01 / PERIODIC SHEAR
yx →
x′ = (x + s·y) mod L / structure, transformed.
BUILT FOR RIGOR. DESIGNED FOR DISCOVERY.LEAN 4 + MATHLIB + YOUR CURIOSITY

CORE DOMAINS / WHO IT’S FOR

Different fields.
The same rigor.

For researchers, builders, and teams
working at the edge of what we know.

01 /

Mathematical research

Explore conjectures, discover useful lemmas, and develop machine-checked proofs.

Mathematicians & formalizers
02 /

Theoretical physics

Connect mathematical structures, formal reasoning, and computational experiments.

Physicists & research groups
03 /

Computer Science

Reason about algorithms, formal methods, and the foundations of computation.

Theorists & verification teams
04 /

Foundations of AI/ML

Investigate learning theory, test hypotheses, and build reproducible research loops.

AI & machine learning researchers
05 /

Quant Finance

Develop mathematical models and evaluate the assumptions behind quantitative strategies.

Quants & quantitative researchers

01 / THE RESEARCH TOOLKIT

Go further.
Stay grounded.

An agent that speaks mathematics.
A workflow that checks its work.

01

Lean, natively.

Your toolchain is part of the agent. Work with Lean, Lake, and Mathlib, with real compiler feedback at every step.

NATIVE TOOLCHAIN
02

A thought. A theorem.

Turn informal mathematics into formal statements. Let the agent propose, check, and refine proofs in a Lean-driven loop.

AUTOFORMALIZATION & PROOF LOOPS
03

Research with context.

Explore the literature, connect relevant results, and bring the mathematical context back into your research workflow.

LITERATURE SEARCH
04

The right lemma, found.

Built-in Mathlib search engines and Lean language-server integration put existing definitions and useful lemmas within reach.

MATHLIB SEARCH & LSP
05

Measure what matters.

Run integrated Lean mathematical benchmarks. Compare proof outcomes and research workflows in reproducible environments.

MATHEMATICAL BENCHMARKS
06

Stay in the loop.

Follow long-running work and interact with supported research workflows from your phone through the Telegram connector.

TELEGRAM CONNECTOR
07

Your models. Your machine.

Work with local models on your own hardware. Keep model inference close to your research and choose the setup that fits your workflow.

LOCAL MODEL SUPPORT
08

From your laptop to the cluster.

Native integration with HPC resources connects your research to SLURM-managed systems and Ray compute clusters. Scale experiments and compute-intensive workflows on your own infrastructure.

HPC & DISTRIBUTED COMPUTE

SHARED WORKSPACES / THEORIA-IDE

Great ideas rarely happen alone.

Bring your team into the same research workspace. Connect projects, conversations, and results—with shared context from the first question to the final proof.

↗

02 / FROM INTUITION TO VERIFICATION

Follow the idea.
Check every step.

You bring the question.
Theoria helps you work through it.

  1. 01

    Start with a question

    A conjecture, a paper, an informal argument. Give your research a direction.

  2. 02

    Make it precise

    Search for useful results and turn your mathematical intent into Lean.

  3. 03

    Close the loop

    Propose a proof. Read Lean’s feedback. Refine until the statement checks.

theoria / a small example↗

# Every discovery starts somewhere.

❯ Prove that the sum of two even
  natural numbers is even.

Θ

Let’s make that precise.

import Mathlib

theorem even_add
    (a b : ℕ)
    (ha : Even a) (hb : Even b) :
    Even (a + b) := by
  exact ha.add hb
✓ Lean check passed · no sorry

ILLUSTRATIVE WORKFLOW / LEAN 4 + MATHLIB

A FEW COMMANDS. A FULL RESEARCH LOOP.

/formalize
Turn an informal statement into precise Lean.
/prove
Build a proof and refine it with Lean’s feedback.
/benchmark
Run mathematical benchmarks and compare results.

03 / A HOME FOR YOUR RESEARCH

The bigger
picture.

The terminal is just the beginning. Theoria-IDE connects your research in a graphical workspace built for deep, collaborative work.

  • Projects, papers, and proofs in context
  • A connected research graph
  • Multi-user team workspaces
DESKTOP PREVIEW / IN DEVELOPMENT

04 / YOUR NEXT QUESTION STARTS HERE

Make room
for discovery.

A familiar terminal.
An entirely new research companion.

Your terminal. A deeper way to think.

The Lean-native research agent, right where you work. Formalize statements, discover lemmas, and iterate on proofs with feedback from Lean.

PLANNED INSTALL COMMANDCOMING SOON
curl -fsSL https://<your-domain>/install/cli.sh | bash

Current source requires Node.js 22.19+. Public installer coming soon.

Public downloads will appear here when releases are ready.