Joseph Tooby-Smith
Lecturer (Assistant Professor) in Computer Science · University of Bath
contact me at: ku.ca.htab@4184sj
(If you email me and I don’t respond in about 3 days, feel free to follow up.)
I started my academic career as a high-energy physicist, but have since moved over to computer science. Back in my high-energy physics days, I used to work on higher categories and how they could be applied and used in physics. Now I’m part of the Mathematical Foundations group at the University of Bath, and I research interactive theorem provers and their use in the physical sciences. Interactive theorem provers are computer languages that allow you to write definitions, and theorems and their proofs, in a way such that mathematical correctness is guaranteed. In particular, I am a maintainer of the project Physlib (something which I started).
Academic career
-
University of Bath
Lecturer in Computer Science
-
Reykjavik University
Postdoctoral researcher in Computer Science
-
Cornell University
Postdoctoral researcher in theoretical physics
-
University of Cambridge
PhD in theoretical physics
-
University of Oxford
Integrated Masters in mathematical and theoretical physics
A list of my publications.
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
Mar 2026
J. Tooby-Smith
arXiv-2603.08139 [hep-ph]
CS
Phys
Physics as Code: From Scans to Theorems with ITP APIs in SU(5) Model Building
Mar 2026
S. Krippendorf, J. Tooby-Smith
arXiv-2603.28406 [hep-th]
CS
Phys
A Perspective on Interactive Theorem Provers in Physics
Oct 2025
J. Tooby-Smith
Advanced science
CS
Phys
Digitalizing Wick's theorem
May 2025
J. Tooby-Smith
arXiv-2505.07939 [hep-th]
CS
Phys
Formalization of physics index notation in Lean 4
Nov 2024
J. Tooby-Smith
arXiv-2411.07667 [cs.LO]
CS
Phys
HepLean: Digitalising high energy physics
May 2024
J. Tooby-Smith
Comput.Phys.Commun. 308 (2025), 109457 (arXiv-2405.08863 [hep-ph])
CS
Phys
Smooth generalized symmetries of quantum field theories
Oct 2023
B. Gripaios, O. Randal-Williams, J. Tooby-Smith
J.Geom.Phys. 201 (2024), 105212 (arXiv-2310.16090 [hep-th])
Phys
Math
Semisimple unifications of any gauge theory
Jun 2023
A. Gomes, M. Ruhdorfer, J. Tooby-Smith
Phys.Rev.D 108 (2023) 7, 075001 (arXiv-2306.16439 [hep-ph])
CS
Phys
The Higgs squared
Oct 2022
C. Csaki, A. Ismail, M. Ruhdorfer, J. Tooby-Smith
JHEP 04 (2023), 082 (arXiv-2210.02456 [hep-ph])
Phys
Generalized symmetries of topological field theories
Sep 2022
B. Gripaios, O. Randal-Williams, J. Tooby-Smith
JHEP 03 (2023), 087 (arXiv-2209.13524 [hep-th])
Phys
Math
Flatland: abelian extensions of the Standard Model with semi-simple completions
Jun 2022
J. Davighi, J. Tooby-Smith
JHEP 09 (2022), 159 (arXiv-2206.11271 [hep-ph])
CS
Phys
Electroweak flavour unification
Jan 2022
J. Davighi, J. Tooby-Smith
JHEP 09 (2022), 193 (arXiv-2201.07245 [hep-ph])
Phys
A ν supersymmetric anomaly-free atlas
Jul 2021
B.C. Allanach, M. Madigan, J. Tooby-Smith
JHEP 02 (2022), 144 (arXiv-2107.07926 [hep-ph])
CS
Phys
Thesis: Arithmetical, geometrical, and categorical forays into particle physics
May 2021
J. Tooby-Smith
PhD thesis, Cambridge U.
CS
Phys
Math
Semisimple extensions of the Standard Model gauge algebra
Apr 2021
B.C. Allanach, B. Gripaios, J. Tooby-Smith
Phys.Rev.D 104 (2021) 3, 035035 (arXiv-2104.14555 [hep-th])
CS
Phys
Math
Inverse Higgs phenomena as duals of holonomic constraints
Mar 2021
B. Gripaios, J. Tooby-Smith
J.Phys.A 55 (2022) 9, 095401 (arXiv-2103.08923 [hep-th])
Phys
Math
Undulating Dark Matter
Jul 2020
J. Davighi, M. McCullough, J. Tooby-Smith
JHEP 11 (2020), 120 (arXiv-2007.03662 [hep-ph])
Phys
Anomaly cancellation with an extra gauge boson
Jun 2020
B.C. Allanach, B. Gripaios, J. Tooby-Smith
Phys.Rev.Lett. 125 (2020) 16, 161601 (arXiv-2006.03588 [hep-th])
Phys
Math
Supersoft top squarks
Feb 2020
T. Cohen, N. Craig, S. Koren, M. McCullough, J. Tooby-Smith
Phys.Rev.Lett. 125 (2020) 15, 151801 (arXiv-2002.12630 [hep-ph])
Phys
Solving local anomaly equations in gauge-rank extensions of the Standard Model
Dec 2019
B.C. Allanach, B. Gripaios, J. Tooby-Smith
Phys.Rev.D 101 (2020) 7, 075015 (arXiv-1912.10022 [hep-th])
Phys
Math
Geometric general solution to the U(1) anomaly equations
Dec 2019
B.C. Allanach, B. Gripaios, J. Tooby-Smith
JHEP 05 (2020), 065 (arXiv-1912.04804 [hep-th])
Phys
Math
Quantum mechanics in magnetic backgrounds with manifest symmetry and locality
May 2019
J. Davighi, B. Gripaios, J. Tooby-Smith
J.Phys.A 53 (2020) 14, 145302 (arXiv-1905.11999 [hep-th])
Phys
Math
My teaching portfolio.
Cybersecurity (Online & in-person)
co-lecturer
2026 : University of Bath
CS
Algebra and Combinatorics
co-instructor
Spring 2025 : Reykjavik University
CS
Introduction to proof assistants
TA
Fall 2024 : Reykjavik University
CS
Symmetries, Fields and Particles
TA
2020 : Cambridge University
Phys
Quantum Field Theory
TA
2019 : Cambridge University
Phys
Gauge Field Theory
TA
2019 & 2020 : Cambridge University
Phys
Theoretical Physics Part I
TA
2018 & 2020 : Cambridge University
Phys
Teaching in schools
Participant
2016 : Oxford University
An elective module about teaching in schools I took during my undergraduate.
Phys
Academic service work I do.
Maintainer of Physlib
2024 - current
Maintainer of Physlib, a Lean 4 library for formalising physics.
Bath + CMS steering committee
2026
Member of the Bath + CMS steering committee, helping coordinate the CS department.
Awards and honors I have received.
Hooke Prize
Christ Church College Oxford
2017/2018
'This prize is awarded to the most outstanding undergraduate Member of the House [Christ Church College] who achieves the highest mark in the following Honour Schools collectively: Mathematics, Molecular and Cellular Biochemistry, Chemistry, Engineering, Physics and Materials Science.'
Clifford Smith Prize
Christ Church College Oxford
2016/2017 (awarded 2018)
The Scott Prize for performance in the Physics Part A examination
University of Oxford
2015/2016
LinkThe Scott Prize for best performance in the MPhys Part B examination
University of Oxford
2016/2017
LinkScholarships
Christ Church College Oxford
2014/2015-2016/2017
Roach Prize
Christ Church College Oxford
2017/2018
'This prize is awarded to the most outstanding undergraduate across the following branches of Science: Mathematics, Biochemistry, Earth Sciences, Engineering, Physics, Materials Science and Biological Science. The most outstanding undergraduate will normally be the person placed proportionately highest in an appropriate Honour School (including in a joint School with Philosophy).'
Prize for the Best Results on the Oxford MMathPhys
Oxford University
2017/2018
Collections Prize
Christ Church College Oxford
2016
Talks I have given.
PhysLean: Digitalizing physics into Lean
Imperial (Online)
25/11/2025
PhysLean: Digitalizing physics into Lean
University of Sussex
12/11/2025
PhysLean: Digitalizing physics into Lean
University of Cambridge (HEP group)
17/10/2025
Using interactive theorem provers in physics
University of Cambridge
16/10/2025
PhysLean: Digitalizing Physics in Lean
EuroProofNet Workshop on Proof Libraries
16/09/2025
Lean and the physical sciences
Reykjavik University
02/10/2024
HepLean: Lean and high energy physics
Cornell-Syracuse joint high energy physics conference
March 20204
🎥Gauge extensions of the Standard Model
Carleton
03/04/2023
Electroweak flavour unification and anomaly free gauge groups
Program on New Directions in Particle Physics ICTP-SAIFR
13/09/2022
🎥Semisimple extensions of the Standard Model
Pheno 2022
10/05/2022
A voyage through undulating dark matter and the GUTs of u(48)
Perimeter
15/12/2020
Supersoft Stops
Bonn
13/05/2022
Local anomalies in Z' models
Edinburgh
29/04/2020
Local anomalies in Z' models
Cambridge
16/01/2020
Outreach I have done (not up-to-date).
Assumptions of Physics Youtube (University of Michigan)
Guest, discussing PhysLean with Gabriele Carcassi
2025
Cornell’s Centre for Materials Research
Volunteer at two events
2022
Cambridge HEP master classes
Volunteer
2019
Cambridge Science Festival
Volunteer
2019
Oxford Physics department and Christ Church college open days
Volunteer
2017-2018
Conferences I have attended (not up-to-date).
Organizing Mathematical Knowledge in the Age of AI and Formalization Meeting
July 2026
National Academy of Sciences, Washington DC, USA
Math
AI reasoning in theoretical physics
June 2026
Aspen Center for Physics, Summer 2026 Program
AI reasoning in theoretical physics
June 2026
Aspen Center for Physics, Summer 2026 Program
String Data 2025
Dec 2025
London Institute for Mathematical Sciences
EuroProofNet Workshop on Proof Libraries
Sep 2025
Orsay, France.
CS
Lean Together 2025
Jan 2025
CS
Higher Structures in Functorial Field Theory
Aug 2023
Math
Topological Festival Cornell
May 2023
Math
Program on New Directions in Particle Physics ICTP-SAIFR
Sep 2022
Phys
Phenomenology 2022 Symposium: From Virtual to Real
May 2022
Phys
Cavendish Laboratory Graduate Student Conference
Dec 2019
On Organising Committee and a convener.
Phys
NExT PhD Workshop
Jul 2019
Phys
Young Experimentalists & Theorists Institute
Jan 2019
Phys
YTF 11
Dec 2018
Phys
Annual Theory Meeting
Dec 2018
Phys
British Universities Summer School in Theoretical Elementary Particle Physics (BUSSTEPP)
Aug 2018
Phys
I use to run competitively. Here is a list of my persona bests (PBs) and other achievements.
PB 800m
1:59.4
PB 1500m
3:59.40
PB 3000m
8:39.6
PB 3000m Steeple chase
9:59.49
PB 5000m
15:08.92
PB 10k
30:01
National 6-stage road relays with Cambridge and Coleridge AC
3rd Team
2019
National Cross Country relays with Cambridge and Coleridge AC
2nd Team
2019
Oxford Town and Gown 10k
1st Overall
2019
Cambridge Town and Gown 10k
1st Overall
2019
Represented Cambridgeshire in track-and-field
2019
Oxford Vs Cambridge Blues varsity cross country (representing Cambridge)
2nd Indivdual, team win.
2019
National Cross Country Championships
30th Overall
2020