The example is copied to the build directory during configuration.
You can execute it using
    python example.py
in the build directory after you build Z3.

Proof regression testing
------------------------

The proof matrix runner, its tests, and the proof canaries live in Z3Prover/z3test:
https://github.com/Z3Prover/z3test/blob/master/scripts/proofs/README.md

Z3's CI invokes those tests against the freshly built Z3 executable and runs
the canary lists in the releaseClang configuration. The prooflogs.py and
proofreplay.py examples remain here.

Native Boolean proof certificates
--------------------------------

proof_certificate.py exports a native Z3 proof DAG as JSON. It is a first
milestone toward independent proof checking, not a Lean proof or a verified
unsat verdict. Every bundle explicitly has verification = "unverified".
For every fragment it can use the legacy proof objects of the smt core in a
separate proof-enabled context, without changing global settings. For
arithmetic and uninterpreted functions it rebuilds the sat.smt clause log by
default, which is also available for propositional input; see "Linear real
arithmetic through the clause log" and "Linear real arithmetic through the
legacy proof object" below.

Build the local Python bindings and examples:

    cmake -G Ninja -S . -B build -DCMAKE_BUILD_TYPE=Release \
        -DZ3_BUILD_PYTHON_BINDINGS=ON
    ninja -C build build_z3_python_bindings build_z3_python_examples

From the repository root, export a proof:

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py - \
        > proof.json <<'SMT'
    (set-option :produce-proofs true)
    (declare-const p Bool)
    (assert p)
    (assert (not p))
    (check-sat)
    (get-proof)
    SMT

Pass a filename instead of "-" to read a file. A successful invocation writes
only the JSON bundle to stdout and exits with status 0. Sat, unknown, unsupported
input, missing proofs, and parse errors produce diagnostics on stderr and exit
with status 2, without a bundle. Check the exit status before consuming output.

The Python entry point is export_certificate(source_smt2).

Input scope
-----------

