Zhan JING
PhD student at CS school, Shanghai Jiao Tong U. | Le diplôme d'ingénieur, Mines Paris-PSL | BSc and MSc (Honours) from Shanghai Jiao Tong U.
Email: jing_zhan@sjtu.edu.cn | zhan.jing@etu.minesparis.psl.eu
Current research interests include formal verification, algorithmic game theory, and Kalman filter.
Interactive theorem proving for algorithmic mechanism design
NuancedCoq is a notebook for introduction to Coq Ssreflect and Mathematical Component. Continuous updating.
mech.v is a Coq-ssreflect based project for algorithmic Mechanism Design.
"Collusive biddings."
"Collusive biddings."
EconCSLib is a Lean 4-mathlib based project for algorithmic game theory.
"Thanks, codex."
"Thanks, codex."
PREs
基于卡尔曼滤波的带电粒子能量重建及其应用 is a report on The 13th National Advanced Gas Detector Seminar.
"曼波 since 1960"
"曼波 since 1960"
Abstract VCG: Tie-breaking rules in VCG mechanism design is accepted by RocqPL 2026 workshop.
"formerly known as Coq"
"formerly known as Coq"
Théorie des ondelettes is a presentation on the course Distribution and Applications.
"And from here begins JPEG."
"And from here begins JPEG."
Blogs
从对角线论证开始 provides formal demonstrations on Cantor's Thm and Fixed Point Thm.