References

1

Anne Baanen, Alain Chavarri Villarello, and Sander R. Dahmen. Certifying rings of integers in number fields. In Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, page 50–66, New York, NY, USA, 2025. Association for Computing Machinery.

2

Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, page 253–266, New York, NY, USA, 2023. Association for Computing Machinery.

3

Vladimir Gladshtein, George Pîrlea, and Ilya Sergey. Small scale reflection for the working lean user, 2024.

4

Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean copilot: Large language models as copilots for theorem proving in lean. NeuS 2025, 2025.

5

Eric Wieser. Computation models for polynomials and finitely supported functions. https://github.com/leanprover-community/mathlib4/wiki/Computation-models-for-polynomials-and-finitely-supported-functions, 2023.

6

Jens Wagemaker. A formally verified proof of the mason-stothers theorem in lean, 2018.

7

Jineon Baek and Seewoo Lee. Formalizing mason-stothers theorem and its corollaries in lean 4, 2024.

8

Markos Dermitzakis. An implementation of buchberger’s algorithm in lean, 2019.

9

Nicholas Dyson, Benedikt Ahrens, and Jacopo Emmenegger. The solutions to single-variable polynomials, implemented and verified in lean, 2022.

10

James Harold Davenport. First steps towards computational polynomials in lean, 2024.

11

Dhruv Bhatia, Eric Wieser, Mario Carneiro, and Thomas Zhu. polyrith tactic. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Polyrith.html, 2022.

12

The Lean Language Reference, chapter The grind tactic. GitHub.

13

Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. Theorem Proving in Lean 4, chapter Type Classes. GitHub.