A student of pure math in pursuit of building bridges from pure mathematics to formalized and AI-driven reasoning.