AI-safe tasks
I would like to promote the use of the following term: AI-safe task to mean the following:
Joseph Tooby-Smith
A portfolio website
Latest posts
An idea: Maintained and unmaintained files
There are three recurring friction points in Physlib.
Contributions to open-source projects
Lean is becoming increasingly prevalent, as AI demonstrates that formalization is a promising future for mathematics, physics, and beyond.
A message to AI companies
Harmonic, Axiom, Math Inc, Axiomatic AI, and others — all companies whose mission includes, in some form, the goal of AI for formalization.
Physics, AI and Lean
Recently there has been a dramatic increase in the number of people using AI to do physics in Lean. This ranges from seasoned researchers to weekend hobbyists.
A future without physics papers?
A future without Physics papers?
Citations and AI
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.
Good Lean code for Physics
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. This is naturally related to the question of how to detect ‘AI slop’ when it comes to Lean code in physics.
Axiomization vs Formalization
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):
Datastructures and physics
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 representation of the data structure we reduce them to can massively effect how easy it is to work with them or think about them.