\( %%-------------------------------------------------------------------------------- \usepackage[sc]{mathpazo} % Palatino with smallcaps as text font \usepackage{eulervm} % Euler math \usepackage{mathrsfs} \usepackage{amscd} \usepackage[top=3cm,bottom=3cm,left=3cm,right=3cm]{geometry} \usepackage{amsthm} \usepackage{thmtools} \usepackage{cleveref} \renewcommand{\descriptionlabel}[1]{\hspace{\labelsep}#1} \numberwithin{equation}{section} \declaretheorem[numberwithin=section,Refname={Theorem,Theorems}]{theorem} \declaretheorem[sibling=theorem,name=Proposition,Refname={Proposition,Propositions}]{proposition} \declaretheorem[sibling=theorem,name=Corollary,Refname={Corollary,Corollaries}]{corollary} \declaretheorem[sibling=theorem,name=Lemma,Refname={Lemma,Lemmas}]{lemma} \declaretheorem[sibling=theorem,name=Remark,style=remark,Refname={Remark,Remarks}]{remark} \declaretheorem[sibling=theorem,name=Example,style=remark,Refname={Example,Examples}]{example} \declaretheorem[sibling=theorem,name=Definition,style=remark,Refname={Definition,Definitions}]{definition} %%-------------------------------------------------------------------------------- % power series \newcommand{\pow}[1]{[ \hspace{-1.6pt} [ {#1} ] \hspace{-1.6pt} ]} \newcommand{\powfield}[1]{( \hspace{-1.6pt} ( {#1} ) \hspace{-1.6pt} )} \newcommand{\Spec}{\operatorname{Spec}} \newcommand{\Proj}{\operatorname{Proj}} \newcommand{\nr}{\operatorname{nr}} \newcommand{\Unr}{U_{\nr}} \newcommand{\Knr}{K_{\nr}} \newcommand{\G}{\mathbf{G}} \newcommand{\Mat}{\operatorname{Mat}} \newcommand{\Lie}{\operatorname{Lie}} \newcommand{\GL}{\operatorname{GL}} \newcommand{\SL}{\operatorname{SL}} \newcommand{\Aut}{\operatorname{Aut}} \newcommand{\AAut}{\underline{\textbf{Aut}}} \newcommand{\Out}{\underline{\textbf{Out}}} \newcommand{\Gal}{\operatorname{Gal}} \newcommand{\id}{\operatorname{id}} \newcommand{\Int}{\operatorname{Int}} \newcommand{\OO}{\mathscr{O}} \newcommand{\A}{\mathscr{A}} \newcommand{\B}{\mathscr{B}} \newcommand{\C}{\mathscr{C}} \newcommand{\FF}{\mathscr{F}} \newcommand{\LF}{\mathcal{LF}} \newcommand{\HH}{\mathcal{H}} \newcommand{\X}{\mathscr{X}} \newcommand{\ff}{\mathfrak{f}} \newcommand{\pp}{\mathfrak{p}} \newcommand{\lie}[1]{\mathfrak{#1}} \newcommand{\glie}{\lie{g}} \newcommand{\gllie}{\lie{gl}} \newcommand{\clie}{\lie{c}} \newcommand{\hlie}{\lie{h}} \newcommand{\plie}{\lie{p}} \newcommand{\nlie}{\lie{n}} \newcommand{\mlie}{\lie{m}} \newcommand{\rlie}{\lie{r}} \newcommand{\alg}{\operatorname{alg}} \newcommand{\sep}{\operatorname{sep}} \newcommand{\Kalg}{K_{\alg}} \newcommand{\Lalg}{L_{\alg}} \newcommand{\Kun}{K_{\un}} \newcommand{\Lun}{L_{\un}} \newcommand{\Gun}{G_{/\Kun}} \newcommand{\Sun}{S_{\un}} \newcommand{\Aun}{\A_{\un}} \newcommand{\Fsep}{F_{\sep}} \newcommand{\Ksep}{K_{\sep}} \newcommand{\Lsep}{L_{\sep}} \newcommand{\Qalg}{\mathbf{Q}_{\alg}} \newcommand{\Fpalg}{\mathbf{F}_{p,\alg}} \newcommand{\ksep}{k_{\sep}} \newcommand{\kalg}{k_{\alg}} \newcommand{\mm}{\mathfrak{m}} \newcommand{\nn}{\mathfrak{n}} \newcommand{\GG}{\mathcal{G}} \newcommand{\parah}{\mathcal{P}} \newcommand{\qparah}{\mathcal{Q}} \newcommand{\parahun}{\mathcal{P}_{\un}} \newcommand{\PP}{\mathbf{P}} \renewcommand{\SS}{\mathscr{S}} \newcommand{\Z}{\mathbf{Z}} \newcommand{\Q}{\mathbf{Q}} %%-------------------------------------------------------------------------------- \)

Formalization and “finite algebra”

Project Description

In the field of pure mathematics, there is widening interest in the possibility of formalizing proofs of mathematical statements. The project will involve learning to use the Lean proof assistant to formalize mathematics of finite geometries.

The introduction to the book Mathematics in Lean (available online) describes formalization as follows:

Formalization can be seen as a kind of computer programming: we will write mathematical definitions, theorems, and proofs in a regimented language, like a programming language, that Lean can understand. In return, Lean provides feedback and information, interprets expressions and guarantees that they are well-formed, and ultimately certifies the correctness of our proofs.

For example, the following code (depending on the mathlib library) defines the notion of a left coset of a subgroup \(H\) in a group \(G\) and proves that if two cosets \(xH\) and \(yH\) are equal then \(x \in yH\). 

import Mathlib.Tactic

variable {G : Type} [Group G]

def leftCoset {G : Type} [Group G] (H : Subgroup G) (x:G): Set G := 
  { y:G | ∃ h ∈ H , y = x*h }    

lemma contain {H : Subgroup G} {x y : G} :
  leftCoset H x = leftCoset H y → x ∈ leftCoset H y := by 
    intro h
    have hx : x ∈ leftCoset H x := by
      use 1
      constructor
      · exact Subgroup.one_mem _
      · group
    rw [h] at hx
    assumption

Broadly speaking, the goal is to learn to use formalization to develop mathematics. Thus, we should first target results in a particular part of mathematics for formalization. Here, we’ll choose to study the algebra and geometry arising in the study of finite vector spaces (i.e. of finite dimensional vector spaces over finite fields). We'll hope to build on existing formalization already in place in mathlib. There should remain many interesting results to formalize in this setting: basic properties of finite projective and polar spaces, results about error-correcting codes, etc.

Desired Background

A project participant should have some background in algebra (completion of an undergraduate course introducing groups, rings and fields should suffice). Part of our time will be spent learning to use the formalization tools; this phase will probably be quicker for candidates having some familiarity with computer programming.