Start with the failure it exists to catch

This is the clearest way to explain what certo is for.

Here is the shape of a Lean theorem. It has no sorry. It audits clean on #print axioms — [propext, Classical.choice, Quot.sound], everything a formalisation is supposed to look like.

theorem main (dens : ℝ)
    (dens_high : dens ≥ 3/4)      -- the regime the paper works in
    (sparse    : dens ≤ 1/2)      -- ...and a bound from section 2
    : conclusion := by
  linarith [dens_high, sparse]

It is also about nothing. Its hypotheses contradict each other, so it would have proved any goal at all. A user had two modules like it. Another line produced four.

certo asks that question directly, and answers it in milliseconds:

$ certo prove regime.py
PROVED -- symbolic and universal under the hypotheses  [unsat]
  VACUOUS: these hypotheses contradict each other, so this goal -- and
  every other goal -- follows. The proof is valid and says nothing.
  The clash is: dens_high, kappa_small

Note the second line. It does not just say “empty” — it names the minimal clashing set, so the next question is already answered. And the flag travels in the certificate, so it keeps saying so months later, when only the artefact remains.

The idea: a verdict you can re-check

A verdict you cannot re-check is a rumour.

Every command writes an artefact. Most of them re-check with nothing but arithmetic — no Z3, no CBC, nothing to take on trust:

$ certo verify out/lp.json
VALID  lp_dual certificate (verified without a solver)
  [ok] primal feasibility (A x <= b)
  [ok] dual feasibility (A^T y >= c)
  [ok] exact strong duality (c.x == b.y)  (c.x=25/2 | b.y=25/2)
  EXACT rational arithmetic, no tolerances

That matters for two different people. For you, it is a safety net: if the solver had a bug, the certificate would not verify and you would get ERROR, not PROVED. For whoever reads your paper, it is the difference between an assertion and something they can check on their own machine without running your code.

The arc

Six things you do between an idea and a proof.

• FindIs there an object like this? What is the best one? the object itself — and with mixed --prove-optimal, a proof that it is the best
• BreakIs this claim actually true? a counterexample with concrete values, in milliseconds
• MeasureNot whether it fails — how much, and where is it worst? exact min, max and mean, and the extreme instances by name
• ReduceNinety counterexamples. How many objects is that really? orbits under your symmetry, and one minimal witness per orbit
• EstablishIs it true for every case, every n, exactly? DRAT proofs, induction with the chain checked, Farkas multipliers, Gröbner cofactors, rigorous enclosures
• AssembleWhat does my project rest on, and what do I still owe? the proof with every bridge named, and a report of what is still assumed

Two minutes

pip install "certo-math[mcp,numerics]"

certo core examples/amgm.py

PROVED -- symbolic and universal under the hypotheses  [unsat]
  hypotheses needed: a_pos, b_pos, c_pos | redundant: noise

A spec is ordinary Python. There is no bespoke language, because an LLM writes Python far better than it writes SMT-LIB:

import z3
from certo import Spec

def spec():
    a, b, c = z3.Reals("a b c")
    s = Spec()
    s.assume("a_pos", a > 0)      # NAMED: core reports on them
    s.assume("b_pos", b > 0)
    s.assume("c_pos", c > 0)
    s.claim((a+b)*(b+c)*(a+c) >= 8*a*b*c)
    return s

Find the command by the question

Read the question, not the name. certo commands prints this in your terminal, in your language.

You want to ask	Command
Is this claim true under these hypotheses?	prove
Which of my hypotheses does it actually need?	core
Does every hypothesis earn its place, or is my theorem overstated?	audit
Is my regime non-empty at all?	check --hypotheses-only
What is the optimum, exactly?	opt
Does this term decay in n, or is it Θ(1)?	order
I checked it for p = 5..12. Does it hold for every p?	parametric
Does it hold for every graph on n vertices?	sweep
A thousand failures — how many objects is that?	sweep --witnesses
“By symmetry” — is that step actually sound here?	reduce
How do I assemble my lemmas into one proof?	compose
Is this spec well-posed, before I spend the compute?	lint

All forty-three, each with what it does not establish, in the command reference.

What it does not do

This matters as much as the command list.

The hard limit is asymptotic statements with quantifiers over n. The ladder, with Ramsey numbers:

Question	certo?
Is R(3,3) ≤ 6?	Yes. cases, a 23-line DRAT proof, verified
Is R(3,3) = 6?	Yes. bisect, certified on both sides
Is R(5,5) ≤ 48?	Not in practice. Finite, but the space is 2903
Does R(k,k)1/k converge?	No, in principle. Asymptotic: not expressible

certo is not a proof assistant — that is Lean, Rocq or Isabelle — nor a computer algebra catalogue. It is the layer before: discover objects, destroy false formulations and minimise hypotheses before paying the cost of formalising them.