formalware.ai

Tools and results for the formalization of mathematics… and everything else.

We build systems that turn research papers into reliable, machine-checked proofs — and we publish the formalizations they produce.

See the results Explore the tools

Tools

Software for autoformalization

Our flagship system, Trellis, formalizes mathematics with LLM agents constrained inside a deterministic, kernel-verified workflow.

Trellis

Autoformalization system

Trellis leverages LLM agents in a deterministically constrained workflow to produce machine-checked Lean proofs from research papers. Its design goal: make it routine to elaborate any part of a proof in further detail, so that what the system outputs is genuinely trustworthy.

Work is organized as a Proof Tablet — a directed acyclic graph of nodes pairing natural-language statements with their Lean counterparts. A deterministic kernel (written in Rust, with a TLA⁺ specification) supervises a worker, verifier lanes, a reviewer, and an isolated Lean checker.

arXiv Read the paper ↗ GitHub & TLA⁺ spec

Results

Formalized papers

Complete research papers, formalized end-to-end and verified by the Lean kernel.

Ramsey theory

Nearly Tight Exponents for Off-Diagonal Ramsey Numbers

Domagoj Bradač

Formalized directly from the original arXiv v1 source — no human-supplied proof steps.

arXiv Paper ↗ GitHub ▦ Proof viewer

Ramsey theory

Improving R(3,k) in Just Two Bites

Zion Hefty · Paul Horn · Dylan King · Florian Pfender

Completed during active development of Trellis; structural finishing was human-directed, with no mathematical content or proof steps supplied by hand.

arXiv Paper ↗ GitHub ▦ Proof viewer