Publications / Writings

This work introduces LeanCat, a benchmark suite designed to evaluate automated theorem provers on formalized category theory within the Lean 4 / mathlib ecosystem. The project focuses on abstraction-heavy reasoning tasks derived from modern categorical mathematics, reflecting the structural nature of contemporary mathematical libraries.

In this collaboration, my primary contribution was the formalization of category-theoretic statements using the Lean 4 theorem prover. Specifically, I translated natural mathematical formulations from category theory into precise machine-verifiable formal language, constructing theorem statements and formal structures compatible with the Lean / mathlib framework.

This work highlights the process of bridging traditional mathematical exposition and formal proof assistant languages, demonstrating how abstract categorical concepts can be systematically encoded into a rigorous computational framework. The project contributes toward building reliable benchmarks for evaluating progress in formal mathematics and AI-assisted theorem proving.

[GitHub]

This project develops a systematic formalization of core algebraic structures in the Lean 4 theorem prover. Starting from the foundational definitions of groups, rings, and fields, the implementation explores how classical algebraic hierarchies can be encoded as machine-verifiable mathematical structures.

The work demonstrates the use of Lean's type class mechanism and structure inheritance to construct algebraic hierarchies including monoids, additive groups, commutative rings, and fields. The project also illustrates how formal proofs interact with the mathlib algebraic ecosystem, including tactics such as group, abel and ring.

Through this implementation, natural-language algebraic definitions are translated into precise formal structures, highlighting the methodology required to bridge classical abstract algebra and formal proof assistant languages.

[PDF]  |  [Code]

This project implements a foundational formalization of category theory using the Lean 4 theorem prover. The work begins with a direct encoding of the definition of a category, including objects, morphisms, identity maps, and composition laws, together with proofs of associativity and identity properties.

Building on this foundation, the project formalizes essential categorical constructions such as functors and natural transformations, demonstrating how categorical abstractions can be represented within Lean's dependent type theory.

Particular attention is given to the treatment of universe levels and structural notation, allowing categorical objects and morphisms to be expressed in a form compatible with Lean's type system while remaining close to standard mathematical notation.

[PDF]  |  [Code]

This work establishes a unified categorical perspective on two classical correspondence theorems: the fundamental theorem of Galois theory and the corresponding of covering spaces with its fundamental groups. Beginning with the order-theoretic concept of Galois connections between partially ordered sets, the paper demonstrates how this notion naturally categorifies to the theory of adjoint functors.

The core contribution shows how both Galois theory in algebra and covering space classification theorem in topology emerge as concrete instances of the same abstract adjunction. The work bridges these seemingly distinct mathematical domains through the common language of category theory, making the structural parallels explicit and rigorously formalized. Accessible to undergraduates with basic knowledge of abstract algebra and algebraic topology, the paper includes a self-contained introduction to the necessary categorical foundations.

This work introduces the fundamental concepts of algebraic topology from a categorical perspective, providing a natural motivation for the study of homotopy theory. It builds a bridge between fundamental groups and fundamental groupoids, concretely demonstrated by proving the categorical equivalence of the van Kampen theorem under its colimit formulations for groupoids versus groups. The work further categorifies covering space theory, establishing an isomorphism between the fundamental groupoids of covering spaces and the structures of Galois theory, thereby deepening the categorical language of algebraic topology. It also provides an introduction to homotopy theory and homotopy type theory, undertaking initial steps in formalizing some of these foundations using the Lean theorem prover.

This work entailed a study and deep dive into fractal constructions and the definition and computation of Hausdorff dimension. It introduced the concept of fractal dimension through the classic historical problem of coastline measurement and employed Iterated Function Systems (IFS) to construct fractals, thereby introducing the concept of a fractal generating group. By analyzing geometric structures through algebraic methods, it culminated in a conjecture relating the lower bound of a fractal's Hausdorff dimension to the order of its generating group, attempting to build a bridge between fractal geometry and algebra.

This project explored a method of assisting mathematical learning through AI-generated code. By formulating precise prompts based on specific problems, I designed and implemented simple Python programs to deepen the understanding of abstract concepts. Key implementations include: a machine learning model to analyze winning strategies in the K₅ graph game related to Ramsey's Theorem; a 2D visualization tool for holomorphic functions in four dimensions with automatic singularity detection; and a program that visualizes scalar fields and automatically computes and plots their corresponding gradient vector fields. The inspiration for all programs stemmed from challenges encountered in coursework, and their development significantly enhanced my comprehension of the underlying mathematical theory.

As a student teaching assistant, I created and delivered a lecture based on a group theory permutation problem from the animated series Futurama, specifically the "mind-switching" dilemma. This approach was designed to help students new to abstract algebra deepen their understanding of group structures and permutations. The lecture included a full solution to the problem and concluded with a related exercise for further student practice.

Study notes on the foundational concepts of commutative algebra, suitable as a primer for a seminar. They detail the necessary prerequisites for the subject, offering a review of groups, rings, and fields, and include a discussion of various special types of ideals.

A large-scale visualization project on prime number spirals. Utilizing Python, it generates Sacks, Ulam, and other prime spirals over extensive numerical ranges to investigate prime distribution patterns at a large scale and analyze their underlying structures. The project also involves computing prime-rich polynomials, specifically evaluating the prime density of famous cases like Euler's polynomial n² + n + 41.

These are comprehensive study notes on Tom Apostol's Introduction to Analytic Number Theory. They meticulously document all essential arithmetic functions used in the field and cover classic theorems on the distribution of prime numbers. The notes serve as a dictionary of analytic number theory functions, providing detailed definitions and explanations for each. The latter part discusses the asymptotic approximation of the prime-counting function.