Jakob von Raumer

About me

• First-year Ph.D. student
• Supervisor: Thorsten Altenkirch
• Interests: Homotopy Type Theory, Formalization of Mathematics, Interactive Theorem Proving

Contact information

• Address: Office A04, School of Computer Science, Wollaton Rd, Nottingham, NG8 1BB
• E-mail address: psxjv4@nottingham.ac.uk
• Jabber: javra@jabber.ccc.de
• GitHub | Bitbucket | Panoramio | Google Plus

Publications, Talks, etc.

• Homotopy Type Theory in Lean
  with Floris van Doorn and Ulrik Buchholtz
  International Conference on Interactive Theorem Proving, Brasília, Brazil, 2017
  [PDF] [ArXiv]
• The Lean theorem prover (system description)
  with Leonardo de Moura, Soonho Kong, Jermy Avigad, and Floris van Doorn
  International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015
  [PDF]
• Master Thesis: Formalization of Non-Abelian Topology for Homotopy Type Theory
  Supervisors: Prof. Jermy Avigad, Prof. Steve Awodey, Prof. Gregor Snelting
  [PDF] [GitHub] [Slides (German)]
• The Jordan-Hölder Theorem
  Archive of Formal Proofs
  [Proof outline] [AFP]
• Secondary Sylow Theorems
  Archive of Formal Proofs
  [Proof outline] [AFP]
• Bachelor Thesis: Visualization of Hyperbolic Tessellations
  Supervisors: Tanja Hartmann, Martin Nöllenburg
  [PDF (German)] [Slides (German)] [Slides (English)]