Input is an SMT-LIB script; the certificate is about one check-sat,
check-sat-using, or check-sat-assuming query of it: the declarations,
definitions, and assertions in scope at that query, plus the query's
assumptions (check-sat-assuming's list, or Z3's check-sat with literal
arguments), each of which becomes one more hypothesis of the theorem. A
script with one query needs nothing; one with several (incremental scripts
with push, pop, reset, reset-assertions) names the query by its zero-based
index (--query N, the query= argument of the Python functions), and the
certificate records it as "query" so that the reconstructor rebuilds the
same snapshot from the original script (proof_certificate.query_snapshot).
push and pop take an optional count, declarations are scoped as in Z3's
default (a constant declared inside a popped scope is gone with its
assertions), reset-assertions behaves as in Z3 rather than as SMT-LIB's
"pop every scope" (it removes every assertion, keeps the declarations and
the open scopes, and a later pop still drops its scope's declarations),
and reset clears everything; a script without any query is one query over
its final state. Queries may be followed by get-proof, get-model, get-unsat-core,
get-assignment, and the script by exit. Declarations, declare-sort with
arity 0, define-sort (plain and parametric aliases, scoped like
declarations and expanded by Z3's parser, so the certificate and the Lean
statement mention only the expanded sorts), define-fun, set-logic, set-info, named assertions, and the
information queries get-info, get-option, and echo are accepted. The
certificate is a
statement about the parsed assertions, checked by Lean, so front matter that
only configures Z3's output, models, resource limits, or search is ignored:
the tactic of check-sat-using, the output queries, and the set-option
commands on an allowlist (_IGNORED_OPTIONS in proof_certificate.py:
produce-models, produce-unsat-cores, produce-proofs, proof, model,
model_validate, print-success, auto-config, timeout, rlimit, random-seed,
smt.arith.solver, smt.random_seed, smt.phase_selection, smt.mbqi,
sat.local_search, and the like, plus the pp.*, model.*, and opt.* families,
by Z3's parameter names with - and _ identified). Options that change how
the input is read (numeral-as-real, int-real-coercions, smtlib2_compliant,
which changes the scanner and the Int/Real coercions, and rewriter.*) and
the proof-production and preprocessing options the exporter sets itself
(sat.smt, solver.proof.*, smt.clause_proof, smt.solve_eqs, combined_solver.*)
are rejected, as is any option not on the allowlist; :global-decls is
accepted with false only, Z3's default scoping. Commands that only print
(get-value, eval, simplify, apply, display, get-assertions) are dropped
unless they contain a :named label, which would define a name in Z3,
define-const is a definition, and the script ends at exit, where Z3's parser
stops. The optimization commands (assert-soft, minimize, maximize,
get-objectives) are dropped the same way: Z3 then optimizes over the
assertions as hard constraints, and the certificate states that those are
contradictory (an unsat that only reports an exhausted Pareto front has none,
as the hard constraints are satisfiable). A pop beyond the open scopes, a
query index the script does not have, several queries without an index, a
malformed define-sort, get-consequences, include, and other commands are
rejected rather than ignored.
Standard semicolon comments, doubled quotes in strings, and quoted symbols are
supported. Quoted symbols have no escape mechanism: backslashes are rejected
and a vertical bar always closes the symbol, matching SMT-LIB 2.5+ and Z3's
scanner. Nonstandard block comments are rejected.

Assertions may use Boolean constants, Boolean variables, not, and, or, implies,
xor (including Z3's one-argument xor, which it reads as the argument itself),
Boolean equality/distinct, and Boolean ite. Propositional input may also use
the pseudo-Boolean constraints at-most, at-least, pble, pbge, and pbeq over
Boolean variables and their negations (integer bounds and coefficients);
they are certified through the legacy proof object only (theory_pb's
th-lemma pb steps), since the sat.smt core compiles them away before its
clause log starts, and Lean values each literal 0 or 1 over Int and proves
those steps and Z3's pseudo-Boolean rewrites by omega. A constraint over
any other argument, or next to arithmetic or uninterpreted functions, is
rejected. The qf_lra fragment adds Real
variables and numerals, sums, differences, negation, multiplication by a
constant (one-argument + and *, which Z3 keeps as written, included),
division by a nonzero constant, Real-valued ite whose condition is
any supported formula, abs (SMT-LIB defines it on Int only; Z3 accepts it
over Real with the same definition, (ite (>= t 0) t (- t))), and the atoms
<=, <, >=, >, =, and distinct over Real terms. The qf_uf fragment adds any
number of uninterpreted sorts with constants, functions, and predicates
whose arguments have uninterpreted
sorts or Bool (functions may map between sorts; a Bool argument is any
supported formula), ite terms over a sort whose condition is any supported
formula, and the atoms = and distinct over terms of one sort. The qf_uflra
fragment is the union of the two: uninterpreted sorts or functions together
with linear real arithmetic, where functions and predicates may also take
Real arguments and return Real (an application with a Real result is an
opaque atom of the linear forms, as in Z3's arithmetic solver); a function
whose signature mentions Real makes the input qf_uflra even without any
Real atom. Predicates whose arguments are all Bool are the qf_uf fragment
even without any uninterpreted sort (qf_uflra when their arguments are Real
atoms); both cores certify them. The qf_lia fragment is linear integer
arithmetic on its own: Int variables and numerals, sums, differences,
negation, multiplication by a numeral, Int-valued ite, integer div and mod
by a nonzero numeral (negative too), Z3's rem by a nonzero numeral, and
abs, and the same atoms over Int
terms; both cores certify it, and a consumer of parse_assertions or
parse_legacy_assertions accepts it explicitly (integer=True, as the
exporter and the reconstructor do), because its cut steps are certified by
Lean alone rather than re-derived in Python first. The qf_uflia fragment is the
Int twin of qf_uflra: uninterpreted sorts or functions together with linear
integer arithmetic, where functions and predicates may take and return Int
(an application with an Int result is an opaque atom of the linear forms),
a function whose signature mentions Int makes the input qf_uflia even
without any Int atom, and a Bool-only predicate over Int atoms belongs here
too; it shares qf_lia's opt-in on both cores. The qf_lira fragment has
Int and Real atoms side by side (the qf_lia and qf_lra shapes, Boolean
structure tying them together), to_real of Int terms (variables, sums,
ite, div, mod, abs) inside Real atoms, and to_int and is_int of linear Real
terms; it shares the opt-in too, and both cores certify it. The
qf_uflira fragment is qf_lira next to uninterpreted sorts and functions:
functions and predicates may take and return Int and Real (both in one
signature too), and an input whose signatures and atoms mention both sorts
is qf_uflira; it shares the opt-in, and both cores certify it. Arrays
whose index and element sorts are uninterpreted, Int, or Real, the element
sort Bool too (sets, (Array Int Bool)) (QF_AX,
QF_ALIA, QF_AUFLIA: (Array Index Element) or (Array Int Int) constants,
select, store, ite over arrays, and equality between arrays) join whichever
UF fragment the rest of the input is in, their uninterpreted index and
element sorts counting as its uninterpreted sorts and an Int or Real one as
its arithmetic (an input with Int arrays alone is qf_uflia); functions and
predicates may take arrays as arguments, functions may return them,
constant arrays ((as const (Array I E)) v) and default values (default a)
are supported over Int and Real indices, and sets combine by maps of not,
and, or, => ((_ map and) a b) and Z3's set operators (union, intersection,
setminus, complement); maps of xor, = and distinct, Int and Real +, -, and
comparisons, ite, and uninterpreted functions and predicates of up to three
arguments apply over elements of an uninterpreted sort, Int, Real, or Bool.
Only the clause log certifies them (the legacy core
rejects them explicitly); arrays may also be indexed by Bool ((Array Bool
Int), see below), and an index or element sort may itself be such an array
((Array Int (Array Int Int)), (Array (Array Int Int) Bool), nested to any
depth); arrays
with several indices, constant arrays and default values over other index
sorts, default values that are arrays, maps of other functions (*, conversions,
uninterpreted functions of four or more arguments) or over arrays of arrays, and as-array are rejected.
Enumeration datatypes (declare-datatype or declare-datatypes whose
constructors are all nullary, not parametric) count as uninterpreted sorts,
so an input with one is in a UF fragment: constants, functions, predicates,
and ite over the enumeration, its constructors, and its recognizers
((_ is c) t or SMT-LIB 2.5's (is-c t), which is (= t c)) are accepted,
through the clause log only (the legacy core rejects them explicitly), and
so are arrays whose element sort is an enumeration, (Array I Color) over the
index sorts above: their constants, functions into and over them, store,
ite, select, equality, and extensionality, and over Int or Real indices
constant arrays of an enumeration and the default values of arrays built
from them by store and ite. Any other datatype, an array indexed by an
enumeration, an array of an enumeration nested in another array (as its
rows or indices), maps of arrays of an enumeration and the default value of
an array constant or application of one, and a distinct with more arguments than its
enumeration has constructors (with proofs Z3 refutes it by an exponential
pigeonhole search) over more than five constructors or with more than
sixteen arguments, past which Lean runs out of memory, are rejected.
Integer div, mod, and rem by zero or by a term (SMT-LIB leaves division by zero
uninterpreted, where Lean's Int division is total; a term divisor is
nonlinear), and Int
mixed with Real next to uninterpreted functions (also through a function
signature such as (Int) Real) are rejected explicitly.
The exception is an integer numeral where a Real is expected: without a
set-logic, or under ALL, Z3 reads (* 2 x) over a Real x as
(* (to_real 2) x), and such a to_real of a term built from numerals, sums,
differences, products, negations, and abs is read as the same term over Real
numerals, as QF_LRA reads it ((abs 3) in a Real position is the Real abs of
3.0). The same holds for such a to_real written
explicitly, in any logic: (to_real (+ 2 1)) is read as (+ 2.0 1.0).
One symbol name declared with
several signatures is rejected in every fragment: Z3 accepts such overloading
and tells the declarations apart by sort, but the certificate binds symbols
by name, so classification fails for the exporter and again for the
reconstructor, which parses the input itself. Quantifiers,
nonlinear terms, bit-vectors, and arrays are rejected. Definitions are expanded by Z3's parser.
Named assertions are retained as formulas, not converted into extra tracking
assumptions. Declarations unused by the assertions do not affect the fragment.

Bundle format, version 2
-----------------------

    format          "z3-native-proof-dag"
    format_version  2
    z3_version      producer's full Z3 version
    fragment        "propositional", "qf_lra", "qf_lia", "qf_lira", "qf_uf", "qf_uflra", "qf_uflia",
                    or "qf_uflira"
    result          "unsat" (the producer's result, not a checked claim)
    verification    "unverified"
    source_smt2     original input text
    query           zero-based index of the certified check-sat query (0 for a
                    script with at most one query); version 2 added this field
    declarations    native declaration kind, name, domain, range, parameters
    nodes           native applications: declaration index and argument indices
    assertions      node indices of the parsed assertions, in input order
    proof           node index of the native refutation
    rule_counts     counts of distinct proof nodes by native rule name

All indices are zero-based. Nodes are topologically ordered: each argument
refers to an earlier node. Nodes and declarations preserve native identity
and sharing; names are metadata, not identifiers. Proof applications retain
all their arguments, including their conclusions. Declaration kinds are the
Z3_OP_* API constants, not a new set of logical rules.

This version supports application nodes with Bool/Proof sorts and declarations
without parameters, except that a pseudo-Boolean declaration's parameters
are its bound followed, for pble, pbge, and pbeq, by one coefficient per
argument (decimal integers), and propositional certificates may contain
th-lemma declarations with the parameter "pb" alone. The qf_lra fragment additionally uses the Real sort,
numeral declarations whose name is the exact rational value, the arithmetic
operators and predicates listed above, and th-lemma declarations whose
parameters name a theory hint ("farkas", "bound", "implied-eq", "euf",
"tseitin", "smt", or the exporter's own "cnf") followed, for the first three,
by one nonnegative rational coefficient per literal of the lemma clause.
The qf_lia fragment uses the Int sort the same way, with integer numerals,
no Real division, and the declarations div, mod, rem (over (Int Int)) and
abs (over (Int)) in its place; its th-lemma hints
additionally include "cut" (the integer solver's Gomory cuts and gcd
conflicts) and "arith" (the solver's own div, mod, and rem axioms), which carry
no coefficients, and a farkas or bound whose
coefficients did not re-derive the lemma over the tightened and rounded
integer bounds is recorded without coefficients too (see below); a
certificate never mixes Int with Real declarations.
The qf_uf fragment uses the input's uninterpreted sorts under their own names
(never Bool, Real, or Proof) for constants, function declarations whose
range is one of those sorts and whose domain consists of those sorts and
Bool, predicate declarations over the same domains, and equality and
distinct declarations over one of the sorts; the certificate stays
many-sorted even though Lean sees one type (see below). The qf_uflra
fragment combines both and additionally allows Real in the domain of
functions and predicates and function declarations with range Real and a
nonempty domain; qf_uflia does the same with Int, and qf_uflira with
both. A certificate declaring an uninterpreted sort or function must be
labelled qf_uf, qf_uflra, qf_uflia, or qf_uflira according to whether it
contains arithmetic and over which sorts, and the reconstructor rejects any
other combination; only a qf_lira or qf_uflira certificate declares both
Int and Real symbols, and it must; to_real, from
Int to Real, to_int, from Real to Int, and is_int, over Real, are its
conversion declarations.
Other native shapes are rejected, never serialized incompletely. The root is
required to conclude false, but checking that shape does not establish proof
correctness.

The exporter itself does not verify inference rules. A separate, deliberately
limited Lean reconstruction path is now available below. Theory support and
general proof-required solver integration remain later milestones.

Run the focused regression suite with the local bindings:

    PYTHONPATH=build/python python3 -m unittest discover -s examples/python \
        -p test_proof_certificate.py

Linear real arithmetic through the clause log
--------------------------------------------

The sat.smt core's clause log carries Farkas coefficients for every
arithmetic inference: each inferred clause comes with a hint such as
(farkas 1 $11 2 $17 1 $21). proof_certificate.py drives the z3 executable for
arithmetic input by default and rebuilds the log into the same DAG format
(the smt core's proof object is the alternative; see the next section):

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py \
        --z3 build/z3 input.smt2 > proof.json

--core auto (the default) uses the legacy proof object for propositional input
and the clause log otherwise; --core clause-log forces the log for Boolean
input too, and --core legacy the proof object for QF_UF, QF_LRA, QF_UFLRA,
QF_LIA, and QF_UFLIA input. --query N selects the check-sat query of an
incremental script (see "Input scope"); both cores solve that query's
snapshot on its own, non-incrementally.
--z3 defaults to $Z3_EXE, then build/z3 next to this
checkout, then z3 on PATH. --timeout (seconds, default 600) and --memory
(megabytes, default 8192) bound each z3 run of the clause-log export, the
solver's and the native trimmer's; z3 stops itself at either limit (-T and
-memory), a run that outlives its time limit by 30 s is killed, and the export
fails with an error naming the limit hit. --timeout also bounds the Python
replay of the log, checked before every log command and every bounded solver
call of the assumption search. Limits above 1000000 s or
4194304 MB are rejected (z3 cannot hold them). The legacy core solves in
process under the same options: the time limit is its solver's timeout and
the memory limit z3's memory_high_watermark_mb, which the smt core polls
during the search (a global parameter, set for the check and restored after
it); either hit is an error naming it. The executable runs
with sat.smt=true and with solve_eqs, propagate_values, elim_unconstrained, and
bound_simplifier disabled, because the log starts after preprocessing and
bound_simplifier runs solve_eqs internally regardless of its own option. It
also runs with combined_solver.ignore_solver1=true: for a non-incremental
check-sat the frontend otherwise applies the tactic of the input's logic
before the core (simplify, propagate-values, ctx-simplify, solve-eqs, and
elim-uncnstr for logics without a dedicated tactic), whose passes ignore the
smt.* options, replace subterms whose variable occurs nowhere else by fresh
k!N constants, and Ackermannize predicates over Bool alone, so the log
would refer to symbols the certificate cannot tie to the input. The legacy
exporter sets the same option on its solver, whose proof would otherwise
name such subterms by intro-def steps.

proof_clause_log.py replays the log with exact bookkeeping and never trusts a
step:

  - Each assumed clause is tied to an original assertion: the identical
    formula is asserted directly; an equivalent formula or conjunct is bridged
    by and-elim, rewrite, and mp; a formula that merely implies the clause,
    which happens when preprocessing splits an xor or an equivalence into
    several clauses, is bridged by a th-lemma with hint "cnf" and one
    unit-resolution. When no single assertion implies the clause (Z3 found a
    contradiction while asserting, or simplified an ite inside one assertion
    under a unit asserted by another, which shows in alldiff clauses), the
    cnf lemma is over an unsat core of the assertions. Clauses with true, not
    false, or complementary literals are def-axiom nodes. Nothing else is
    accepted as an assumption. In Lean a cnf lemma is first proved by gate
    propagation over the Boolean structure of the clause with the theory
    atoms opaque (two atoms denoting one constraint, or complementary ones,
    are bridged by an equivalence the theory tactic proves; a distinct over
    terms is the conjunction of its pairs' negated equalities when Z3 logged
    some pair as an equality node, a pair without a node being a synthetic
    leaf rendered as the distinct's conjunct). The proof keeps only the
    steps it uses, and a case split whose branch does not need its
    hypothesis is dropped. When the search gives up, it is repeated over the
    gates of z3's unsat core of the propositional abstraction (an untrusted
    hint; Lean checks the proof). A clause that needs a theory fact, or that
    neither search refutes within its budget, falls back to the unfolded
    grind proof.
  - farkas, bound, implied-eq, and euf hints list literals that are jointly
    contradictory; the exporter emits one th-lemma concluding the clause of
    their complements, after checking farkas and bound coefficients with exact
    rational arithmetic. Equality literals in these hints carry placeholder
    coefficients, so their multipliers are solved for by Gaussian elimination,
    as Z3's own checker does. implied-eq ends in a disequality, not an
    inequality to sum: its shape is checked in Python and Lean proves that
    the preceding literals imply the complementary equality. euf hints may
    also carry congruence claims (cc (= a b)) or (comm (= a b)) that guide
    Z3's checker; they are not literals of the lemma and are dropped after a
    shape check, since Lean's grind performs its own congruence closure.
    tseitin hints list a gate clause and become def-axiom nodes. A bare smt
    hint claims the logged clause outright and becomes a th-lemma with hint
    "smt".
  - A Real ite term is an opaque variable in every Farkas combination, as in
    Z3's arithmetic solver. Its two gate clauses, (not c) or (ite c a b) = a
    and c or (ite c a b) = b, are added as def-axiom nodes and also arrive as
    tseitin inferences; Lean proves them directly from a decidability witness
    for c with ite_eq_left and ite_eq_right.
  - alldiff hints list the gate clauses of a distinct below the root (the
    distinct against the disjunction of its pairwise equalities); a distinct
    asserted at the root is clausified into assumed clauses. A gate clause of
    the right shape (two literals of one polarity, every disjunct equating
    two arguments of the distinct, every pair covered for the positive
    clause) becomes a def-axiom node that Lean proves from the pairs, like a
    tseitin clause. Any other alldiff clause must be derived from the
    original assertions, like an assumed clause; the hint itself never
    authorizes a theorem.
  - rup inferences and every logged clause that differs from its hint's lemma
    are derived by unit propagation over the live clause database, including
    the Tseitin definitions of compound Boolean atoms that Z3's checker also
    uses implicitly. The derivation is emitted as hypothesis, unit-resolution,
    and lemma nodes, so the reconstructor needs no new Boolean rules.
  - del steps remove clauses from the database. If the log never derives the
    empty clause, because the contradiction was found while asserting, the
    empty clause is derived from the assumptions or tied to the assertions.
  - The sat core logs Boolean variables that have no expression, such as
    goal2sat's internal true literal when a unit is asserted, as nullary Bool
    constants k!<n> absent from the input. Assumed and deleted clauses over
    such a phantom are dropped silently: they are tied to no assertion, and
    dropping a clause can only remove support for a later rup step, which
    then fails explicitly. An inference or definition that mentions a phantom
    is rejected as a fresh symbol, as is any other symbol absent from the
    input.

Logs of at least 4,096 characters are reduced with Z3's native proof trimmer
before replay.
The exporter follows the final empty clause's dependency graph, checks it for
missing references and cycles, and replays every retained inference using the
listed premises and independently proved Boolean gate clauses. These
dependencies are untrusted hints, not proof rules. Incorrect trimming must
fail replay or Lean checking. Trimming only shortens the replay: when the
trimmer reports an error (an inference it cannot derive by unit propagation)
or writes a dependency graph with missing or cyclic references, the exporter
emits a `RuntimeWarning` naming the failure and replays every step of the
untrimmed log instead, so the export still succeeds but takes longer. The
compact exported DAG keeps every original assertion, even if its proof is
outside the selected refutation.

EUF hints can also contain cc/comm congruence annotations. These are not
additional assumptions: the exported lemma contains only the actual Boolean
literals, and Lean independently proves their inconsistency.

The exporter's own checks only fail early with a clear message; Lean remains
the arbiter.

Uninterpreted functions (QF_UF) go through the same clause log. The log
declares the sort and the functions it uses, which must be the input's own;
function applications are rebuilt with the input's declarations, so a wrong
arity or an ill-sorted argument is rejected. Equality conflicts arrive as
euf hints, distinct as alldiff clauses, and the Boolean structure as tseitin
and rup steps, exactly as for arithmetic; no new hint kind is involved. An
ite term over the sort is an opaque element for the euf core, tied to its
branches by the same two gate clauses as a Real ite, which the replay adds
as def-axiom nodes.

Uninterpreted functions mixed with arithmetic (QF_UFLRA) need nothing new
in the log either: an application with a Real result, (f x) or (g a), is an
opaque variable of the farkas, bound, and implied-eq hints, exactly like a
Real ite (the replay's linear forms key such terms by identity), euf hints
carry the congruences (= (f x) (f y)) from (= x y), and implied-eq hints
supply the equalities between Real terms that the congruences rest on. Z3's
rewriter normalizes the arguments before logging ((f (+ x 0.0)) is logged as
(f x)), which the usual assumption bridging covers with a rewrite. The same
holds over Int (QF_UFLIA): an application with an Int result is an opaque
integer atom, so a strict bound on it is tightened, a cut may run through
it (2 (f x) = 2 y + 1 is a gcd conflict), and the integer conventions of
the next paragraph apply unchanged. A log
that still refers to a fresh symbol is rejected ("declares a symbol absent
from the input" when the log declares it, "uses an undeclared or fresh
symbol" when it first appears inside a clause).

Linear integer arithmetic (QF_LIA) goes through the same clause log with
three integer-specific conventions, all taken from Z3's own clause-log
checker. The log prints numerals without a sort, so an integer input values
them in Int (the exporter never mixes Int with Real). A strict bound over Int
is tightened to its non-strict form, (< t 5) and (not (<= 5 t)) both to
(<= t 4), in the Farkas combinations and in the canonical keys that tie
assumed clauses to assertions, since Z3's rewriter rounds the input's own
bounds the same way ((<= 1 (* 3 x)) is logged as (>= x 1); the rewrite is
proved by Lean). A bound hint's combination may be rounded to the integer
lattice before the propagated literal cancels it, with the literal's
multiplier recomputed as Z3's checker does. Two hint shapes certify nothing
beyond the clause: cut, the integer solver's Gomory cuts and gcd conflicts,
and a farkas or bound whose coefficients do not refute the tightened literals
even after rounding, which happens when the LP explanation rests on cuts Z3
made along the way (Z3's checker fails on those too; 2 of 1,382 lemmas in a
random sample). Over Real such a hint is rejected; over Int the lemma is kept
without coefficients, which marks it in the certificate as proved by Lean
alone, and the reconstructor accepts coefficient-free farkas and bound
th-lemmas in Int certificates only. Coefficients that are present must
re-derive the lemma on both paths. Integer div and mod by a numeral k are
opaque atoms of the linear forms, like ite terms: the arithmetic solver adds
their defining clauses itself, k (div t k) + (mod t k) = t, (mod t k) >= 0,
and (mod t k) <= |k| - 1, under the hint arith, whose arguments are the
negated clause literals (an input mentioning div alone still gets the mod
atom and all three clauses). Z3's rem is (ite (>= k 0) (mod t k) (- (mod t
k))); its rewriter turns (rem t k) by a numeral into (mod t k), or its
negation for a negative k, unless t is a sum or a product, and the solver
relates the rem atoms it keeps to mod by two more arith clauses,
(or (not (>= k 0)) (= (rem t k) (mod t k))) and
(or (>= k 0) (= (rem t k) (- (mod t k)))). An arith hint is shape-checked like a cut
(every literal an arithmetic atom over linear terms, under any negations)
and proved by Lean alone. Real division axioms use arith too, for example
2 * (1 / 2) = 1, sometimes with a true literal standing for an elided
false clause literal. The replay drops true from the hint's contradictory
set before checking its arithmetic shape, removing its coefficient too
when present. An otherwise empty hint is still rejected. abs, over Int or
Real, rarely reaches the log: Z3's rewriter replaces
(abs t) by (ite (>= t 0) t (- t)), and the exporter's rewrite bridge ties
the assertion to the logged ite, as for any other rewrite. When the
arithmetic solver does see an abs term, its two case axioms are arith hints,
and the replay rebuilds the logged (abs t) as that abs application.

Uninterpreted functions through the legacy proof object
-------------------------------------------------------

The smt core's conflict resolution records complete equality proofs, so a
QF_UF refutation from the legacy proof object (--core legacy, or
export_certificate) needs no theory hint at all: every equality between
terms is derived by trans, trans*, symm, and monotonicity steps, with the
preprocessing rewrites the clause log never sees. The certificate format is
unchanged (the same declarations and nodes as a clause-log certificate, with
rule counts over the native rules instead of th-lemma). The reconstructor
accepts the same rules over terms of a sort as over Boolean formulas; see
"Uninterpreted functions in Lean" for the Lean terms. Shapes the legacy core
emits for this fragment beyond the Boolean slice: rewrites between terms
(for example (= (ite true a b) a)), the commutativity rule, congruence
through ite terms and distinct, and def-axiom gate clauses pairing a distinct
with its expansion into disequalities.

Uninterpreted predicates over Bool alone, (declare-fun r (Bool) Bool) with no
uninterpreted sort in the assertions, are certified on both paths: the smt
core's proof object proves (= (r p) (r q)) by monotonicity from (= p q) like
any other congruence, with iff-true, iff-false, and hypothesis steps when it
splits on an argument, and the clause log carries the same congruences as
euf hints once the frontend's tactic preamble is bypassed (it Ackermannized
such predicates with fresh symbols r!1, k!2, or decided the input before a
clause was logged). The certificate is a qf_uf certificate without sort
names; Lean uses the same encoding, with the carrier _m.U holding nothing but
the injected Boolean arguments (see "Uninterpreted functions in Lean").

Linear real arithmetic through the legacy proof object
------------------------------------------------------

In the flat arithmetic proof format, theory_lra records each LP conflict and
bound propagation as th-lemma parameters: (_ th-lemma arith farkas c1 ... cn) for a conflict,
(_ th-lemma arith bound c1 ... cn 1) for a propagated bound literal, and
(_ th-lemma arith implied-eq) for a propagated equality (the coefficients are
the Farkas multipliers of the LP explanation, one per premise in the order
the step lists them; before 2026-10-14 the parameter vector was reset and
never filled, which is why arithmetic needed the clause log). Unlike a
clause-log th-lemma, a legacy th-lemma has premises: the literals and
equalities the step rests on, each with its own proof, and it concludes
false, the propagated literal, or the implied equality. The certificate keeps
the hint and the normalized coefficients as the declaration's parameters
(premises first, then the literals of the concluding clause) and drops the
leading "arith" symbol. Two more legacy shapes are accepted: triangle-eq,
arith_eq_adapter's axioms tying (= s t) to (<= (- s t) 0) and (>= (- s t) 0),
and the parameters of the older theory_arith (smt.arith.solver=2, which the
frontend's tactic preamble used to select for difference-logic-shaped
input): assign-bounds (a propagation weighting the antecedents only, with
signed coefficients) becomes bound with the propagated literal's weight 1
added, eq-propagate becomes implied-eq, and only magnitudes are kept. A
th-lemma whose hint is none of these (nla, gomory-cut, gcd-test) is rejected
at export, and so is a bare (_ th-lemma arith) over Real, which records no
evidence.

Integer input (qf_lia, qf_uflia, qf_lira, qf_uflira, opt-in as for the
clause log) is certified
on this path too, since 2026-10-16. theory_lra emits the same farkas, bound,
implied-eq, and triangle-eq steps over Int, and three shapes of its own: a
bare (_ th-lemma arith) with premises is a cut (the bound literal a Gomory
or Hermite cut derives from the bounds it lists), a bare one without
premises is a div or mod axiom stated as (or false l) and resolved with the
unit true (a true-axiom step, rendered True.intro), and a farkas whose
coefficients do not refute its premises rationally is a lattice conflict
(no integer point on the rationally feasible region) or an explanation
through bounds the LP tightened to the integer lattice. The exporter keeps
the first two as the arith hint and strips the coefficients of the third
(_integer_coefficients_certify, the decision check_linear_hint makes for
the clause log); the reconstructor shape-checks all three (held premises
and clause literals are linear integer atoms) and Lean proves them with
first | omega | grind, as it proves the clause log's cut and arith lemmas.
A fourth shape is theory_lra's own verdict on a conflict it could not
certify: when its Farkas check fails or the LP explanation does not
linearize, which is what a lattice conflict looks like from inside the
solver, it labels the step (_ th-lemma arith unsupported) instead of
farkas with coefficients. Over Int the exporter keeps such a step (it must
list at least one premise and conclude false) as the same coefficient-free
farkas, so nothing changes on the reconstructor's side; over Real it stays
rejected ("th-lemma without a replayable theory hint: arith unsupported"),
as does the nonlinear variant (arith unsupported nla).
Z3's rewriter also cancels the common factor of (div (* 2 x) (- 2)) through
(ite (= 0 (- 2)) (div (* 2 x) 0) (div (* x 1) (- 1))), whose dead branch
divides by zero: such a term may appear in a proof step but never in the
assertions (see "Arithmetic in Lean").

The current LP proof format also carries a shared lp-context, which concludes
true and stores the indexed arithmetic certificate in declaration parameters.
The exporter removes this nonlogical context dependency, not the logical
premises of the inference. It translates lp-linear's local coefficients
(after the step index) to farkas, bound, or implied-eq as appropriate.
lp-input bridges from the supplied input proof to the normalized arithmetic
fact, and lp-discharge bridges from a native lemma that discharges its
temporary hypothesis; both become smt implications proved independently by
Lean, as do premise-free equality identities. Context metadata is not trusted
or interpreted as an assumption.
In Int certificates, lp-integer-tighten, lp-integer-lattice, and lp-gomory
become coefficient-free arith implications or farkas refutations, checked
by Lean alone. Nonlinear and unknown lp- rules remain unsupported.

The reconstructor re-derives every farkas and bound combination from the
premises and the clause with exact rationals before Lean runs, checks the
shapes of implied-eq and triangle-eq steps, and states each th-lemma as the
implication from its premises, proved by grind and applied to the premise
steps. Congruence through an arithmetic operator or comparison (monotonicity
over +, *, -, /, div, mod, abs, <=, <, >=, >), which the smt core's rewriting of atoms
produces, is a grind lemma taking the argument equalities as premises; the
other monotonicity shapes keep their explicit terms. Inputs with Real ite
terms are certified on this path as well: the smt core reached directly
keeps the ite terms and records their gate clauses as def-axioms (the
frontend's tactic preamble, bypassed since 2026-10-15, named each ite term
by an intro-def step, a fresh definition the certificate cannot tie to the
input). --core auto keeps the clause log for arithmetic.

Reconstruct and check a Boolean proof in Lean
-------------------------------------------

proof_to_lean.py consumes the original SMT-LIB file and its native JSON bundle.
It supports asserted, unit-resolution, mp, Boolean rewrite, refl, symm, trans,
trans*, iff-true, iff-false, Boolean monotonicity, commutativity, and-elim,
not-or-elim, hypothesis, and lemma proof nodes.
It also reconstructs supported Boolean def-axiom clauses.
mp checks its ordered premises and conclusion, accepting implications and
Boolean equivalences. Each rewrite must conclude an equality or equivalence and
is checked independently of the input hypotheses: a Boolean rewrite by a direct
proof term (truth values propagated through the gates of both sides, then case
splits on atoms; an exhaustive truth table only as the fallback), a theory
rewrite by grind, and a rewrite between two identical sides by Iff.refl or
Eq.refl in place (see "Uninterpreted functions in Lean").

refl, symm, and trans check Boolean equivalence endpoints and compose Lean's
logical rules. monotonicity checks identical application heads and arities,
and requires an oriented equivalence for every changed argument. Unchanged
arguments need no premise; repeated arguments can share evidence. Congruence
covers all supported Boolean connectives using direct proof terms, not truth
tables or propositional extensionality. commutativity proves (= (f a b) (f b
a)) for equality, equivalence, and, or, and xor. and-elim selects an immediate conjunct.
not-or-elim selects the complement of an immediate disjunct, including native
double-negation cancellation.

iff-true derives (p <-> True) from a proof of p; iff-false derives (p <-> False)
from a proof of (not p). Both validate the premise and ordered endpoints and
use direct Lean logical terms, retaining any open hypothesis dependencies.

trans* finds an equivalence path using only its supplied premises, which may be
reordered, reversed, repeated, cyclic, or redundant. It emits a balanced
composition of Iff.symm and Iff.trans terms without truth tables or solver calls.
Reflexive conclusions permit an empty path. Every premise must be a Boolean
equivalence, even if unused by the chosen path, and disconnected endpoints are
rejected. All supplied premises retain their hypothesis dependencies; choosing
a path does not silently discharge unused assumptions.

hypothesis introduces a temporary assumption, not an original assertion. Open
proof steps are functions of their hypotheses, so a shared subproof can be used
under different lemma scopes without leaking assumptions. lemma requires a proof
of false and a conclusion containing a complement of every open hypothesis.
It supports both complement orientations, compound literals, reordered or
repeated literals, and weakened clauses. All hypotheses of its premise are
discharged; the final proof must have no open hypotheses. Nested lemmas and
shared subproofs use direct Lean proof terms, not truth tables.

def-axiom is not permission to introduce a Lean axiom. Each supported clause is
proved in a separate Lean theorem with no input assertions or proof premises.
Supported shapes are the Boolean gate clauses for not, n-ary and/or, implication,
Boolean equivalence, xor, and Boolean ite, plus complementary literals and
constant tautologies. Negated and compound operands, literal reordering,
duplicates, and weakened clauses are supported. The proof negates the clause
and derives a contradiction from one gate and its immediate operands, without
enumerating assignments to nested atoms. Unsupported or malformed clauses fail
explicitly, even when unused in the final refutation. This is not a general
propositional tautology prover, and fresh-symbol definitions remain unsupported.

th-lemma nodes and arithmetic rewrites are proved by Lean's grind tactic
after unfolding the formula and term definitions they mention; a th-lemma
with premises (the legacy core's) is stated as the implication from its
premises and applied to their steps; see the arithmetic sections. Other
proof rules, including rewrite*, mp~, and definition introduction, fail
explicitly. Consequently, some otherwise propositional Z3 refutations are
still unsupported.

Install the pinned Lean toolchain as described in lean/README.md. The Boolean
inputs live in Z3Prover/z3test under regressions/proofs/lean/; the commands
below assume a z3test checkout next to this repository. From the repository
root, run this end-to-end example:

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py \
        ../z3test/regressions/proofs/lean/unit_resolution.smt2 > /tmp/unit_resolution.json
    PYTHONPATH=build/python python3 examples/python/proof_to_lean.py \
        ../z3test/regressions/proofs/lean/unit_resolution.smt2 /tmp/unit_resolution.json \
        -o /tmp/unit_resolution.lean

To exercise implication rewriting and mp as well:

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py \
        ../z3test/regressions/proofs/lean/boolean_rewrite.smt2 > /tmp/boolean_rewrite.json
    PYTHONPATH=build/python python3 examples/python/proof_to_lean.py \
        ../z3test/regressions/proofs/lean/boolean_rewrite.smt2 /tmp/boolean_rewrite.json \
        -o /tmp/boolean_rewrite.lean

To also exercise trans, monotonicity, and not-or-elim, replace boolean_rewrite
with boolean_structural in both commands. Use boolean_branching to exercise
hypothesis discharge and learned clauses. Use boolean_def_axiom for clauses
forcing both arguments of an xor to be true, whose native proof still requires
a Boolean gate clause after preprocessing.

The second command invokes scripts/check_lean.sh and publishes the .lean file
only if the pinned Lean checker succeeds. It exits nonzero for malformed or
unsupported certificates, input mismatches, or Lean failures. Existing output
is left unchanged on failure. Output must not alias the original input or JSON
file. Bash and the pinned Lean toolchain must be available.

You can check the resulting Lean file again without Z3:

    ./scripts/check_lean.sh /tmp/unit_resolution.lean

The generated file imports only Init. It contains shared formula definitions
and proof steps built from input hypotheses and Lean core logical rules.
Rewrite lemmas split only the atoms occurring in that rewrite and use
of_decide_eq_true rfl to check every case by kernel reduction, not native_decide
or a solver call. The case count is exponential in a rewrite's atom count;
large rewrites can exceed Lean's normal resource limits and fail without
publishing a proof.

Arithmetic in Lean
------------------

For qf_lra certificates every formula definition takes a second argument
_vars : Nat -> Rat, Real variables become term definitions over it, numerals
become exact Rat literals, and the theorem reads

    theorem unsat (_atoms : Nat -> Prop) (_vars : Nat -> Rat)
        (_h0 : formula_k _atoms _vars) ... : False

Real variables are encoded as Rat. This is sound for the supported fragment:
a system of linear constraints with rational coefficients has a real solution
if and only if it has a rational one, so unsatisfiability over Rat is
unsatisfiability over the reals. The exporter rejects nonlinear terms, which
is the precondition of that argument; extending the fragment must revisit
this encoding. A Real ite becomes Lean's ite over Rat with the classical
decidability instance for its condition, so the term definitions that contain
one are noncomputable; the argument above still applies, because under each
fixed valuation of the conditions the constraints are linear. A Real abs is
the same kind of ite, (if t >= 0 then t else -t) over Rat. Every term
definition takes the atom valuation as well as the Rat valuation.

Each th-lemma and each rewrite whose equivalence mentions arithmetic is proved
in a private theorem by unfolding its definitions and calling grind, whose
linear-arithmetic and propositional procedures produce a kernel-checked proof.
Large rewrites first prove a normalized form for each arithmetic atom, then
prove the Boolean equivalence separately over abstract propositions. And/or
rearrangements use projections and case analysis instead of enumerating all
truth assignments or repeatedly invoking arithmetic during Boolean search.
Before Lean runs, the reconstructor re-derives the recorded farkas and bound
combination with exact rationals and rejects coefficients that do not refute
the lemma's literals. grind does not always combine equalities whose constants
are fractions, so the generated proof first states each fractional atom's
denominator-free form as an implication that grind proves, then calls grind
on the lemma; a false helper fails rather than weakening anything. For the
same reason each Real ite reachable from the lemma gets its two branch
equalities, under the condition and under its negation, stated the same way
(scaled to integer coefficients when a branch has fractions) and proved with
ite_eq_left and ite_eq_right; Z3's rewriter can push a comparison through an
ite, in which case these are the only facts tying the ite to its branches.
Without arrays both kinds of facts are stated over the term and formula
definitions, proved with only the definitions down to the atoms of their
linear forms unfolded, and unfolded together with the goal, so nested ites
are never written out in them.

A qf_lira certificate takes both valuations, (_vars : Nat -> Rat)
(_ivars : Nat -> Int): a Real variable is _vars i and an Int one _ivars i
(one numbering for both), numerals, ite, and abs take the type of their
node, and every atom compares two terms of one sort, a Real one as for
qf_lra and an Int one as for qf_lia below. to_real is Lean's Int.cast into
Rat, through which a Real atom's linear form can range over Int terms;
such an atom keys like the equivalent tightened Int atom when atoms are
matched up in normalized rewrites and ite tables. Without to_real, Z3
relates no atoms of the two sorts in one arithmetic lemma, so the
reconstructor reads each th-lemma's sort off its atoms: an Int lemma takes
the integer path (tightening, the generalized attempt, the combination and
split proofs), a Real one the Real path, and a lemma over both sorts is
rejected. An arithmetic ite is one atom of the linear forms, tied to its
branches by gate clauses, so the atoms of its condition are not the
lemma's: an Int ite over a Real comparison (as the rewriter makes of a
read of a store into an (Array Real Int)) keeps a lemma over Int atoms
Int, and a to_real inside such a condition does not make the lemma a cast
lemma. A lemma reaching to_real is checked as a rational combination with
each Int atom tightened on its own (its coefficients, when it has any, must
refute the literals; a cut must round Int atoms and Real atoms over Int
terms only) and proved by grind after two kinds of facts: every Int atom
s R t is stated equivalent, in both polarities, to the tightened bound
between the casts of s and t (three private lemmas, _int_cast_le,
_int_cast_lt, _int_cast_eq, from core's Rat.intCast_le_intCast and its
siblings), and every Real atom over Int terms alone is stated equivalent to
the Int atom of its integer-scaled form; push_cast then distributes the
casts. to_int is Rat.floor, an Int atom of the linear forms like div,
and (is_int t) is ((Rat.floor t : Int) : Rat) = t, SMT-LIB's definition; a
lemma reaching either gets the floor bounds of each floored term a from
core's Rat.floor_le and Rat.lt_floor_add_one (Z3's two arith axioms for
to_int), floor a = D (core's Rat.floor_intCast) when a is itself an
integer D over Int terms, and floor a = floor b + D (core's
Rat.floor_add_intCast) for two floored terms differing by an integer D,
which Z3's rewriter uses to move integer summands out of a floor (these
pairs only up to 12 floors per lemma). A cut or coefficient-free farkas or
bound that rounds a Real atom over a Real variable through a floor (x and
x/2 both integers) also gets its projection onto the Int atoms: the Real
atoms are eliminated exactly (substitution, then Fourier-Motzkin, up to 200
constraints), and each projected constraint F R 0 (x = 5 leaves
2 floor(x/2) - 5 = 0) is stated over Int through its cast lemma, so grind's
Int module refutes it. A cut whose literals reach no Int atom is rejected.
Without arrays the cast facts, the Real-to-Int atom equivalences, and the
floor bounds are stated over the term and formula definitions, folded, and
unfolded together with the goal, like the ite gates; so, in every fragment
without arrays, are the excluded middles of Boolean arguments of
uninterpreted functions.
Rewrites, which may span both sorts, are proved by first | omega |
grind (splits := 64). The Rat encoding of the Real variables stays sound
next to Int ones: fix the Int values and the truth value of every atom and
ite condition, and the Real constraints left (to_real terms now integer
constants) are a linear system with rational coefficients, which has a
rational solution if it has a real one. Int and Real ites with the same value
table are kept apart in normalized rewrites, so an ite term of one sort never
stands for one of the other.

For qf_lia certificates the second argument is _vars : Nat -> Int, numerals
are Int literals, an Int ite is Lean's ite over Int with the classical
instance, and no encoding argument is needed: the variables range over
exactly the integers. Integer div and mod by a numeral are Lean's Int / and
%, which follow the same Euclidean convention as SMT-LIB (the remainder is
nonnegative and below the divisor's absolute value, for negative divisors
too), and abs is the ite SMT-LIB defines it as, (if t >= 0 then t else -t)
with the classical instance. Z3's rem by a numeral k is its definition at k:
t % k for a positive k, -(t % k) for a negative one. The agreement holds for
nonzero divisors only (Lean's x / 0 is 0 where SMT-LIB's is any value), so
the reconstructor rejects every div, mod, or rem node whose divisor is not a
nonzero constant among the nodes the theorem states, the assertions and
their subterms (a proof step may mention a div or mod by zero, in the dead
branch of the rewriter's factor cancellation, which Lean checks under its
total division without that reaching the statement; a rem is rendered from
the sign of its divisor, so a rem by zero or by a term is rejected wherever
it occurs); omega reads / and % by a positive numeral directly,
and leaves them as atoms for a negative divisor, whose arith axioms grind
proves instead. Each th-lemma and arithmetic rewrite is proved by
first | omega | grind (splits := 64): omega decides linear integer
arithmetic (ite over Int included) and produces a kernel-checked proof,
where grind's integer module ran out of steps on Farkas lemmas with several
equalities and on ite splits; grind still handles goals omega does not read.
An Int th-lemma with hint farkas, bound, or cut whose literals contain div,
mod, abs, ite, or application atoms gets a first attempt over the atoms
generalized to integers: the definitions outside the atoms are unfolded,
for a cut or a coefficient-free lemma each mod atom's bounds 0 <= m < |k|
are stated (Int.emod_nonneg, Int.emod_lt_of_pos, through Int.emod_neg for
a negative divisor; Z3 fixes them at base level and omits them from the
lemmas it explains) and reverted into the goal, each atom is generalized to
a fresh integer, and omega (a farkas or bound with coefficients, a
combination over the atoms already re-derived by the reconstructor, so it
gets no mod bounds: they are redundant there and made omega's case analysis
take tens of seconds on a 33-literal lemma) or grind (splits := 64) (a cut
or a coefficient-free lemma) closes the linear goal with no Euclidean
unfolding and no ite splits. If that attempt fails,
the unfolded proof above runs unchanged as the fallback under first. A
lemma over a dozen such atoms by negative numerals used to exhaust its
heartbeats in the unfolded proof.
Ahead of both, a farkas or bound with at least 16 bounds (premises and
literals) and a coefficient of magnitude 10000 or more is proved by the
combination itself: each premise and negated literal becomes
0 <= upper - lower (Int.sub_nonneg_of_le, strict bounds tightened by
Int.lt_iff_add_one_le, equalities turned by the sign of their multiplier),
the facts are scaled by the integer multipliers and summed (Int.mul_nonneg,
Int.add_nonneg) as a balanced tree, and with no hypothesis in scope
simp +arith only [] (omega as the fallback) checks that the sum is a
negative constant; omega alone was quadratic in the summands and ran out of
heartbeats on 140 bounds or more. With all bounds in scope omega searched for
the combination itself and did not finish on 21-literal lemmas with
eight-digit coefficients (QF_LIA cut_lemmas). A wide lemma whose
coefficients are small but some bound spans 8 atoms or more (dense rows,
where omega took minutes) gets the combination too. Smaller lemmas, and
wide sparse ones with small coefficients, stay with omega, which is quick
on them and whose proofs cost Lean less memory; a
bound whose refutation needs rounding gets no such attempt.
A cut, and a farkas or bound without coefficients, is proved ahead of the
same alternatives by one split (since 2026-10-30): z3, as an untrusted
oracle, searches for an integer form s and an integer k such that each
side of k < s or s <= k, as a fact 0 <= s - (k + 1) or 0 <= k - s, makes
the bounds refutable by a combination (a mixed integer problem, the
coefficients of s within [-1, 1] first, each search within a fixed z3
rlimit); Python checks both combinations, and Lean checks the case split
(Int.lt_or_le) and each side as above. Every Gomory cut is such a split
cut; a lemma without one within the budget (a cut resting on the
base-level bounds of a mod atom, or on the rounding of a bound inside a
side, as the cut of lia_gomory) keeps only those alternatives.
A cut, an arith axiom, or a farkas or bound without coefficients (see the
clause-log section), reaches Lean with its literal shapes checked only; a
false one fails there and no proof is published. Coefficients that are present are
re-derived over the tightened integer constraints, with the bound rounding
of Z3's checker, and rejected when they do not refute the lemma. In a
rewrite over more than 16 linear atoms (the normalized path above) a
tightened strict atom is keyed as the negation of the bound it contradicts,
so (< x 5) and (>= x 5) share one atom name, as they share one key in the
exporter's replay. Known limit: an Int ite nested inside the condition of
another ite can push omega and grind past the heartbeat budget on the
th-lemma that reaches it; the certificate is then rejected (no proof is
published), never misproved. An ite whose two branches are one term,
(ite c a a), which Z3 keeps when it occurs inside an application or a
product, gets its two gate clauses and the bare equality (ite c a a) = a
that Z3 logs as a tseitin step; all three are proved by a case split on c
with ite_eq_left and ite_eq_right. The lemma does not depend on the
fragment, but Z3 has only been observed to log these clauses for Int input:
over Real and the uninterpreted sorts it simplified (ite c a a) away in
every input tried.

Gate clauses also accept negated conditions whose guards Z3 simplified by
collapsing double negations. Their proofs split on the innermost condition
and introduce the required negations, without adding axioms.

Lean core's Rat library itself depends on propext, Classical.choice, and
Quot.sound, so arithmetic theorems necessarily report those three standard
axioms (Int theorems do as well, through omega and the classical ite
instance). The propositional slice remains axiom-free. Long refutations elaborate
under set_option maxRecDepth 100000; this is an elaborator limit, not a trust
setting. A file of more than 8 MB of Lean text also sets Elab.async false, so
Lean elaborates its declarations one at a time instead of in parallel tasks:
that is a schedule, not a trust setting, and keeps a third less memory alive
(z3test's QF_UF NEQ004_size4, 21 MB, peaks at about 7 GB under the 8 GB
--memory cap of scripts/check_lean.sh, at the cost of three times the time).

Refutations with more than 500 proof steps, in every fragment, are split into
separately checked lemmas: one at each shared subproof, and one whenever a
chain would otherwise nest more than 500 steps, because a single nested term
elaborates superlinearly and exhausts Lean's default heartbeat budget between
1,000 and 2,000 steps. A step with more than 64 premises or clause literals
counts as that many steps, so a lemma step discharging hundreds of
hypotheses is not elaborated among hundreds of unrelated steps, which made
it about ten times slower. Each lemma receives the original assertions as one
conjunction and abstracts its open hypotheses explicitly; steps the root never
uses are not outlined. The final unsat theorem still takes exactly the original
assertions. Arithmetic and uninterpreted-sort lemmas may use classical
decidability, within the already documented standard axiom boundary.
Propositional lemmas instead take the decidability witnesses they need as
parameters, which the final theorem introduces constructively as described
below, so the propositional slice stays axiom-free at every size.

Uninterpreted functions in Lean
-------------------------------

For qf_uf certificates every definition takes, instead of the Rat valuation,
an interpretation of the uninterpreted sorts, all rendered as one type: a
structure the file declares, quantified as the one argument _m.

    structure Interpretation where
      U : Type
      elems : Nat -> U
      funs : Nat -> List U -> U
      preds : Nat -> List U -> Prop
      bool : Prop -> U

    theorem unsat (_atoms : Nat -> Prop) (_m : Interpretation)
        (_h0 : formula_k _atoms _m) ... : False

Quantifying over the structure is quantifying over its fields; one argument
rather than five keeps every declaration and every reference to it small,
which a certificate of thousands of declarations needs to stay under Lean's
memory cap.

Constants become _m.elems i, an application f(a, b) becomes _m.funs j [a, b], and
a predicate application becomes _m.preds k [a, b]; equality and distinct are
Lean's = on _m.U, and an ite over the sort is Lean's ite over _m.U with the
classical instance, as for Real (its gate clauses are proved the same way).
A Boolean argument p of a function or predicate becomes _m.bool p, so f(a, p)
is _m.funs j [a, _m.bool p]. The theorem quantifies over every type and every indexed
family of functions, so a model of the SMT-LIB input (a nonempty domain with
one function per symbol) is one instance of it: the encoding over-approximates
the class of models and is therefore sound for unsatisfiability. Nothing
relates different indices or different argument lengths, which is exactly the
freedom uninterpreted symbols have. An input with several uninterpreted sorts
is rendered over the same single _m.U, which is sound for the same reason: a
many-sorted model is an instance of the theorem whose _m.U is the disjoint
union of the carriers, with each symbol interpreted as in the model on
arguments of its own sorts (and arbitrarily elsewhere). Bool is one more
such sort: its two values join the disjoint union and _m.bool maps a true
proposition to one and a false one to the other (the instance picks _m.bool
classically). A qf_uflra certificate takes the Rat valuation and the
interpretation together, the structure with two more fields:

    structure Interpretation where
      ... (the five fields above)
      real : Rat -> U
      rfuns : Nat -> List U -> Rat

    theorem unsat (_atoms : Nat -> Prop) (_vars : Nat -> Rat) (_m : Interpretation) ... : False

A Real argument x becomes _m.real x, so Real joins the disjoint union as one
more carrier, and a function with a Real result is the family _m.rfuns, so
(f x) is _m.rfuns i [_m.real x], a Rat term that the arithmetic lemmas treat as
an atom and that congruence closure relates to (f y) once x = y. A
qf_uflia certificate takes the same shape over Int: (_vars : Nat -> Int)
and the fields int : Int -> U and ifuns : Nat -> List U -> Int, with every theory
lemma, rewrite, and argument-equality helper proved by first | omega | grind
as for qf_lia (omega reads applications as atoms; grind proves the
congruences). A qf_uflira certificate takes both valuations as qf_lira,
(_vars : Nat -> Rat) (_ivars : Nat -> Int), and all four fields: an Int
argument is injected by _m.int and a Real one by _m.real, an application
with an Int result is _m.ifuns i [...] and one with a Real result
_m.rfuns i [...] (one numbering for both families), and each theory lemma
takes the sort of its atoms as in qf_lira, an application being one atom
whatever the sorts of its arguments (and an arithmetic ite one atom
whatever the sorts of its condition's atoms). The argument-equality helpers relate
arguments of one sort only: an Int (ite c 1 0) and a Real (ite c 1.0 0.0)
share a linear form but are injected by different maps. Nothing
states that _m.real is injective and no inference needs it: euf lemmas use
only the congruence x = y -> _m.real x = _m.real y, and a model of the input is
again one instance (its Real carrier is the Rat component). grind compares
function arguments as terms, so each grind lemma states the equality of
every pair of reachable Real arguments with the same normal form (for
example (- x y) and (+ x (* (- 1.0) y)), which Z3 identifies, or an ite
and the rewriter's form of it with the condition's complement and the
branches swapped) as a helper it proves first; without arrays the helper is
stated over the two terms' definitions and unfolded in place once proved, so
nested ite arguments are not written out; it is proved level by level, each
pair of corresponding nested ites related first with the ites below them
folded. A to_int is keyed by its argument's normal form, so the floors of
two Real terms with one normal form (to_int of a nested Real ite chain and
the rewriter's form of it) are related too, by congruence from the equality
of the floored terms. The keys are cached and interned per certificate, so
keying a nested chain takes time linear in its depth. The terms a formula
floors (an is_int's argument, a to_int's in a comparison) are paired the
same way, with or without uninterpreted symbols, so (is_int t) and the
rewriter's (= (to_real (to_int t')) t') are related through t = t'.
A certificate whose only uninterpreted symbols are predicates over Bool
uses the same binders with no sort at all: _m.U carries the two
Boolean values, _m.elems and _m.funs are never applied. Every ground term
then denotes its value in the model, and since well-sorted inputs only
compare terms of one sort, every assertion keeps its truth value. Nothing
states that _m.bool True and _m.bool False differ, and no Z3 inference needs it:
the euf lemmas over Boolean arguments use only the congruence
p <-> q -> _m.bool p = _m.bool q, which grind proves through propext, together
with the two cases of each Boolean argument (Z3's egraph assigns every one
true or false), which each grind lemma states as Classical.em first. This
presumes that each symbol name denotes one many-sorted symbol of the input,
which is why overloading a name across sorts is rejected (see above): the
reconstructor binds symbols by name, requires each bound declaration to
carry the input's full signature (argument and result sorts), interns terms
together with their sort, and checks that the certificate is well-sorted
with respect to the input's own sort names before collapsing them, so an
ill-sorted proof graph is rejected rather than rendered. euf th-lemmas and rewrites over the sorts
are proved by grind, whose congruence closure handles the list applications;
Python only checks shapes for these hints, so a false euf lemma is caught by
Lean alone and the file is not published. grind's proofs here report the same
three standard axioms as the arithmetic slice.

An enumeration datatype joins the disjoint union _m.U like any other sort,
and its constructors are one more family of the interpretation, _m.ctors k,
numbered over the input's enumerations (by sort name, each in declaration
order); a recognizer (_ is c) t is t = _m.ctors k. What makes the sort an
enumeration is stated by fields of the structure, read from the input's
datatype declarations and never from the certificate: enum_distinct, that
two constructors of one enumeration differ, and for every constant of an
enumeration sort (enum_cases_i, over _m.elems i) and every function with an
enumeration result (enum_fcases_j, over every argument list of _m.funs j),
that its value is one of the constructors of that sort, all of them whether
the proof names them or not. A model of the input is an instance: the
enumeration's values are the constructors' own, and a function is valued
outside its domain by some constructor of its range. The clause log's
datatype hints (the datatype solver's case splits and constructor clashes)
become th-lemmas over enumeration equalities and recognizers; they, the euf
lemmas, and the cnf fallbacks over such terms are proved by grind after the
fields are instantiated for the constants and applications they reach. The
reconstructor checks every constructor and recognizer of the certificate
against the input's enumeration of that sort and tells constructors apart by
name. An array of an enumeration, (Array I Color), has a field per array
constant (enum_acases_i, over every index of the Lean index type) and per
function into such arrays (enum_afcases_j, over every argument list and
index): each of its reads is a constructor. A model is still an instance, its
arrays extended by a constructor outside the index sort (as in the array
embedding below). A read of a store or of an ite over arrays is a
constructor by the cases of what it may evaluate to (the theorems
_cases_store and _cases_ite); each lemma that reaches a read gets that proof,
built along the read's array down to array constants and applications. A
read of a constant array is its value (_cases_const), and so is the default
value of one (_cases_default_const); the default value of a store is that
of the array below it (_cases_default_store), and the default value of an
ite is that of one of its branches, so it is a constructor if both
branches' default values are (_cases_ite).

An array sort (Array I E) of the clause log is the Lean function type
_m.U -> _m.U, and the array constants are one more field of the
interpretation, arrs : Nat -> U -> U. Each file defines select as _select
(application, kept folded so grind's congruence closure compares reads of
different arrays), store as _store (the classical update at one index),
and the array solver's extensionality witness (_ array-ext 0) as
_array_diff, Classical.epsilon of an index where the two arrays differ,
which needs the field nonempty : Nonempty U (present only then). A model's
array a : I -> E is the function equal to a on I and constant elsewhere;
that embedding is injective and commutes with select and store at indices
of I, and every model's carriers are nonempty, so each model is again an
instance. The array solver's axiom instances (array hints: the store
axiom, select over store, extensionality) are clauses of equalities that
grind proves after each lemma states _store_apply for every read of a
store and _array_ext for every witness it reaches, with _array_diff_comm
(the witness of a and b is the witness of b and a: Z3's congruence
closure takes (_ array-ext 0) as commutative). A read the rewriter
evaluates through several stores gets a fact per level it skips: the
stores at numerals other than the read's ((select (store (store a 1 5) 2
7) 3) is (select a 3)) and the store where that skip stops ((select (store
(store a 3 5) 2 7) 3) is 5), and every store above a constant array (with
_select_const at the bottom); a read of an ite over arrays, which the
rewriter pushes into the branches, gets the facts of a read of each store
or constant-array branch. Array terms stay
folded in those lemmas (term_N, related to its store or ite by an rfl
fact): written out, the shared store chains of the swap and storecomm
benchmarks grow exponentially. A lemma over stores (Z3's rewriter turns
(store (store a i v) i w) into (store a i w) and (store a i (select a i))
into a, and a cnf step over a predicate of such a store relies on it) may
also use _store_store and _store_select, and next to constant arrays
_select_const, _const_store_self ((store (const c) i c) is (const c)), and
_const_eq_store and _store_eq_const ((= (const c) (store (const c) i v)) is
(= c v)), and ite_self (the rewriter drops (ite p c c) first). The
rewriter decides an equality between store chains over two constant arrays
by their values at the stored indices and the constants' values; next to
the facts of that direction, a rewrite or cnf step gets the converse
(extensionality) as a proved fact with one premise per stored index (funext,
a case split on the stored indices, and _store_off down to the constants).
When a side is an ite of different such chains (Z3 logs an asserted
(= (ite p S S') T) as the outcome of comparing each branch with T), each
pair of a leaf of one side with a different leaf of the other gets that
converse over the leaves' terms, for at most 16 pairs per equality.
Each store and constant array a side of such an equality reaches is also
read at every index read from its sort (_store_apply, _select_const): a
cnf lemma may read an array equated to a constant array, (or (not (= a
(const 1))) (not (= 3 (select a k)))), with no read of the constant array.
These reads are stated up to 64 per lemma. All of them are theorems proved in the file, so no array fact is assumed.

An Int or Real index or element sort is Int or Rat itself: (Array Int Int)
is Int -> Int, (Array Int Element) is Int -> _m.U, and each Lean array type
has its own family of constants (arrs_ii : Nat -> Int -> Int; arrs keeps
the arrays between uninterpreted sorts). A read of an Int or Real array is
an atom of the linear forms, like an application of an uninterpreted
function, so Farkas lemmas over reads are checked over them, and an index
is any linear term. The extensionality witness over Int or Rat indices
chooses with Nonempty.intro 0 instead of the nonempty field. An array
argument of a function or predicate is injected into the carrier by one
more field per Lean array type (arrs_ii_inj : (Int -> Int) -> U), like the
numeric injections; lemmas use only its congruence. A model is still an
instance, although no map from U -> U or U -> Int into U is injective
(Cantor): only finitely many array values are denoted by the input's terms,
so U is taken to be the model's carriers plus one fresh point per such
value (arrays over U extended as above, constant off their index sort), the
injection sends each denoted array to its point, and the functions and
predicates read their array arguments back from those points. A function
into an array sort is one more family per Lean array type (arrs_ii_funs :
Nat -> List U -> Int -> Int), taking its argument list like funs and the
numeric families; a model's function into arrays returns its arrays through
the same embedding as the array constants. Its applications stay folded in
the array lemmas like stores, each stated equal to its body (an _t fact), so
grind's congruence closure compares them by their arguments. A Real array is
Rat -> Rat under the argument that values Real variables in Rat: fix the
equalities among the input's terms and the truth values of its atoms; the
reads, applications, and variables left are a linear system with rational
coefficients, so a real model has a rational one with the same equalities,
and arrays over Rat are then defined by the reads at the (now rational)
indices, the store relations and (dis)equalities of arrays included.

A Bool element sort is Prop: (Array Int Bool) is Int -> Prop (the family
arrs_ib, arrs_ub over an uninterpreted index), a read is a formula,
(_select a i) : Prop, and a store's value or a constant array's value is a
formula too. The definitions above are generic in the element type, Prop
included, and a model's set I -> Bool embeds as the predicate true exactly
at its members in I, so the same facts prove the array lemmas; the store
axiom over a Boolean value is a Bool equality (Iff), admitted in an array
lemma only when some array has Bool elements or Bool indices.

A Bool index sort is Prop too: (Array Bool Int) is Prop -> Int (the family
arrs_bi), an index is a formula, and the extensionality witness of two such
arrays is a formula chosen with True ((_array_diff (Nonempty.intro True) a
b)). A model's array a over Bool embeds as fun p => a (decide p), which is
injective and commutes with select and store because equal propositions are
equal (propext), so the generic facts prove the array lemmas. The rewriter
skips a store at false in a read at true as it skips stores at other
numerals, so such reads get every skipped level's _store_apply fact; the SAT
solver identifies (not (not p)) with p, so a unit resolution of the gate
clause (or (not (= (not p) p)) (not (not p)) p) of an index equality
concludes p, which the reconstruction proves by contradiction. Constant
arrays and default values over Bool indices stay rejected (a finite index
sort, like constant arrays over uninterpreted indices).

Nested arrays are functions into or over functions: (Array Int (Array Int
Int)) is Int -> (Int -> Int) (the family arrs_iaii: a nested component is
coded a, then its own two codes), (Array (Array Int Int) Bool) is (Int ->
Int) -> Prop (arrs_aiib). A model embeds its inner arrays first (an
injective embedding that commutes with select and store, as above), then
each outer array as the function equal to it on the embedded indices and
one fixed value elsewhere: two outer arrays that differ do so at an
embedded index, and store (at an embedded index) and ite commute off the
image too, so the same generic facts prove the array lemmas. A pointwise
connective does not commute off the image (the complement of the fixed
value is another value), so maps and set operators over sets indexed by
arrays are rejected by the exporter and by the reconstructor; constant
arrays are admitted over Int and Real indices only, where the embedding
is onto. A read of a row is an array term, and so is the
extensionality witness of two arrays over array indices, chosen with a
constant function from the element type's inhabitant ((Nonempty.elim
(Nonempty.intro (0 : Int)) (fun _e => Nonempty.intro (fun (_ : Int) =>
_e)))), and the default row of a constant array of rows (which the array
solver introduces although the input may not use default). All three are
unfolded in the lemmas, unlike stores and other array terms, which stay
folded, so grind sees them as reads, witnesses, and default values. The
rewriter evaluates a read through a stored row ((select (select (store a i
(store r j v)) i) j) is v) with no read term of the stored row, so every
row stored along the outer store chain gets the facts of a read of it at
the read's index too.

A constant array over Int or Real indices is _const_array Int v (or
_const_array Rat v), the constant function (its reads are _select_const,
rfl). The array solver relates
constant arrays to other arrays through their default values, (default
(const v)) = v and (default (store a i v)) = (default a), logged as array
hints over (default a) terms, which are atoms of the linear forms like reads.
_default is defined on every function I -> E: the value it takes outside
some finite list of indices if there is one (unique, since no finite list
exhausts Int or Rat: _int_unbounded, _rat_unbounded), and otherwise one value that a store does
not change (Classical.choice of a Nonempty proof, which is proof-
irrelevant). _default_const and _default_store are theorems over any index
type that no finite list exhausts. Over a finite index sort no such function
exists (storing at every index turns one constant array into another), so
constant arrays and default terms over uninterpreted indices are rejected
by the exporter and by the reconstructor. Z3's rewriter decides an
equality between stores over constant arrays by their default values or
their values at the stored indices; a rewrite step reaching a constant
array gets those facts for its array equalities.

Maps of not, and, or, => over sets and Z3's set operators (union,
intersection, setminus, complement; Z3 nests n-ary ones into binary ones)
are _map1 f a and _map2 f a b, the pointwise application of a function over
Prop (Not, And, Or, an implication, a difference). A read of one is that
function of the reads by rfl, which is the array solver's select-map axiom,
logged as an array hint stating the propagated equality; each read of a map
gets that fact, and so do the maps, stores, and constant arrays below it,
since Z3's rewriter evaluates a read through all of them with no read term of
the levels in between; a read of a store at another numeral over a map gets
the map's facts too, the rewriter skipping the store. The identities the euf solver and the rewriter apply to
maps are theorems instantiated per map node: maps of and and or commute (euf
compares them as commutative) and are idempotent, a double complement
cancels, a map of stores at one index is the store of the map (a constant
array counting as a store of its value), and a map of constant arrays is
constant. The rewriter turns setminus a b into the map of and over a and the
complement of b, a different Lean function, so each setminus node is stated
equal to that map by rfl; union, intersection, and complement share their
Lean function with the map they become. A map of any other function is
_map1, _map2, or _map3 of a lambda over the element types whose body is the
application as the term and formula renderers write it ((fun (_v0 : Int)
(_v1 : Int) => (_v0 + _v1)), an uninterpreted f as (_m.ifuns k [(_m.int
_v0)])), so the read facts, beta-reduced, match the lemmas' terms. A mapped
function is a symbol of the input even if never applied: the certificate
names it ("declared", f) and the reconstructor binds it to the input's
signature. Maps of commutative functions (xor, =, distinct, +) commute, by
_map2_comm with the pointwise swap proved by grind. The array solver's other map axiom, (default (map f a b)) = (f
(default a) (default b)), holds only for arrays constant at all but finitely
many indices, which _default cannot assume of a map's arguments; the replay
rejects it explicitly. The solver also introduces default values of maps over
any index sort in gate clauses; an untrimmed log's certificate keeps only the
nodes the refutation uses when it has such defaults over an uninterpreted
index, which the reconstructor would otherwise reject.
Z3 logs a map of a built-in with its signature, ((_ map (<= (Int Int) Bool))
a b), and declares a mapped function before the map, so the trimmer reads
map logs back; the replay checks a logged signature against the
application it rebuilds. Logs written before this change print (_ map <=)
and are still read.

