Abstract

Polynomials are crucial to cryptographic protocols for their error-checking applications. Proof assistants like Lean 4 enable machine-verified implementations of those protocols, yielding more correct and secure systems. While those implementations demand an efficient way to prove properties of polynomials in Lean, representations of polynomials in Lean’s mathematics library are not directly computable, making simple results tedious to prove. To address this issue, we design and implement a general proof-by-reflection model in Lean, reducing mathematical problems to decisions on computable representations.

The resulting systems automate proof of degrees, coefficients, evaluations, and expansions for univariate and multivariate polynomials in various contexts. The model’s design specifies three levels of abstraction, producing modular and reusable tactics that are generic to computable representations of properties. We demonstrate this by exploring representations such as lambda functions for evaluations, dense lists for univariate coefficients, and dense trees for multivariate coefficients. Sparse and array representations are priorities for future work to improve efficiency. This work provides automated proving tools for polynomials and a general proof-by-reflection model for Lean, contributing to the development of reliable, machine-verified systems.