Joseph Tooby-Smith

I would like to promote the use of the following term: AI-safe task to mean the following: A task which can be given to an AI, and for which it is universally trivial for an expert human to verify whether the task has been completed or not based on the ch…

There are three recurring friction points in Physlib.

Lean is becoming increasingly prevalent, as AI demonstrates that formalization is a promising future for mathematics, physics, and beyond.

Harmonic, Axiom, Math Inc, Axiomatic AI, and others — all companies whose mission includes, in some form, the goal of AI for formalization.

Recently there has been a dramatic increase in the number of people using AI to do physics in Lean.

A future without Physics papers?

As interactive theorem provers get increasingly popular, and as AI makes it easier to write correct, and compiling Lean code, I think it is important to distinguish good from bad correct Lean code in the context of physics.

I myself am not a researcher in AI, however, I work in interactive theorem provers, which is a hot-topic in the AI world, and thus interact with a lot of people and companies in the AI sphere.

Since this keeps coming up in different scenarios, I thought it was worth writing something about (this is also discussed in one of my papers): Formalizing results from physics in to Lean or another ITP does not necessarily imply the axiomization of those…

One of the things which I found interesting from formalising Wick’s theorem (the precursor to Feynman diagrams), is how many of the ‘complex’ things physicists work with can be reduced to very simple data structures in computer science, and how the precise