def Hex.ECPP.convertSupplied (source : String) : Lean.MetaM (Except ImportError Cert)

Convert PARI certificate text while searching for a proof of the last prime in its chain. The search uses the existing primality elaborator's finite policy. To obtain a Lean theorem, the returned certificate must still be passed to ecpp using, which verifies it in the kernel.

Equations

• One or more equations did not get rendered due to their size.

def Hex.ECPP.certProof (cert : Cert) (n : ℕ) (nE : Lean.Expr) : Lean.MetaM Lean.Expr

Produce the subject-bound proof from checked raw constructor data.

Equations

• One or more equations did not get rendered due to their size.

def Hex.ECPP.ecppUsingTac : Lean.ParserDescr

Produce Nat.Prime n from an explicit, checked ECPP certificate.

Equations

• One or more equations did not get rendered due to their size.

def Hex.ECPP.evalEcppUsing : Lean.Elab.Tactic.Tactic

Elaborate explicit certificate replay for a closed Mathlib primality goal.

Equations

• One or more equations did not get rendered due to their size.