Formal verifications of results from my papers, written in the Lean 4 proof assistant with the Mathlib library. For each paper, the repository states the main theorems in Lean, proves them, and records every difference between the printed statements and the Lean statements.
H.-T. Yau and J. Yin, arXiv:2501.01718. Lean repository on GitHub.
Verified: Theorems 2.2–2.6 of the paper — delocalization, the local semicircle law, quantum diffusion, generalized quantum unique ergodicity and bulk universality. The Lean proofs are complete: no unproved steps, and no axioms beyond Lean’s standard ones.
Assumed: one cited result, the fixed-energy universality of Dyson Brownian motion (Landon, Sosoe and Yau, Adv. Math. 2019). It enters only Theorem 2.6, as an explicit hypothesis; Theorems 2.2–2.5 use no external input.
Code: Lean repository on GitHub, with the README and a statement-by-statement comparison of the paper and the Lean code.
S. Dubova, K. Yang, H.-T. Yau and J. Yin, arXiv:2503.07606. Lean repository on GitHub.
Verified: Theorems 2.2–2.6 of the paper — delocalization, the local semicircle law, generalized quantum unique ergodicity, quantum diffusion and bulk universality. The Lean proofs are complete: no unproved steps, and no axioms beyond Lean’s standard ones.
Assumed: one cited result, the fixed-energy universality of Dyson Brownian motion (Landon, Sosoe and Yau, Adv. Math. 2019). It enters only Theorem 2.6, as an explicit hypothesis; Theorems 2.2–2.5 use no external input.
Code: Lean repository on GitHub, with the README and a statement-by-statement comparison of the paper and the Lean code.
S. Dubova, F. Yang, H.-T. Yau and J. Yin, arXiv:2507.20274. Lean repository on GitHub.
Verified: Theorems 2.1–2.5 and 2.7 of the paper, in every dimension d ≥ 3 — delocalization, the local law, quantum unique ergodicity, bulk universality and quantum diffusion for the random band matrix, and the corresponding results for the block Anderson model. The Lean proofs are complete: no unproved steps, and no axioms beyond Lean’s standard ones.
Assumed: one cited result, the fixed-energy universality of Dyson Brownian motion (Landon, Sosoe and Yau, Adv. Math. 2019). It enters only the bulk universality statements (Theorem 2.4 and the universality part of Theorem 2.7), as an explicit hypothesis; Theorems 2.1, 2.2, 2.3 and 2.5 use no external input.
Code: Lean repository on GitHub, with the README and a statement-by-statement comparison of the paper and the Lean code.