| Name: | Emma R. Hasson |
|---|---|
| Email: | ehasson20@simons-rock.edu |
| Home Institution: | Bard College at Simon's Rock |
| Project: | project |
| Mentor: | Alex Kontorovich |
About My Project
I will be working on formalizing theorems in Elementary Analytic Number Theory using the interactive theorem prover Lean. I hope to contribute my work to MathLib- a library of formalized math in Lean.
Research Log
Week 1:
June 1 - June 3
The program began on Wednesday. We had orientation and I met with my advisor, Alex Kontorovich, and the rest of our research team. Throughout the short week, we discussed potential projects and I got aquainted with Lean, the theorem-proving software I'd be working with. By the end of the week we made presentations on our chosen projects to be presented on Monday. Our reaserch group ran the preliminary presentations for each other on Friday.
Week 2:
June 6 - June 10
This week I studied the sources Alex provided me a gained a much stronger understanding of the concepts I'd be working with in Analytic Number Theory. I took some time to break down some potential goal theorems into the smaller parts I would need to formalize. I got to know Lean better by sudying some proofs in my area and playing the Natural Number Game. On Friday Lazaros gave us a seminar on research ethics. Afterwards, we met with Alex to review our progress and solidify our goals for the next week.
Week 3:
June 13 - June 17
This week I worked with the sample document- fixing small to medium errors and fixing code which was no longer up-to-date. I used mathlib documentation to guide my work and got familiar with some common tactics used to prove theorems in Lean. Ultimately I got the code down from over 40 major errors to just a few by the end of the week.
Week 4:
June 20 - June 24
This week I worked on parsing and organizing the larger unproven theorems. I completed some proofs that were incomplete. Each incomplete proof required careful effort. I began by understanding the statement of the theorem, then thinking about how it might be proven and breaking the proof into very small parts to be formalized. I worked on understanding the parts of the proof that were already there, sometimes working off that and other times starting over with my own method. Also this week was the Data Science Bootcamp.
Week 5:
June 27 - July 1
This week I worked on some of the entirely unproven theorems. I unfortunately did not get as far as I would have liked, only managing to complete a couple of theorems. Writing a proof from scratch requires a much stronger basis in lean and also firm understanding of the material, both of which I continue to work on. I also joined the Lean discussion server on Zulip. It is interesting to see what projects others are working on with respect to Lean. On Tuesday we had a seminar on Data Encryption and on Thursday we discussed scientific writing.
Week 6:
July 5 - July 8
On Tuesday, James Abello gave us a talk about his graph cities project. This week I got to working on the theorems related to the hyperbola method. I learned about splitting logical arguments and different methods for working with sums in Lean.
Week 7:
July 11 - July 15
After much work put into the theorems leading up to the hyperbola method we decided to restructure the entire proof. This involved going back through all the related theorems and changing the statements. Of course this would also require starting the proofs from the beginng. I began with the region_split argument and went from there.
Week 8:
July 18 - July 22
This week I worked on proving some theorems including region_split and hyperbola prelim. I also worked on my final presentation. I decided against using slides and instead split it between a board presentation and a code demonstration. The presentation went well. If I'd had more time I would have spent longer on explaining the Lean code.
Week 9:
July 25 - July 29
This week I worked on my final paper. I went through describing the hyperbola method and analytic number theory in general. I found a way to display Lean code neatly in LaTeX. Then I described a few of the key theorems I formalized. Next steps are to push the code I wrote to mathlib.
Acknowledgement
This work was carried out while the author Emma R. Hasson (ERH) was a participant in the 2022 DIMACS REU program at Rutgers University, supported by NSF grant DMS-1802119. Thank you to the DIMACS REU program for providing this opportunity and Dr. Alex Kontorovitch for being a wonderful mentor.