19.4. Certificates and trust🔗

Parsing produces an executable dense polynomial together with a proof that it denotes the user's expression. Compiled search then finds factors and irreducibility witnesses. The emitted term checks:

• coefficient-level reconstruction of the input;

• one irreducibility certificate for each distinct factor;

• the conversion equality between dense and Mathlib polynomials, when the input uses a Mathlib type.

Finite-field factors use Rabin certificates. Integer factors first try small-prime irreducibility and multi-prime degree obstructions. The factorization and certificate generators are not trusted: only the small checkers and their Lean proofs are part of the logical argument.

The generated proofs use only Lean and Mathlib's documented foundations:

'sqrt2_irred' depends on axioms: [propext, Classical.choice, Quot.sound]