The equality rules of a legacy proof object are explicit Lean terms over the
carrier, checked by Lean's type checker without grind: refl, symm, trans, and
trans* between terms are Eq.refl, Eq.symm, and Eq.trans (between formulas
they stay Iff); monotonicity through a function or predicate is congrArg on
the equality of the argument lists, built from one List.cons congruence per
argument, with a Boolean argument's equivalence turned into an equality of
_m.bool applications by propext; monotonicity of equality and distinct over
terms composes Eq.trans in both directions; monotonicity through an ite term
uses a private lemma ite_congr_classical, stated once per file by cases on
propext of the condition equivalence; commutativity of a term equality is
Iff.intro Eq.symm Eq.symm. Python checks the endpoints of every such step as
for the Boolean rules, and a rewrite between two identical formulas or terms
is Iff.refl or Eq.refl in place. The remaining rewrites of a legacy QF_UF
proof (ite simplification, distinct expansion, Boolean simplification over
term atoms) are grind lemmas as for the clause log, and a def-axiom clause
may pair a distinct with the conjunction of its disequalities, which unfold
to the same Lean proposition.

Classical Boolean rewrites, double-negation cancellation in not-or-elim,
def-axiom clauses, and classical steps in lemma discharge use local decidability
witnesses.
The refutation removes these witnesses constructively: given
k : Decidable p -> False, the term
k (isFalse (fun hp => k (isTrue hp))) proves False without assuming decidability.
The final theorem still quantifies over arbitrary Nat -> Prop atom valuations
and takes only the original assertions as hypotheses. Neither it nor the rewrite
and gate-clause lemmas depend on any axioms, sorry, or solver oracles.

