Looking for Master's thesis co-supervisor or mentor in Lean

Stream: new members

[Samaia Traforti]

CFSG_Project.pdf
Lean_4_Project.pdf

Hello!

My name is Maia, and I've recently completed my undergraduate degree in mathematics at the University of Canterbury in New Zealand. I'm now working towards a Master's degree in mathematics, where I want to do my thesis on formally verifying mathematical proofs using Lean 4. My long-term research interests lie in exploring the intersections between machine learning and automated theorem proving— which is what I hope to expand into for my PhD.

Right now, my main goal is to become fluent in expressing mathematics formally in Lean. I'm looking for an external co-supervisor or mentor who has experience working with Lean 4 to help guide me during my Master's research. This role would involve a weekly online meeting to discuss my progress, share ideas, and help keep my project moving in the right direction, as well as help me to define an appropriate scope for the project at the beginning.

I've spoken with a couple of professors at Canterbury who can support me with the math from this end, but no one at here has any experience with Lean at all, so I've been given the green light to reach out for external co-supervision for specific guidance. I'm really excited about contributing to the digitisation of mathematics and want to 'place my brick in the wall', so to speak, of the collective effort to build this library.

To give an indication of where I'm currently at, I've attached a couple of projects I put together in my undergrad. The first is an introductory exposition on the classification of finite simple groups, and the second is an elementary exploration of the logic behind Lean 4 (with some basic type class implementations in group theory). While neither document is complete (are they ever?), both have been fun places for me to document my personal learning journey and primarily serve as a rough idea of what knowledge I've been building in these areas outside of coursework. My experience in Lean is very limited, so I would be starting at a basic level and hoping to build up substantially throughout the course of the thesis.

If you're interested in advising on my project in any capacity (any and all kinds of advise are welcome), or if you know of anyone who might be able to help, I'd love to hear from you. I'm very committed and excited about this journey, and would greatly appreciate any introductions, recommendations, or advice you might be able to offer!

Thanks so much, and looking forward to hearing from you :big_smile:

Warmest regards,

Maia

[Kevin Buzzard]

Imperial College London offers a 1 year MSc degree in mathematics, with opportunities for formalization: there is a formalization course and the opportunity to do a formalization project.

Univ Lyon in France offered a "Higher Algebra and Formalised Mathematics" course last year -- will this be running again @Filippo A. E. Nuccio ?

Oxford have an MSc in mathematics and the foundations of computer science, although I don't know if there's any lean-specific component there.

I think there's also some foundations of logic course which ran in Amsterdam (the Hitchhikers guide to logical verification was a book which came from a course on that degree) but unfortunately I can't remember the exact name of the program or whether it still exists. @Anne Baanen can you advise on whether I'm talking nonsense about this last MSc course?

[Filippo A. E. Nuccio]

No, it will not run again soon, because the Ecole Normale offers new thematic programs each year and it will take a while before the formalisation team gets another shot. It might happen in 4/5 years, unlikely before.

[Anne Baanen]

The Logical Verification course at VU Amsterdam (from the Hitchhiker's Guide) is very much focussed on computer science. Formal maths can be found quite well represented in the maths department at the VU. Also, there is a MasterMath (so Netherlands-wide) formal math course being run by @Johan Commelin and @Sander Dahmen: https://elo.mastermath.nl/mod/page/view.php?id=333

I think that the MasterMath course is also planned to run in the coming years, am I correct?

[Johan Commelin]

It is at least scheduled for the 25/26 academic year.

[Andrew Yang]

Reading the original post, I have an impression that they are planning to stay in Canterbury and only looking for external co-supervision?

[Shreyas Srinivas]

Kevin Buzzard said:

Oxford have an MSc in mathematics and the foundations of computer science, although I don't know if there's any lean-specific component there.

As an MFoCS alum, I can recommend it a lot, but please keep in mind that you'll effectively have about 4 months for the masters thesis. I don't know whether that's long enough for a formalisation project in your chosen area. The programme is largely designed to get people doing conventional math PhDs or very math-like PhDs outside math departments.

[Jireh Loreaux]

@Samaia Traforti pending further discussion about the details, I would be willing to co-supervise. Please reach out via DM.

[Yaël Dillies]

I am always incredibly busy, but helping bachelor/master students in Imperial College London with their thesis has been a source of great joy for me the past few months. I would be happy to set up some weekly call with you

[Samaia Traforti]

Thank you everyone so much for taking the time to respond! Its so exciting to read about the opportunities available, thank you for sharing those @Kevin Buzzard ! My situation is as Andrew mentioned, I am currently undertaking a Master's in Mathematical Science here at Canterbury looking for external supervision, with the hope to make the shift over to Europe for my PhD. @Jireh Loreaux and @Yaël Dillies , I am so deeply grateful for your offers of support! I will send you a DM to organise a time we can catch up and discuss ideas :) Wow guys, so excited and grateful. Thank you all so much :)