A key result in algebraic geometry states that for X a locally Noetherian scheme, X is normal if and only if X has properties (R1) and (S2). This result follows from the local result in commutative algebra known as Serre's criterion for normality. In this talk I will describe the geometry behind Serre's criterion and its proof, as well as my ongoing formalization of the result and what is required to complete it.
For millennia, mathematicians have attempted to answer the question: "What is a number?". In this talk, I will.
We will give an amateur introduction to dependent type theories (like those implemented in Lean) focusing on Martin-Loff type theory and its extension 'homotopy type theory'.
We give an introduction into the history of proof assistants, recent formalization projects, and describe typical challenges when formalizing mathematics.
We demonstrate how to use prove theorems in Lean, in the process learning the most common tactics and how to write idiomatic Lean code.
Before the seminar, we will assist in installing Lean and mathlib from 2.30pm in Room 107 Greg Hjorth.Machine learning for theorem proving has classically focused on lemma selection and guidance of automated reasoning processes, where statistical methods help navigate large formal libraries and search spaces. More recent work has expanded this perspective toward coming up with useful conjectures or even theory exploration, refocusing the attention from supervised tasks on given statements to proposing useful new ones. In the second half of the talk I will turn to our most recent results on automating large parts of the formalization process, combining modern LLMs with proof automation. I will discuss the direct use of multiple collaborating LLMs, providing them with effective formalization incentives, and ways such approaches can be supervised towards a particular mathematical goal.
Formalising mathematics demands paying attention to things typically taken for granted, and this includes ensuring lemmas that apply to a additive group or a ring naturally apply to a field, with minimal friction. In traditional mathematics this would be as short as to note a field is an additive group in its operations, but to treat the field as an additive group, the field properties are implicitly forgotten. In Lean 4, this is done via the type-class system, such that when one states there is a field 'instance', this also comes with the appropriate instances that build up to the field. Conversely, if for example one defines and proves a field instance on the reals, it will automatically come with the associated substructures and operations. This talk describes how the type class system has been used to build up algebraic structures in Lean 4 and mathlib, assuming minimal previous knowledge of Lean.