The theorem is named unsat inside a namespace derived from the source SHA-256;
the digest is an identifier, not a substitute for checking input equality.
Atoms use generated numeric identifiers, with their original names escaped in
comments. Certificate text is never inserted as executable Lean source.

Trust boundary
--------------

The original file is supplied separately, its text must match source_smt2, and
its parsed assertion DAG must match the certificate's assertion roots exactly,
including order and duplicates. Matching text or result = "unsat" alone does not
authorize a proof. The consumer reparses with Z3's SMT-LIB parser but does not
run Z3's solver search.

Parsing and the Python translation of Boolean expressions, linear
arithmetic, and uninterpreted-function terms into Lean propositions remain
trusted frontend components, not formally verified implementations. Lean
checks the reconstructed theorem, Boolean gate-clause lemmas, rewrite truth
tables, and the grind-proved arithmetic and euf lemmas relative to that
encoding. Boolean equality is encoded as Iff, Boolean xor/ite/distinct as
their logical definitions, Real as Rat under the linearity argument above,
and the uninterpreted sorts as one universally quantified type with indexed
function families. This is not yet a fully formalized SMT-LIB frontend.

The JSON bundle remains marked unverified: successful reconstruction produces
a separate Lean proof artifact rather than changing the producer's claim.

The reconstruction API is reconstruct(source, certificate), which returns
unchecked Lean source, and check_and_write(source, certificate, output), which
checks before publishing. Public API signatures and proof-disabled solving
are unchanged by the preprocessing proof support described below.

