Person. Cheni Yuki Yang [yuki]

The name was written as Chenyi Yang before. In Chinese it is written as 「楊晨翌」

她會說吳語，普通話，英語，德語和一些日語。她汲取著多語言的知識和美，以期對抗單語和短視的魔咒。

她將長門 有希視作自己的倒影和理想人格。她此生的夙願可能是做一個通天圖書館的管理員，直至死亡將她與知識分離。

很幸運的是，她生來便很喜歡做純粹邏輯性的思考並感謝上蒼。她追求所有美麗的數學知識，並在可見的將來也會繼續如此。

Curriculum vitæ [cv]

    Education [education]

      I am a first year PhD student at Universität Heidelberg, under the supervision of Alberto Merici.

      From October 2024 to February 2026, I was a master student at Universität Heidelberg. I wrote my master thesis about motivic homotopy theory under the supervision of Alberto.

      From October 2022 to July 2024, I studied mathematics with a minor in physics at Universität Heidelberg. I wrote my bachelor thesis under the supervision of Florent Schaffhauser.

      Research interests [interest]

        I am interested in homotopy theory, especially the motivic homotopy theory and its relation to algebraic $K$-theory, arithmetic cohomology and geometry. Currently, I am thinking about the $p$-adic rigidity of motivic homotopy category, using logarithmic techniques.

        I have an interest on formalizing mathematics too, in particular, algebra in LEAN and homotopy theory in HoTT. Actually, the first inspiration that guides me to study maths is type theory. My bachelor thesis is just about homotopy type theory.

        Workshops and conferences [conf]

          You will find me in the following coming activities:

          Workshop. Bridging Lean and the LMFDB [uea_2026_lean_lmfdb]

          This workshop will feature tutorials to navigate the number theory programming interface in Lean’s mathematical library (number fields, elliptic curves, modular forms, etc), as well as a variety of research talks in relevant areas of number theory.

          Conference. CATS 8 - A conference in honour of Gabriele Vezzosi’s 60th birthday [cnrs_2026_cats8]

          I have participated in:

          Conference. Graduate Research Opportunities for Women 2025 [fra_2025_GROW]

          GROW@Frankfurt 2025 is for all students of underrepresented gender identities in mathematics, especially female students, who are interested in learning about graduate programmes and further opportunities in research, both within and outside academia.

          Workshop. CMI-HIMR summer school on formalizing class field theory [oxford_2025_cmi]

          The Github repo is: kbuzzard/ClassFieldTheory.

          I formalized part of Tate cohomology and local fields.

          Class Field Theory in its cohomological form is one of the highlights of early 20th century mathematics, and is now understood as the abelian case of the Langlands Philosophy. Although it sounds like science fiction to many mathematicians, some computer scientists are arguing that AI methods are progressing so fast that soon computers will be helping humans to push back the boundaries of research in the Langlands Philosophy. However, there is currently no concrete evidence that this is happening. Furthermore, using a language model alone to do mathematics at this level is problematic, because language models are error-prone, and one error in a mathematical argument invalidates it.

          This summer school does not have anything to do with AI, but it has a lot to do with class field theory. During the school, we will be teaching class field theory to the Lean theorem prover. You can imagine the school as a group of people collaborating on writing a Bourbaki-like document explaining class field theory. Or you can imagine it as a group of people turning class field theory into a bunch of levels of a puzzle game and then solving these levels. Or you can imagine it as a group of people creating training data for a theorem prover-backed AI which can then try and learn some of these interesting mathematical ideas.

          Conference. Higher Invariants: interactions between arithmetic geometry and global analysis [regensburg_2025_hi]

          Workshop. Lean Workshop 2025 : Formalising Algebraic Geometry [heidelberg_2025_fag]

          I formalized lemmas regarding geometrically irreducibility of a ring, and its relation to tensor products. And shown this coincides with the same notion in scheme world.

          This workshop is aimed primarily at PhD students with an interest in formalising results from algebraic geomery using the Lean proof assistant. Participants will work in teams on formalisation projects designed by our guest speakers.

          Theses [thesis]

            You can find my bachelor and master thesis here.

            Bachelor’s Thesis. Cell complexes in homotopy type theory [bachelor]

            In this thesis we study the theory of CW-complexes in a synthetic way. We first introduced some important concepts of homotopy type theory and used them to define cell complexes as a homotopical pushout. After that, we have proven some topological properties of CW-complexes and calculated the homotopy groups of some examples with methods in type theory.

            Master’s Thesis. Slice, décale and realize, motivically [master]

            We study the slice filtrations of motivic ring spectra and spectral sequences associated to them. Using décalage, we could relate Adams-Novikov spectral sequences with slice spectral sequences after suitable Betti realization and étale realization, this works in both characteristic zero and $p$ cases.

            Slight changes after the submitted version.

            Detailed CV in PDF upon request.