Certifying rings of integers in number fields
summary
Lean 4 formalization certifies explicit integral bases and discriminants for number fields by having SageMath generate SageMath → Lean certificates that the checker imports; implementation builds computable polynomials as coefficient lists, a subalgebra‑builder and multiplication tables, and a Posten House criterion for p‑maximality. The work verifies entries from LMFDB including 142 non‑monogenic degree‑5 fields, produces ~13,000 handwritten lines plus ~32,000 generated Lean lines, checks a typical degree‑5 proof in about 30s proof‑check, and currently limits examples to degrees under eight.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 3:14Motivation in number theory
- 4:17Number fields and rings
- 8:56Problem in Lean
- 10:22Polynomial arithmetic
- 12:07Constructing O in Lean
- 17:29Proving O is ring of integers
- 21:47Lean proofs from SageMath
- 22:51Verifying L-functions data
- 23:58Future directions
- 24:19Q&A
related talks
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
20mFormalizing polynomial laws and the universal divided power algebra
25mFormalising Perfectoid Spaces
30mTrustworthy Formal Natural Language Specifications
58mFrom Formal Verification to Correctly Rounded Math Libraries
22mThe Lean Mathematical Library
23mGenerating Programs for Polynomial Multiplication with Correctness Assurance
19mAutomated Verification of Fundamental Algebraic Laws