academic.lean
do: #cv #github #linkedin #email #orcid #transition
ZHAI Jun portrait
import Mathlib
open scoped Classical
 
namespace Jun
 
structure Profile where
name role focus affiliation : String
 
/--
Personal info
--/
 
def me : Profile :=
{ name := "ZHAI Jun"
role := "PhD student, Mathematics"
focus := "AI4Math"
}
 
end Jun
 
 
/-- last_update: 2026-01-07 --/