Explaining the finiteness of the class group of a number field to a computer

Abstract: A proof-assistant is a computer program that can digest a mathematical proof, implemented as a chain of statements. If all statements follow logically from previously proven ones, then the assistant is happy, and certifies the correctness of the proof; if it is doubtful about a certain point, it will not let you continue until it gets convinced. Among other proof assistants, Lean3 is getting popular among some "classical" mathematicians, who are formalising well-known proofs in order to shape a larger and larger mathematical library upon which subsequent work can rely. In this talk, I will show how to discuss with Lean3, I will show some examples and I will report on a recent work, joint with A. Baanen, S. Daamen and Ashvni N., where we formalised the finiteness of the class group of a number field in Lean3.

number theory

Audience: researchers in the topic

Algebra and Number Theory Seminars at Université Laval