简历 Curriculum Vitae

Xi’an Jiaotong University, China

Bachelor of Mathematics and Applied Mathematics

• Current GPA: 3.36/4.3 (84.04/100)
• Abstract Algebra (94/100), Advanced Algebra and Analytic Geometry (93/100)
• Language Proficiency: IELTS 8.0/9.0, CET6 646/710
  

University of Wisconsin – Madison, US

Exchange program

• GPA: 4.0/4.0
• Courses Studied: Introduction to Cryptography (4.0/4.0), Intro-Combinatorics (4.0/4.0).
  

Peking University, China

Beijing International Center for Mathematical Research

• Seminar: AI for Mathematics: Mathematics formalization and theorem proving
• Thorough study of Lean, a programming language for formalization and theorem proving. Utilized Lean to formalize theorems in number theory, algebra, analysis, and even Euclidean geometry.
  

Wolfram Research Inc., US

Internship: Wolfram Student Ambassador

• Beta testing for Wolfram Mathematica. Contributing to the Wolfram community.
  

Peking University, China

Beijing International Center for Mathematical Research

• Seminar: AI for Mathematics: Formalization on abstract algebra
• Conference: AI for Mathematics Workshop on Lean, Automated Reasoning and Beyond
• Awarded the special prize and offered chances for further cooperation.
• Working on connecting the Stacks Project with mathlib4. Assisting in building an automated theorem search engine.
  

Peking University, China

Beijing International Center for Mathematical Research

• Research Project: (GitHub username: Yu-Misaka)
     - Formalization of Jacobson-Noether theorem
     - Formalization of filtered and graded ring, filtered and graded category
  

National College Students Mathematical Competition

Third Prize

Thesis: The Kronecker-Weber Theorem and Current Progress in its Formalization

https://misaka-yu.com/usr/uploads/2024/10/3138034828.pdf