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.
