1 Introduction

1.1 Organization of the Blueprint

The blueprint is organized as follows: The rest of Section 1 examines previous work in proof automation and polynomials in Lean, and provides a brief comparison with the approach taken in our work. Section 2 describes our approach to proof by reflection and outlines a model for its implementation. This section will also be of interest to readers curious about our use of type-class inference in proof automation. Section 3 details the implementation of each part of the model for univariate polynomials. Readers interested in using the univariate system for proof automation should be directed specifially to Section 3.4. Section 4 addresses ongoing work towards a system for multivariate polynomials.

1.2 Automation in Lean

Previous work outlines a number of approaches to proof automation in Lean 4, each with different advantages and preferred applications. The Ring of Integers project [ 1 ] covers proof automation methods in Lean extensively and may be referenced for a more technical address of the topic. This blueprint will introduce and evaluate proof automation strategies in previous work as it relates to our approach. We broadly refer to these strategies as proof by reflection.

One proof-by-reflection paradigm is white-box automation [ 2 ] , in which the automation procedure is transparent and simple enough for users to trace and predict how an application will deal with their goals. Although these solutions tend to be narrow-application in terms of the goals they can deal with, they are highly extensible to different contexts since the user can understand and customize them. Search tactics such as aesop [ 2 ] and reflection models such as LeanSSR [ 3 ] are common examples of such automation. While alternative proof-by-reflection paradigms such as LLMs are more general-application, they tend to be more brittle to changes in context and difficult to debug due to their complexity. There have even been recent efforts to make these solutions more usable by integrating them as assistants in the interactive-proving process, using them to resolve subgoals instead of relying on them for complex theorems. Lean Copilot [ 4 ] , for instance, integrates their LLM implementation with aesop’s search, resulting in a white-box solution with some of the general-application benefits of LLM automation.

Popular implementations also tend to be native to Lean since they are easier to use, entail less dependencies, and enjoy the benefits of Lean’s powerful tactics and metaprogramming. For instance, Lean Copilot [ 4 ] implements their Lean declarations in C++, to which Lean compiles directly. Moreover, LeanSSR [ 3 ] emphasizes how Lean is a great candidate for implementation of their reflection model because of its powerful metaprogramming support. LeanSSR also discusses how Lean’s flexible tactics for goal manipulation result in convenient “last-mile automation” strategies, where the user only needs to manipulate the goal to a point where it can be automatically resolved by some form of reduction. For example, the built-in tactics rfl and simp automate a variety of goals by reducing them according to simple rules. Our native approach makes generous use of these last-mile automation strategies. Overall, it seems that native, white-box automation is a leading contender for Lean.

Type-class inference, which our project employs to construct computable representations, seems unexplored as a search method compared to metaprogramming and search tactics. We find in our project that it greatly simplifies resolving goals that can be split into similar subgoals without much additional verification at each step. However, it requires additional help from tactics when verification beyond the scope of the procedure is necessary at any step (see Section 2.3).

1.3 Polynomials in Lean

Previous work with polynomials in Lean highlights how a lack of computable representations can limit the impact of a formalization. As described by Wieser [ 5 ] , polynomials in Mathlib are non-computable because they are implemented using the Finsupp type for finitely supported functions, whose underlying support set may not have decidable membership. An early Lean 3 formalization [ 6 ] aimed to prove the Mason Stothers Theorem. The project achieved this goals, though it first had to build up the necessary background in number theory and polynomials. A later project [ 7 ] which achieved the same formalization using Lean 4’s Mathlib noted that the previous project’s rejection of established machinery limited its application and reusability. This is because its results cannot be easily related to the standard Mathlib definitions used in other projects.

Some projects take advantage of the computational benefits of machine formalization, implementing algorithms on polynomials in Lean. One project implemented Buchberger’s Algorithm [ 8 ] but noted that Mathlib’s non-computable polynomial representation made it ineffective for their application. The authors implemented their own polynomials for use in their implementation, limiting its reusability similarly to the projects dealing with the Mason Stothers Theorem. Another project [ 9 ] implemented algorithms for finding solutions to univariate polynomials, but built their mathematical machinery—all the way from natural numbers—from scratch. Although an impressive look into what it takes to formalize such mathematical background, this definitional separation limits the project in the same ways as the previous one.

Recent work focuses on more computable representations and automations for polynomials in Lean. Davenport [ 10 ] outlines the design decisions towards implementing such a representation and some operations on it. However, he does not detail any proof of correctness for those operations, and instead discusses verification using SageMath. Another approach to automation is Wieser’s polyrith tactic [ 11 ] , which uses SageMath to compute necessary parameters for resolving a goal with Mathlib’s linear_combination tactic. It is a highly effective white-box method for polynomials over fields. In both these methods, proof automation is non-native. Our approach introduces a computable representation and correctness-verified operations all native to Lean. Furthermore, the representations do not require polynomials defined over fields, only commutative semirings in the most specific cases, making the solution more general than polyrith in this aspect.

The Ring of Integers project [ 1 ] briefly discusses construction of computable representations based on expressions in the current goal as a proof automation method. They also discuss their list-based implementation of a computable representation for polynomials which is similar to our list-based implementation. However, they explain as a limitation that their implementation does not provide such a way to automatically construct this representation. This type of automated construction is central to our approach and is achieved using the unexplored method of type-class inference (recall Section 1.2). For these reasons, we consider this aspect the most novel contribution of our work.

It should be noted that the powerful grind tactic [ 12 ] for automated reasoning over finite algebras became available in Lean during work on this project. For its Gröbner basis computations, the system ships with a computable representation of polynomials implemented by the Poly type (see Poly.lean) and automated construction methods for it. It is still unclear how those automated construction methods compare to those used in our project, though future work may explore this question as well as how adoption of the convenient Poly type could improve our system.