Formalising Hilbert Polynomials in Lean
File(s)
Accepted version
Author(s)
Li, Fangming
Zhang, Jujian
Type
Conference Paper
Abstract
In commutative algebra and algebraic geometry, Hilbert polynomials are an important tool used in the proof of Bézout’s Theorem, the construction of Hilbert schemes, and so on. We have used the proof assistant Lean to formalise the Hilbert polynomial of a graded module. Several times, we discovered issues which were not present in the informal proofs but which mattered in the formalisation. As the notions of Hilbert polynomials associated with other algebraic structures rely on the version we have formalised, our project provides a foundation for the future formalisation of them.
Editor(s)
Naumowicz, Adam
Seidl, Martina
Date Issued
2026-09-29
Date Acceptance
2026-06-11
Citation
Intelligent Computer Mathematics, 2026, 16907, pp.216-231
ISBN
978-3-032-38214-6
ISSN
0302-9743
Publisher
Springer
Start Page
216
End Page
231
Journal / Book Title
Intelligent Computer Mathematics
Volume
16907
Copyright Statement
© 2027 The Author(s), under exclusive license to Springer Nature Switzerland AG. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Identifier
https://orcid.org/0009-0006-0967-6746;%20https://orcid.org/0000-0001-7340-2703
Source
The 19th Conference on Intelligent Computer Mathematics (CICM 2026)
Subjects
Algebraic geometry
Commutative algebra
Formalisation
Hilbert polynomial
Lean
Place of Publication
Cham, Switzerland
Publication Status
Published
Start Date
2026-09-21
Finish Date
2026-09-25
Coverage Spatial
Ljubljana, Slovenia
Date Publish Online
2026-09-29