Research and writing

Nov 1, 2024 — In-progress masters thesis defining connections, curvature, and Chern-Weil theory in the discrete setting of homotopy type theory.

Dec 15, 2021 — Gottlob Frege had a healthier and more humanistic view of the separation between the doing of math and the formalization of math than today's AI advocates do.

Dec 16, 2020 — Mathematicians have been exploring the advantages of locale theory for 60 or so years, along with its related disciplines of topos theory and type theory. When you tie one hand behind your back (such as avoiding the use of the existence of points, the axiom of choice, and/or the law of the excluded middle) then the constructions and proofs you invent can be more illuminating and deeper than before. I want to convince you that this may be true for algorithmic randomness notions.

Nov 9, 2018 — Categories and modalities for smoothness Categories and modalities for smoothness Greg Langmead Abstract Differential cohesion and modal HoTT promise to give access to constructions from differential geometry. In this series of talks I will tell a story that takes us from the classical definition of a smooth manifold to differential cohesion in a category where we can interpret modal HoTT. I will assume only basic topology and category theory and will provide details that are sometimes waved away. I will also motivate the study of smooth manifolds as a worthy field with surprising results and tough open questions such as the smooth four-dimensional Poincaré conjecture.

Aug 11, 2009 — This post is for anyone who enjoyed watching the movies, is willing to re-watch the extended editions, and has a desire to read the books but hesitates to invest the full time required to read 3 novels.

Oct 21, 2002 — What we build here amounts to a mathematical treatment of a physical treatment of a mathematical construction of Donaldson.