Skip to content
View astrainfinita's full-sized avatar
142 followers · 71 following
  • CUHK-Shenzhen | 香港中文大学（深圳）
  • {Futian, Longgang}, Shenzhen | 深圳{福田, 龙岗}

Achievements

Achievement: Pull Sharkx3Achievement: Pair Extraordinairex2Achievement: StarstruckAchievement: QuickdrawAchievement: Arctic Code Vault Contributor

Achievements

Achievement: Pull Sharkx3Achievement: Pair Extraordinairex2Achievement: StarstruckAchievement: QuickdrawAchievement: Arctic Code Vault Contributor

Organizations

@bicmr-ai4math

Block or report astrainfinita

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
astrainfinita/README.md

Hello world 👋

Untutored pure mathematics (notably theoretical computer science) learner / Exploring the future of proving and programming in Lean / Former competitive programmer

  • I’m a mathlib contributor. My work spans formalizing mathematics, designing and refactoring foundational mathematical APIs, and improving build performance.
Some competitive programming achievements

  • NOI[1] 2019 Joint Provincial Team Selection The 2nd Place (in all 12 provinces)

  • NOI[1] 2019 The 63rd Place

  • The 2020 ICPC Asia Shanghai Regional Contest The 13th Place

  • The 2020 ICPC Asia Jinan Regional Contest The 10th Place

  • The 2020 ICPC Asia-East Continent Final Contest The 14th Place

  • The 2022 ICPC Asia Nanjing Regional Contest The 5th Place (Solo)

1. National Olympiad in Informatics (China)

Popular repositories Loading

  1. Algorithm Algorithm Public

    Verified efficient algorithms in Lean4.

    Lean 41 1

  2. transcendental transcendental Public

    Lindemann–Weierstrass Theorem

    Lean 12

  3. some-theory-on-words some-theory-on-words Public

    Lean 3

  4. resultant resultant Public

    Two weeks ago I wrote about some basic resultant theory (maybe in a bad way...) Just upload it.

    Lean 2

  5. astrainfinita astrainfinita Public

    2

  6. std4 std4 Public

    Forked from leanprover-community/batteries

    Standard Library for Lean 4

    Lean 1