Code

• RL Theory in Lean
  Here I take the ambitious goal to formalize RL theory in Lean. I have formalized the almost sure convergence of linear TD and Q learning with Markovian samples.

• Reinforcement Learning: An Introduction
  This repo is a Python implementation of the RL textbook from Sutton & Barto. This is my course project when I took Rich’s RL course in my first term at the University of Alberta, when the book was about to complete.

• PyTorch Deep RL
  This repo includes almost all codes of my papers during my DPhil. It helps me prototype new ideas easily but is unfortunately no longer maintained.

Blog

• Tips for LaTeX
• Tips for writing (a paper)

Hobby

• Sports: alpine skiing, swimming, marathon, table tennis
• Video games: Black Myth: Wukong, Elden Ring, Monster Hunter, Zelda, Mario Kart, Tetris 99, Civilization, Resident Evil, Overwatch, Hearthstone, DoTA, Warcraft III, PopKart …

Current UVA Students

• If you need me to approve your OPT / CPT (because I am listed as your advisor), please email me the required information. You can find the required information here.