Thesius Suite

A local-first theorem and proof research workbench.
Explore the docs »

View Usage · Report Bug · Request Feature

Table of Contents

1. About The Project
   • Built With
2. Getting Started
   • Prerequisites
   • Installation
3. Configuration
4. Usage
5. Deployment
6. Testing
7. Roadmap
8. Contributing
9. License
10. Contact
11. Acknowledgments

About The Project

Thesius Suite is a local-first research workbench for theorem and proof exploration. It combines a Python command-line interface, an interactive terminal UI, a SQLite theorem codex, browser-friendly UIs, and research-agent components into one repository.

The project is organized around a few practical goals:

• keep theorem data available locally in SQLite;
• expose the codex through CLI, TUI, Datasette, and Streamlit workflows;
• support LangGraph and LangChain research-agent experiments;
• keep CAS and formalization hooks close to the theorem corpus;
• avoid shell-script-only workflows by providing Python entry points.

Core project documentation lives in docs/, while reusable research components live in components/.

(back to top)

Built With

• Python
• Typer
• Rich
• SQLite
• Datasette
• Streamlit
• LangGraph
• LangChain
• pytest

(back to top)

Getting Started

Follow these steps to install Thesius locally and initialize the theorem codex.

Prerequisites

• Python 3.10 or newer
• Git
• Optional: API credentials for any agent workflows that call external model providers

Installation

1. Clone the repo.

   git clone git@github.com:aconsapart/thesys.git
   cd thesys

2. Create and activate a virtual environment.

   python -m venv .venv
   source .venv/bin/activate

3. Install the package with test and agent dependencies.

   pip install -U pip
   pip install -e ".[test,agents]"

4. Initialize the theorem codex.

   thesius init

You can also initialize the codex with Python only:

python -m scripts.init_codex

(back to top)

Configuration

Thesius stores the default SQLite database path in config/local_cli_settings.json. That local settings file is ignored by git.

Set a default database once:

thesius config set-db proof_codex.sqlite

Inspect the configured database:

thesius config get-db
thesius config show

Every command uses the configured database by default. Override it for a single command with --db:

thesius status --db another_codex.sqlite

Initialize and save a database path in one step:

thesius init --db proof_codex.sqlite --save-db

See config/local_cli_settings.example.json for a local settings template.

(back to top)

Usage

Start the command-line TUI:

thesius tui

Common TUI commands:

status
frontier
strategies
show <theorem_slug>
add-attempt <theorem_slug> <strategy_slug> <STATUS> <text...>
add-falsification <theorem_slug> <strategy_slug> <SEVERITY> <text...>
quit

Run direct CLI commands:

thesius status
thesius frontier
thesius strategies
thesius theorem exact-short-box-product-fiber-curve-intersection

Launch browser UIs without shell scripts:

thesius serve streamlit
thesius serve datasette

Run the generic workbench agent:

thesius run workbench \
  --iterations 3 \
  --parallel-strategies 3 \
  --out runs/workbench_example

More details:

• docs/PYTHON_TUI.md
• docs/DATABASE_SETTING.md
• docs/INTEGRATION_GUIDE.md
• docs/COMPONENTS.md
• docs/TESTING.md

(back to top)

Deployment

Deploy the Theorem Codex dashboard as a website with Docker:

THESIUS_PASSWORD=change-me docker compose up --build

The app serves on port 8501 with the SQLite database on a persistent volume, and requires the password whenever THESIUS_PASSWORD is set. Google/OIDC single sign-on is also supported via Streamlit secrets (see .streamlit/secrets.example.toml).

Follow the step-by-step runbook in DEPLOY.md to go live on Fly.io, Render/Railway, a VPS, or Streamlit Community Cloud; reference details are in docs/DEPLOYMENT.md.

(back to top)

Testing

Run the test suite from the project root:

pytest -q

If the package is not installed in the active environment, run tests against the source tree:

PYTHONPATH=src pytest -q

(back to top)

Roadmap

• Package the Thesius CLI as a Python entry point
• Add a Python TUI for codex workflows
• Add local database configuration
• Add Datasette and Streamlit launch commands
• Include research-agent components
• Expand automated coverage for agent and UI workflows
• Add more formalization and CAS integration examples

See the open issues for proposed features and known issues.

(back to top)

Contributing

Contributions should keep the project local-first, Python-driven, and easy to test.

1. Fork the project.
2. Create your feature branch (git checkout -b feature/amazing-feature).
3. Commit your changes (git commit -m 'Add amazing feature').
4. Push to the branch (git push origin feature/amazing-feature).
5. Open a pull request.

Before opening a pull request, run:

pytest -q

(back to top)

License

Distributed under the MIT License. See LICENSE.txt for more information.

(back to top)

Contact

Project Link: https://github.com/aconsapart/thesys

(back to top)

Acknowledgments

This project builds on the Python scientific and developer tooling ecosystem, including Typer, Rich, SQLite, Datasette, Streamlit, LangGraph, LangChain, and pytest.

The README layout follows the structure of Best-README-Template.

(back to top)