# 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.

## Recommended Citation

Clements, Adam; Long, Christian; Morton-Lill, Case; and Samuel, "Formalizing Conway's Little Theorem in LEAN" (2022). *South Carolina Junior Academy of Science*. 111.

https://scholarexchange.furman.edu/scjas/2022/all/111

## Location

HSS 209

## Start Date

4-2-2022 11:30 AM

## Presentation Format

Oral Only

## Group Project

Yes

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.