Wenrong Zou

From September 2026, I am a Ph.D. student at the Institut Camille Jordan, Université Jean Monnet Saint-Étienne, working with Filippo A. E. Nuccio and Riccardo Brasca. My Ph.D. is part of the ANR project FALSE (Formalising Arithmetic in the Lean Software Environment).

I am interested in the formalisation of mathematics in the Lean proof assistant, especially mathematics related to number theory. More on the research page.

Before that, I completed my M.Sc. in Mathematics at the University of Bonn under the supervision of María Inés de Frutos-Fernández and Floris van Doorn, and obtained my bachelor's degree at Sichuan University.

Awards

• AI for Math Summer Fellow, AI for Math Fund at Renaissance Philanthropy, whose founding donor is XTX Markets. Project: Robo, mentored by Marcus Zibrowius.

Education

• 2026 – Ph.D. in Mathematics, Institut Camille Jordan, Université Jean Monnet Saint-Étienne
  Advisors: Filippo Nuccio and Riccardo Brasca. ANR project FALSE.
• 2024 – 2026 M.Sc. in Mathematics, University of Bonn
  Advisors: Floris van Doorn and María Inés de Frutos-Fernández
  Master's thesis: “Formalization of Formal Group Laws” with grade 1,0 (sehr gut)
• 2020 – 2024 B.Sc. in Mathematics and Applied Mathematics, Sichuan University
  Advisor: Bin Xu
  Bachelor thesis: “Cohomological methods for the proof of local class field theory and their applications” with grade 4.0/4.0