Verify Claim
verify_claimVerify a stated mathematical claim and get an honest verdict—proved, refuted, supported, or undecided—with evidence.
Instructions
Independently re-check a stated mathematical claim and report how far the evidence goes: proved, refuted, supported or undecided.
Use this to verify your own algebra before presenting it. The claim is a single comparison in Sage syntax -- an equality, an inequality, or anything that evaluates to True/False:
integral(x^2/(e^x-1), x, 0, oo) == 2*zeta(3) sin(x)^2 + cos(x)^2 == 1 pi < 22/7 e^pi != pi^e
The check climbs a ladder: Sage's symbolic prover, the exact difference ((lhs-rhs).simplify_full().is_zero()), exact arithmetic over QQbar/AA when the claim is constant, then certified interval arithmetic and numeric sampling over the free variables. Verdicts are honest by construction: 'proved' and 'refuted' are exact decisions ('refuted' always exhibits its counterexample or certified enclosure); 'supported' means the numeric evidence is consistent with the claim without proving it, and says how many samples at what precision; 'undecided' means every rung was inconclusive -- it never means false.
Exactness is never assumed. Decimal literals are read exactly (0.1 means 1/10, never the 53-bit double), and a comparison whose operands are machine floats (RR/RDF/CC, an .n() result) is reported as 'supported' over inexact numbers, never as an exact proof -- state it over ZZ/QQ/QQbar or symbolically for an exact verdict. The session's active assumptions (assume(x > 0), assume(x, 'integer')) are honored: a sampled counterexample must lie inside the stated domain, and any verdict that relied on an assumption names it in the evidence.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| claim | Yes | The claim to check, as a single comparison, e.g. 'sin(x)**2 + cos(x)**2 == 1' | |
| samples | No | Sample points per free variable sweep when the claim cannot be decided exactly | |
| session | No | Workspace to use, as a name or a portable handle. Workspaces have independent variables. A name is scoped to this MCP session; a handle returned by start_sage_session (workspace_token) reaches the same workspace across reconnects and is a bearer credential -- keep it secret. Omit for 'default'. | default |
| timeout | No | Override the evaluation timeout in seconds | |
| precision_bits | No | Precision of the certified interval arithmetic behind numeric verdicts |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| claim | Yes | The claim that was checked, whitespace-folded. | |
| method | No | The rung that decided: exact_comparison, symbolic_prover, exact_difference, exact_algebraic, certified_interval, numeric_sampling, float_comparison (operands were machine floats, so the result is only supported, never exact) or exhausted. | |
| samples | No | Number of sample points supporting a numeric-sampling verdict. | |
| verdict | Yes | proved/refuted are exact; supported is evidence short of proof; undecided means every rung of the ladder was inconclusive. | |
| evidence | No | What the deciding rung actually established, including the counterexample for a sampled refutation. | |
| assumptions | No | The session's active assumptions in force during the check (e.g. "x is integer"). A verdict is only valid under these; they are also named in the evidence so no branch can conceal them. | |
| precision_bits | No | Interval-arithmetic precision behind a numeric verdict. |