Interests
Proof mining focuses on extracting quantitative data from classical mathematical proofs using logic tools, such as functional interpretation. In some sense, proof mining can be viewed as a partial revival of Hilbert’s grand program to reduce infinitary mathematics to finitary objects in (higher-order) arithmetic. My thesis project is to structurally extend existing methodologies in proof mining to continuous model theory.
Besides my thesis project, some of my logic interests include
- Proof theory in general
- Nonclassical logics, especially fuzzy logics and substructural logics
- Constructive mathematics
- Set-theoretic and type-theoretic foundations
- Proof assistants
- Categorical logic
Paper
- Approximate Completeness of Hypersequent Calculus for First-Order Łukasiewicz Logic, submitted. Preprint version available on ArXiv.
You can find my CV here.
Slides
Here are some slides of my previous talks.
- Life Pro Tip: How to Responsibly Obtain More Real Numbers? in the Pizza Seminar
- Proof Theory of Continuous Logic in Fudan Logic Student Seminar
- Defying Gödel: Let’s Prove the Consistency of Peano Arithmetic in the Pizza Seminar
Projects
I also have ongoing projects formalizing Tarski geometry and Proof Theory in Lean.