Audit preprocessing proof evidence
---------------------------------

proof_preprocessing.py compares two explicit solve-eqs pipelines with proof
generation both disabled and enabled:

    Simplifier("solve-eqs").add(SimpleSolver())
    Then(Tactic("solve-eqs"), Tactic("smt")).solver()

Each run uses a separate context and reports its result, native statistics,
proof terms, rule inventory, and reconstruction/Lean-checking outcome as JSON.
The certificate is always bound to the original input assertions, not the
reduced goal. Checking uses temporary Lean files, which are removed afterward.
This is an opt-in diagnostic, not a replacement exporter or a change to solver
defaults. It currently accepts the same propositional input fragment.

Exercise an essential Boolean equality followed by branching search:

    PYTHONPATH=build/python python3 examples/python/proof_preprocessing.py \
        ../z3test/regressions/proofs/lean/boolean_solve_eqs.smt2 --require-search

Here, removing (= p q) makes the original constraints satisfiable. solve-eqs
eliminates one variable but leaves four clauses; subsequent search reports
positive decision and conflict counts. Also cover goals discharged entirely by
preprocessing, where requiring a search step would be inappropriate:

    PYTHONPATH=build/python python3 examples/python/proof_preprocessing.py \
        ../z3test/regressions/proofs/lean/unit_resolution.smt2

