Title

Formalizing Conway's Little Theorem in LEAN

School Name

South Carolina Governor's School for Science and Mathematics

Grade Level

12th Grade

Presentation Topic

Mathematics

Presentation Type

Mentored

Abstract

LEAN is an interactive proof assistant program that is headed by Project Xena. It uses mathlib, an online, crowdsourced mathematical library containing thousands of formalized theorems and lemmas. LEAN helps users formulate proofs by offering lemmas and theorems, using tactics, and highlighting the goal of the proof. Our goals for the month-long research project were to learn about higher math, learn how to formalize math, learn how to program with LEAN, and formalize a proof to be added to the public mathlib. We spent the first half of the project learning about formal math and how to use LEAN. In the second half of the project, we decided to try to formalize Conway’s little theorem in LEAN. It proves that a certain quality of triangles is exclusive to equilateral triangles: the ratio between two sides and two angles of a triangle being a rational number. We chose to formalize O.A.S. Karamzadeh’s proof of Conway’s Little Theorem. First, we proved that the cosine of double angles is rational. Then we used properties of a Euclidean domain to try to prove that cosine has a finite number of rational outputs, and that they are periodical. Unfortunately, we didn’t have enough time to finish the formalization.

Location

HSS 209

Start Date

4-2-2022 11:30 AM

Presentation Format

Oral Only

Group Project

Yes

COinS
 
Apr 2nd, 11:30 AM

Formalizing Conway's Little Theorem in LEAN

HSS 209

LEAN is an interactive proof assistant program that is headed by Project Xena. It uses mathlib, an online, crowdsourced mathematical library containing thousands of formalized theorems and lemmas. LEAN helps users formulate proofs by offering lemmas and theorems, using tactics, and highlighting the goal of the proof. Our goals for the month-long research project were to learn about higher math, learn how to formalize math, learn how to program with LEAN, and formalize a proof to be added to the public mathlib. We spent the first half of the project learning about formal math and how to use LEAN. In the second half of the project, we decided to try to formalize Conway’s little theorem in LEAN. It proves that a certain quality of triangles is exclusive to equilateral triangles: the ratio between two sides and two angles of a triangle being a rational number. We chose to formalize O.A.S. Karamzadeh’s proof of Conway’s Little Theorem. First, we proved that the cosine of double angles is rational. Then we used properties of a Euclidean domain to try to prove that cosine has a finite number of rational outputs, and that they are periodical. Unfortunately, we didn’t have enough time to finish the formalization.