University of Cambridge > Talks.cam > Number Theory Seminar > Formalising modular forms, Eisenstein series and the modularity conjecture in Lean

Formalising modular forms, Eisenstein series and the modularity conjecture in Lean

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Rong Zhou.

I’ll discuss some recent work on defining modular forms and Eisenstein series in Lean. This is an interactive theorem prover which has recently attracted mathematicians and computer scientists who are working together to create a unified digitised library of mathematics. In my talk I will explain what Lean is and explain the process of taking basic definitions/examples of modular forms and formalising them.

This talk is part of the Number Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity