Determining the satisfiability of formulas involving nonlinear real arithmetic and transcendental functions is necessary in many applications, such as formally verifying dynamic systems.

Doing this automatically generally requires costly and intricate methods, which limits their applicability.

In the context of SMT solving, \emph{Incremental Linearization} was introduced recently to facilitate reasoning on this domain, via an incomplete but easy to implement and highly effective approach.

The approach, based on abstraction-refinement via an incremental axiomatization of the nonlinear and transcendental operators, is currently implemented in the SMT solvers \textsc{MathSAT} and \textsc{cvc5}.

The cvc5 implementation is also proof-producing.

This paper presents two contributions: a formalization of the proof calculus employed by cvc5 using the Lean proof assistant and an extension of the lean-smt plugin to reconstructing the proofs produced by cvc5 using this proof calculus.

These contributions ensure the soundness of the proof calculus, making the underlying algorithm more trustworthy, and enable users to check cvc5 results obtained via incremenation linearization, as well as improve Lean’s automation for problems in nonlinear arithmetic.

We discuss how we modeled the rules in the proof assistant and the challenges encountered while formalizing them, as well as the issues involved in reconstructing proofs involving these rules in Lean, and how we solved them.