- Proving Descartes Theorem in Lean
- Project Year:
2022
- REU Student (s):
Archana Mohandas | Massachusetts Institute of Technology MA
- Student 1 Institution:
Massachusetts Institute of Technology
- Project Mentor:
Alex Kontorovich
- Project Mentor Area:
Mathematics
- Project Abstract:
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.
