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.

To me good Lean code for physics has, at least, the following features:

1. Organized as API around key data structures
2. Has no axioms
3. Has short moules with a clear purpose
4. Has good clear and concise documentation (not AI slop)
5. Has concise proofs
6. Uses existing formulizations where possible – doesn’t reproduce work already done
7. Uses a fixed naming convention (following e.g. that of Mathlib)
8. … probably many more

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.

Really since the start of the AI boom there has been discussions about companies’ use of data to train their models, whether that be reddit posts, books, copy-righted works of art, or closer to home for me academic papers or formalized definitions and proofs. The law sides with the AI companies here, saying that the use of such training data is “fair-use”. However, there is another question here: is it academic misconduct not to cite the training data you (or someone else) used to train the AI model you used to help write your paper, or come up with your theory? I think many would fall back to the above “fair-use” ruling on this and say no. However, citations have nothing to do with copyright. They are about crediting work that has been done, make it easier to set precedents and have been so fundamental to scientific progress that it is drilled into students from very early on.

It is my opinion that if you writing an academic paper or coming up with a theory with the help of an AI, and you are not citing the training data you (or the AI makers) used, you are not working to the level of academic integrity that for some many decades with have prescribed to.

The real problem is that asking for this level of academic integrity takes away many AI companies profit mechanisms.

(My views here are totally my own, and do not represent any position of projects I work on etc.)

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 results. If it did, the amount of material one could formalize into an ITP from physics would be extremely limited. In the same way that a physics paper does not necessarily need to start with an axiomization of the area of physics, a formalization does not either. As long as the starting point is well-defined and can be mathematically formulated, then we are good - and you still get a lot of the benefits from Lean.

It is this approach which allows us in PhysLean to formalize areas related to quantum field theory, the Higgs boson, high-level results in classical mechanics and special relativity etc. We pick a starting point, and then derive results from that starting point - just as a physics paper does. Those starting points can be interconnected to each other, and could be refactored, and moved further and further back until I meets an axiomization (or multiple), if indeed possible.

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.

Take for example, Wick contractions, which are often taught in a Master’s level quantum field theory course. In computer science they essentially correspond to unordered pairings of indices in a list where each index is in at most one pair. There are lots of ways one could represent this data structure in a program like Lean, from inductive types based on the inductive definition of a list, to involutions from the indices of the list back to itself. After lots of trail and error the definition I ended up with is the one shown below. It may not be the prettiest definition in the world, but it was the one that was easiest to work with, and to build and API around.

For a long time academia has relied on an element of trust. This is especially in areas like physics or the natural sciences where papers do not give every nitty-gritty detail of proofs, calculations, or analyses.

When reading papers in these disciplines we are putting our trust in the authors that they have checked the proofs, calculations or analyses, and that they are not spreading misinformation (or even worse disinformation).

As AI have become more prevalent, it is up for debate whether the quality of information in papers has decreased. I personally would argue it has, but I think something which less contentious is that: the ability to trust papers and their content has gone down.

There are ways to increase the trust we have in papers, these include things like peer-review, although I would argue that in some areas this doesn’t put as much trust back into papers as one would naively hope. Another way is through some sort of verification methods, like interactive theorem provers.

In some of my talks and papers I try and articulate how I view the difference between mathematics and physics, from the point of view of programs like Lean.

In both mathematics and physics there are definitions, equations, theorems and proofs. Each such result has its “mathematical context” - the mathematical structures that make it up and the way that those structures are arranged to make a mathematically well-defined statement. For example, the mathematical context of the statement ‘F = m * a’ is that it is a propositional equality between two vectors and a non-negative real number.

Mathematics is about the beauty or complexity of said the mathematical context, or the insights which the mathematical context gives you.

However in physics, each result carries, in addition to its mathematical context, physical context. For example in ‘F = m * a’, the vector ‘F’ describes a force, and ‘a’ an acceleration. Physics cares about both the physics context of a result and the mathematical context, and importantly, how they interact with one another.

To me this distinction between maths and physics clearly distinguishes them as distinct subjects, and goes against the “spectrum” between physics and maths that is sometimes portrayed. It explains why, for example, maths papers are split into definitions and theorems, whilst physics papers are written in prose.

Interactive theorem provers (ITPs) are built around the mathematical context of results, and they help us ensure that the mathematical context is correct. However, ITPs don’t say anything about the physics context of results. In the project PhysLean, we are trying to include that physics context through organization, documentation, names of lemmas and theorems, and in the style of proves.