Mathematician turned software professional with expertise in Lean4 theorem proving. Experienced in bridging rigorous mathematical logic with formal verification.

Github: BryceT233 (Bingyu Xia) 

CV : drive.google.com/file/d/10PFjKObomISNpnzSseZSmJtY5srRid5V/view?usp=drive_link 

Email: xiabingyu@gmail.com

Research interest: formal mathematics (Lean 4), derived category, stability conditions.

Papers:

1. Bingyu Xia. "Hilbert Scheme of Twisted Cubics as a Simple Wall-crossing." Transactions of the American Mathematical Society, vol. 370, no. 8, 2018, pp. 5535–5559.

2. Yinbang Lin, Sz-Sheng Wang, and Bingyu Xia. "Decorated sheaves and morphisms in tilted hearts." Journal of the Korean Mathematical Society, 2021.

3. Rebecca Tramel and Bingyu Xia. "Bridgeland stability conditions on surfaces with curves of negative self-intersection." Advances in Geometry, vol. 22, no. 3, 2022, pp. 383–408. doi: 10.1515/advgeom-2022-0009.

4. Ravi, Nikil et al. (2026). “FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?” In: ICLR 2026 Workshop: VerifAI-2: The Second Workshop on AI Verification in the Wild. url: https://openreview.net/forum?id=1LdnVndCEG.