Theoria

Theoria interface, deep math proof reasoning
Generate tex in Theoria
Theoria welcome

Inspiration

I teach undergraduate mathematics at the University of Zimbabwe — Real Analysis, Linear Algebra, ODEs/PDEs, Optimization — while pursuing a Ph.D. in Pure Mathematics at Rhodes University on separation axioms in the category of S-frames. In Zimbabwe, the bottleneck for my students is rarely talent. It is access: unstable connectivity, no GPU budget, and cloud tutors that vanish when data runs out.

That classroom reality is the brief for Theoria: an offline math & scientific reasoning assistant that fits the ADTC Standard Laptop (8 GB RAM, integrated graphics, Ubuntu). As someone who also reviews LLM-generated proofs (topology, logic, PDEs) for industry, I see daily how fluent text can still be wrong. Theoria’s goal is not a chat novelty — it is a private tutor that students can trust when the network is gone.

What it does

Theoria runs a compact GGUF model through llama.cpp and wraps it with load-bearing tools:

SymPy for exact algebra, derivatives, and integrals (verification badge + fallback)
Local RAG over curated math corpora and user PDFs
Lean4 (TheoriaKit) for small formal checks where we can say “proved,” not only “plausible”
Offline UI with KaTeX so answers render as real mathematics, e.g. solving $$x^{2}-5x+6=0 \quad\Rightarrow\quad x\in{2,3}$$ or differentiating via the chain rule $$\frac{d}{dx}\sin(x^{2})=\cos(x^{2})\cdot 2x.$$

How we built it

We bake-off’d small open models under ADTC constraints and shipped a model (~1.9 GB peak RSS on an 8 GB VM, ~11 tok/s generation). Stack: FastAPI + persistent llama-server, intent routing (so “hello” is not answered with a fake proof), SymPy/Lean tool loop, and a lightweight web UI. Telemetry is self-checked with the official profiler against the 7 GB ceiling and the fixed speed reference $$ S_{\mathrm{perf}}=\min!\Bigl(\frac{\mathrm{TPS}}{15},1\Bigr)\times 100,\qquad S_{\mathrm{eff}}=\frac{7-\mathrm{PeakRAM}_{\mathrm{GB}}}{7}\times 100. $$

Challenges we ran into

Accuracy vs. size — a 1.7B model cannot replace a lecturer; tools must carry exactness.
Fine-tuning risk — an aggressive QLoRA mix collapsed generation
Scoring honesty — the app helps students; audit metrics are model-only. We designed prompts and REPORT numbers for the naked GGUF on 8 GB-class hardware (VM thermals (N/A); physical audit applies (P_{\mathrm{thermal}})).

What we learned

On-device AI for Africa is a systems problem: model choice, quantization, RAM, and verification matter more than a flashy UI. Coming from time-scale calculus and pointfree topology into llama.cpp taught me the same lesson I give my students — beautiful arguments fail if they are not checked. Theoria is my attempt to put that discipline on every desk that already has an 8 GB laptop.