Skip to content
View jstoobysmith's full-sized avatar

Organizations

@HEPLean

Block or report jstoobysmith

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
jstoobysmith/README.md

About me

Institution
Masters University of Oxford Integrated masters in mathematical and theoretical physics. Top of year in third, and fourth years.
PhD University of Cambridge Supervised by Ben Gripaios. PhD in theoretical physics. Thesis focused on the application of techniques in mathematics to solve problems in physics. Including the use of number theory, category theory and geometry.
Postdoc Cornell University Started a program to digitalise results from high energy physics into Lean 4. Also, continued use of higher category theory in physics by studying generalized symmetries.
Postdoc Reykjavik University Currently using category theory in computer science.

What am I currently working on?

Description
HepLean This is a project to digitalize results from high energy physics in Lean.
Perturbation theory in Lean I'm working on formalizing perturbation theory from theoretical physics into Lean 4.
Metaprogramming for HepLean I'm writing metaprograms for HepLean to help with refactoring.

Academic skills

Physics Mathematics Computer Science
Particle physics Category theory Lean 4
Generalized symmetries Higher categories Functional programming
Topological field theories Topos theory Theorem proving
Guage algebras and their extensions Lie groups and Lie algebras

Pinned Loading

  1. HEPLean/HepLean HEPLean/HepLean Public

    A project to digitalise results from high energy physics into Lean.

    Lean 87 6