Research

Research interests at the intersection of mathematical foundations, formal methods, and AI reasoning.

Research

Mathematical foundations for reliable reasoning

My research interests concern the representation, transformation, and verification of mathematical meaning within formal reasoning systems. The directions below describe research interests and ongoing exploration, not completed results or established claims.

Guiding question

How can mathematical meaning be represented, transformed, and verified within formal reasoning systems?

01

Mathematical Foundations

Type Theory, Homotopy Theory, and Higher Category Theory

I am interested in the structural foundations of mathematics, particularly dependent type theory, homotopy type theory, and higher category theory. These subjects provide mathematical languages for studying objects, constructions, proofs, and equivalences.

An important aspect of my current work is understanding how such structures can be represented within proof assistants, including Lean 4 and Cubical Agda. I am particularly interested in the role of paths, equivalences, and higher-dimensional structures in formal mathematical reasoning.

  • Dependent Type Theory
  • Homotopy Type Theory
  • Cubical Type Theory
  • Higher Category Theory
  • Formalized Homotopy Theory

02

AI for Formal Mathematics

Autoformalization and Semantic Faithfulness

Modern proof assistants can verify formal mathematical proofs with a high degree of logical precision. However, the correctness of a formal proof does not, by itself, establish that the formalized statement expresses the intended mathematical meaning. This distinction becomes especially important when artificial intelligence is used to translate mathematical language into formal representations.

$$ \text{Natural Language} \longrightarrow \text{Mathematical Language} \longrightarrow \text{Formal Code} \longrightarrow \text{Machine Verification}. $$

I am interested in how to evaluate and improve the faithfulness of these transformations. Formal correctness asks whether a generated proof satisfies the rules of a formal system; semantic faithfulness asks whether the generated formal statement accurately represents the intended mathematical problem.

I am exploring how mathematical structure, type systems, and formal verification can contribute to more reliable AI-assisted mathematical reasoning.

  • Mathematical Autoformalization
  • Semantic Faithfulness
  • Formal Verification of AI-Generated Proofs
  • Mathematical Language Representation
  • Human–AI Collaboration in Mathematics

03

Formal Methods for Trustworthy AI

Reliable Reasoning and Verified AI Systems

Beyond mathematical theorem proving, I am interested in how formal methods can support the development of trustworthy artificial intelligence. Formal specifications can describe properties that an AI system is expected to satisfy, while verification techniques can provide evidence that specific implementations or behaviors satisfy those properties.

I am interested in exploring these methods in the context of AI reasoning systems and autonomous agents. Potential applications include the verification of decision-making procedures, constraints on AI-agent behavior, and the formal specification of safety-critical workflows.

This direction aims to connect mathematical foundations with practical challenges in reliable AI.

  • Formal Specification
  • AI Reasoning Verification
  • Verified AI Agents
  • Type-Theoretic Approaches to Reliability
  • Formal Methods for Decision-Making Systems

Research philosophy

Verification in relation to meaning

I view formal verification not only as a technique for establishing logical correctness, but also as part of a broader effort to understand the relationship between mathematical structures, their representations, and their intended meaning. My long-term interest is in mathematical frameworks that make machine reasoning more transparent, interpretable, and verifiable.