Exit status 0 requires unsat and observed solve-eqs variable elimination in all
four runs, plus successful Lean reconstruction for both proof-enabled runs.
With --require-search, positive decision and conflict counts are also required.
Status 1 reports incomplete coverage or rejected evidence; status 2 indicates an
input, dependency, or invocation error. --timeout-ms bounds each solver check
(default: 10000). Missing statistics mean no execution evidence, not success.

Both examples now exit 0: solve-eqs runs through both interfaces in proof mode,
and the resulting native proofs reconstruct in Lean. Native equality evidence
is carried through extraction, substitution normalization/application, and
solver proof conversion. Congruence proofs are preserved rather than replaced
by unsupported rewrite claims. Boolean unit substitutions use iff-true and
iff-false. Conjunction flattening, replay of eliminated definitions, and tracked
assertions also retain their evidence and original assumption identities.

Proof mode currently supports direct variable equalities, including compound
right-hand sides, and Boolean units. Algebraic/bit-vector isolation, conditional
and nested-equation extraction, and guarded array definitions are skipped until
their own evidence is implemented. A proof-disabled goal still uses the normal
extraction schemes even inside a proof-enabled context. Native support for a
direct equality of another sort does not extend the Lean consumer beyond its
propositional fragment.

Regression coverage includes chained and reversed substitutions, incremental
assertions, push/pop, query assumptions, context translation, and tracked
assertions with single or multiple labels. These are checked against explicit
snapshots of their original active constraints; the exporter certifies one
query of an incremental SMT-LIB script at a time, with the query's
assumptions as hypotheses (see "Input scope").

