CUHK-Shenzhen | 香港中文大学（深圳）
{Futian, Longgang}, Shenzhen | 深圳{福田, 龙岗}
130
Followers
67
Following
12
Public Repos
0
Private Repos
Language Breakdown
Lines of code distribution across 5 owned repositories
443K
Total LOC
Lean
443,165 lines
100.0%
N/A
C++
180 lines
0.0%
N/A
I
I-Shaped Developer
I-shapedSpecialist — deep expertise in Lean
Lean
C++
Collaboration Network
Global Impact visualization
Repos
49
PRs
0
Growth
+18%
Top Collaborators
No collaborator data yet.
Coding Streak
Contribution activity over the past year
1 day
179
Contributions
76
Commits
96
Pull Requests
Jun
Jul
Aug
Sep
Oct
Nov
Dec
Jan
Feb
Mar
Apr
May
Jun
Mo
We
Fr
Based on GitHub activity
Less
More
Following
67 total
Vvauted
@Vvauted
Jiayi Lu
@Kieray0w0
Junyan Xu
@alreadydone
Yang Ming-Tian
@skylee03
ypcpy
@Kensuke-Hinata
Synced via GitHub
Top Repositories
Algorithm
Verified efficient algorithms in Lean4.
39
1
Lean
transcendental
Lindemann–Weierstrass Theorem
12
0
Lean
some-theory-on-words
3
0
Lean
astrainfinita
2
0
resultant
Two weeks ago I wrote about some basic resultant theory (maybe in a bad way...) Just upload it.
2
0
Lean
lean4
Lean 4 programming language and theorem prover
1
0
Lean
std4
Standard Library for Lean 4
1
0
Lean
combinatorial-games
Combinatorial game library in Lean 4
0
0
Lean
mathlib4
The math library of Lean 4
0
0
Lean
Proof-of-Surreal
A formal proof of NOI 2020 D2T2
0
0
Lean
Open Source Impact
Contributions to external projects
126 merged PRs
leanprover/lean4
8225
leanprover-community/mathlib4
3437
leanprover-community/batteries
392
vihdzp/combinatorial-games
61
riccardobrasca/mathlib4
0
Vierkantor/lean4
0
Contributed to 6 repositories