Mathematical Notes

Here are my mathematical notes: short notes about well-known or research problems, notes from self-studying mathematical texts, and lecture notes from lectures. By "mathematics", of course theoretical computer science is included.

Lecture Notes

Topics in Mathematical Science VI (数理科学特論VI) (WIP)
Lecturer: Erik Darpö, Graduate School of Mathematics, Nagoya University, Fall 2019
A gentle introduction to module theory and homological algebra, accessible to anyone with a basic undergraduate background in abstract algebra.
[PDF] [LaTeX Source] (Latest build: November 1, 2019)

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.

Short Notes

An Alternative Proof of Convergence for \( e^x \)
Proving that the exponential function converges using only the very basic facts about infinite series.

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.