| Name: | Archana Mohandas |
|---|---|
| Email: | amohanda@mit.edu |
| Home Institution: | Massachusetts Institute of Technology |
| Project: | Hyperbolic Geometry in the Lean Theorem Prover |
| Mentor: | Professor Alex Kontorovich |
About My Project
Lean is an interactive theorem prover which reduces mathematical proofs to a set of foundational axioms. The current challenge of using Lean is that full axiomatic proofs are detailed and complicated. Lean becomes more adept at theorem proving as more proved theorems are added to its library. Our goal in this project was to prove Descartes' Theorem and its generalized version, the Soddy-Gossett Theorem, in Lean using inversive geometry. By developing inversive geometry in Lean through the proof of Descartes' Theorem, other proofs which use inversive geometry can be more easily proved in Lean.
Research Log
Week 1: May 30 - June 4
On Wednesday, I met with Professor Alex Kontorovich to discuss potential projects in pure mathematics. Eventually, we decided that developing a proof of Descartes' theorem in Lean would be a good starting point to work towards the eventual goal of building hyperbolic geometry capabilities in Lean. I spent the rest of the week reading "Integral Apollonian packings Peter Sarnak MAA Lecture" to understand the proof of Descartes' theorem using circular inversions. On Friday, I finished my project overview presentation and went over it with Professor Kontorovich.
Week 2: June 6 - June 10
This week, I began experimenting with Lean and learning about which theorems already existed that could be used in the hyperbolic proof of Descartes' theorem. I did not make much progress because I realized I needed more practice familiarizing myself with Lean notation and proof structure. I met with Professor Kontorovich to discuss both Lean and some hyperbolic geometry. Professor Kontorovich explained the connection between the upper half-plane and the hyperboloid model and after conducting the calculations myself, my understanding of the hyperboloid model became much clearer. I plan to work on some more calculations in the next few days before practicing Lean next week.
Week 3: June 13 - June 17
I read and took notes on the paper by Lagarias, Mallows, and Wilks which discusses multiple versions of Descartes' Theorem, including a proof of complex Descartes' theorem, Descartes theorem using spherical geometry and Descartes theorem using hyperbolic geometry. After reviewing my notes with Professor Kontorovich, we decided that reading sections from Iverson's Hyperbolic Geometry would be the best approach to understanding concepts leading up to the hyperbolic geometry used in the proof of hyperbolic Descartes' theorem. From there, we will decide which proof of Descartes Theorem is the most self-contained and thus, could most easily be implemented in Lean while still developing useful concepts in hyperbolic geometry that can be used in proofs of other theorems.
Week 4: June 20 - June 25
This week I continued reading the Lagarias, Mallows, and Wilks proof of Descartes Theorem using spherical geometry. While this proof does not follow the exact approach we will be using to prove Descartes' Theorem in Lean, the idea of using inversive coordinates to show tangent spheres is in a similar vein to the methods we will be using. I also typed up my notes from the papers I have read thus far in Latex in my own words in order to clarify holes in my understanding. This was extremely helpful in compiling the various ideas from different papers that we plan on using in our proof of Descartes' Theorem.
Week 5: June 28 - July 1
After discussing the proof of Descartes' Theorem further with Professor Kontorovich, we decided that the best approach to showing that the Q-product between the vectors associated with two tangent spheres is equal to 1 was to algebraically show that the Q-product equation and the equation relating radii of tangent spheres were equivalent. The approach we were initially going to take was to show that the Q-product of two geodesics is equal to the generalized hyperbolic distance. We decided that this approach, while more general, would be difficult to prove quickly and was not necessary for our goal of proving Descartes' Theorem in Lean. This week, I worked on showing this equivalence and adding the proof to my Latex notes.
Week 6: July 3 - July 8
This week I finished writing the proof of the why the Q-product of two inversive coordinates associated with tangent circles is -1. Professor Kontorovich and I then began working on implementing the entire proof of Descartes' Theorem in Lean. We divided the proof in Lean as follows: defining inversive coordinates, defining the product of inversive coordinates and the lemmas stating that the Q-product of inversive coordinates associated with tangent circles is 1 if the circles are different and -1 f the circles are the same. So far, we have successfully implemented all necessary definitions in Lean but are still working on proving the lemmas. Once the lemmas are proved, we can (hopefully) easily combine the definitions and lemmas to prove Descartes’ theorem.
Week 7: July 11 - July 15
Learning Lean syntax and formatting has been the main challenge thus far, but with the assistance of other Lean users in Zulip and Professor Kontorovich, I have been able to make some progress. This week, we worked on implementing all lemmas used in Descartes’ Theorem in Lean. Our main obstacle was learning linear algebra in Lean but we were able to figure out most of the complications we came across regarding matrix operations. I am also trying to implement a recently announced tactic in Lean called polyrith to replace the linear combination tactic in order to simplify the lemma stating the tangency condition for two circles.
Week 8: July 18 - July 22
This week, I compiled the work I've completed so far and creating a final presentation for the end of the DIMACS program. For the presentation, I decided to focus on explaining the proof of Descartes' and then briefly discussing the implementation of the proof in Lean. I also met with Professor Kontorovich to discuss some holes in the working proof of the Soddy-Gossett Theorem such as the calculation of the inverse Gram matrix and the calculation of the final statement of the Soddy-Gossett Theorem using the Q-inverse matrix.
Week 9: July 25 - July 29
This week, I wrote up the final proof of the generalized Descartes' Theorem, or, Soddy Gossett's Theorem. In the previous week, Professor Kontorovich cleared up some misconceptions I had about the working proof, which made it much easier to write up the final proof of the theorem. Developing a proof of Soddy-Gossett's Theorem that uses inversive geometry is a useful step towards advancing the Lean library and allowing more complex theorems to be proven in Lean. In this project, we produced a concise proof of Soddy-Gossett's Theorem using inversive geometry and began the implementation of the proof in Lean. Thus far, we have defined important concepts that are necessary in the proof such as the definitions of the co-radius, inversive coordinates, the inner product, and the inner product matrix. However, the more complex preliminary lemmas and the main statement of Soddy-Gossett's theorem are still in the process of being proved. A future goal after the conclusion of this project would be to complete the proof of Soddy-Gossett's Theorem in Lean and eventually extend the ideas of this proof to other theorems whose proofs can be simplified using inversive geometry.