Graviterra

Formalization · Proof · Research

Open tools for
formal mathematics.

We build open-source formalization tools and systems that help turn mathematical ideas into formal statements and checked proofs.

Our current focus: formalization, autonomous theorem proving, and tools for mathematical research.

Explore the prover Our research

Featured tool

v1.17 · MIT

Ensemble Prover

Autonomous proof search.
Mathematics you can inspect.

672Putnam problems with saved solutionsCumulative across models · October 7, 2026
Proof graph with a selected helper and its Lean statement and proof.
Follow the proof. Open the helpers. Inspect the Lean.
Actual interface, illustrative example records.
Explore Ensemble Prover
Walk through a real proofView source ↗

Research

The Ensemble

The Ensemble is a reference design for adaptive systems. It explores how a system can generate alternatives, evaluate evidence, and choose its next action within explicit constraints.

ExpandEvaluateSelect

A visualization of the research concept.

Explore alternatives. Give competing hypotheses and approaches room to develop.

Use the right checks. Keep formal proof, empirical evidence, and unresolved claims distinct.

Adapt within limits. Let recorded outcomes guide the next action while preserving the application's rules and resource bounds.