[tabs]

[tab title=“Education”]

[timeline]

[timeline-event date=“Sep 2021 – Jun 2025” title=“Xi’an Jiaotong University, China”]

Bachelor of Mathematics and Applied Mathematics

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

[/timeline-event]

[timeline-event date=“Aug 2025 – Present” title=“National University of Singapore, Singapore”]

Master of Science in Mathematics

[/timeline-event]

[/timeline]

[/tab] [tab title=“Research and Study Experience”]

[timeline]

[timeline-event date=“Jun 2023 – Aug 2023” title=“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).

[/timeline-event]

[timeline-event date=“Jan 2024 - Present” title=“Peking University, China”]

Beijing International Center for Mathematical Research

• Seminar:
  • (Jan 2024)
    • AI for Mathematics: Mathematics formalization and theorem proving
  • (Jul 2024)
    • AI for Mathematics: Formalization on abstract algebra
    • (Awarded the special prize and offered chances for further cooperation)
• Conference & Workshop:
  • (Sep 2024)
    • AI for Mathematics Workshop on Lean, Automated Reasoning and Beyond
  • (joint with Westlake University, Jan 2025)
    • Conference on AI for Math and formalization
  • (May 2025)
    • RUC&PKU joint Lean Workshop
• Research projects: (GitHub username: Yu-Misaka)
  • Adding Stacks Project tags (Merged into master)
  • Formalization of Jacobson-Noether theorem (Merged into master)
  • Formalization of filtered and graded ring (Work in progress)
  • Formalizing Koszul Complex (Work in progress)
• (joint program with Ubiquant inc., Mar 2025 - Present)
  • Full-time internship on formalization and AI

[/timeline-event]

[/timeline]

[/tab] [tab title=“Contact”]

  You can mail to hi@vertin.me or use the form below.

[/tab]

[/tabs]

[friend-card name=“Yu-Misaka” ico=“https://cdn.academe.city/vertin.me/persistent-image/109365723.webp” url=“https://github.com/Yu-Misaka”]GitHub[/friend-card] [friend-card name=“Hilbert-Yu” ico=“https://cdn.academe.city/vertin.me/persistent-image/210fd3b105f46675acb84497c6a6542900407f78.webp” url=“https://space.bilibili.com/71108056”]BiliBili[/friend-card]