Notes & Technical Writing

Here are my notes: short notes, mostly expository, about well-known or research problems, notes from self-studying mathematical texts, and lecture notes from lectures.

Expository Notes & Tutorials

An alternative proof of convergence for \( e^x \)
Proving that the exponential function converges using only the very basic facts about infinite series.
Reynald Affeldt has formalized the proof in Coq, using the Mathematical Components Analysis library.

Introduction to topological K-theory
A brief introduction to the K-theory of topological spaces and its connection with the K-theory of C*-algebras.

Formalized Mathematics

The Eckmann-Hilton Theorem
The higher homotopy groups are abelian. Mostly following the proof of Theorem 2.1.6 in the HoTT Book.


Securing Complex Software Systems Using Formal Verification and Specification
This was originally written as a course report for COMP 116, "Introduction to Computer Security", Fall 2017, Tufts University.

Project Reports

Formalizing the DFUDS Representation in Coq
Project report for CS 591K, "Foundations and Pragmatics of Dependently-Typed Systems", Spring 2019, Boston University.
(Note that the work reported is still very preliminary, and the approach outlined might turn out not to be the most best approach.)

Exploring Corpora-Based Music Classification: Classifying Japanese Popular Music using Lyrics
Project report for COMP 150WC, "Working with Corpora", Fall 2018, Tufts University.