Preprocessing-only refutations still need checked evidence connecting them to
the original assertions. Conversely, a clausal proof after search only proves
the supplied CNF unless the translation to that CNF is also justified. These
are the two boundaries highlighted in the rutgers-apl/Alivio#1 discussion:
https://github.com/rutgers-apl/Alivio/pull/1#issuecomment-5732956039

Run input-validation/reconstruction tests with the native bindings:

    PYTHONPATH=build/python python3 -m unittest discover -s examples/python \
        -p test_proof_to_lean.py

Include the real Lean integration tests when the pinned toolchain is installed:

    PYTHONPATH=build/python python3 -m unittest discover -s examples/python \
        -p 'test_proof_to_lean*.py'

test_proof_to_lean_arith.py covers the qf_lra slice, test_proof_to_lean_lia.py
the qf_lia slice, test_proof_to_lean_uf.py the qf_uf slice,
test_proof_to_lean_uflra.py the qf_uflra slice, and
test_proof_to_lean_uflia.py the qf_uflia slice,
test_proof_to_lean_lira.py the qf_lira slice, and
test_proof_to_lean_uflira.py the qf_uflira slice, and
test_proof_to_lean_array.py arrays (QF_AX, QF_ALIA, QF_AUFLIA, constant
arrays), and test_proof_to_lean_enum.py enumeration datatypes and arrays
of them end to end;
all need the z3
executable as well and are skipped when none is found.
test_proof_to_lean_deep.py exports and checks inputs nested deeper than
Python's recursion limit; its clause-log tests also need the z3 executable.

These run in a Lean-enabled Ubuntu CMake CI configuration, not the dependency-free
build-script job.
