The answers to some questions

• Why now and why has this not been done before?

The project to formalise mathematics only started in 2017. It has taken a while for sufficient areas of mathematics to be formalised such that a project in high energy physics like this is feasible.

• Can we formalise, using Lean, everything in high energy physics?

There are four types of statements in high energy physics: Precise statements made in a precise way. Imprecise statements made in a precise way. Precise statements made in an imprecise way. And imprecise statements made in an imprecise way. Each of these type of statements has its advantages. For instance, an imprecise statements made in an imprecise way is useful when we don't get bogged down in the details, because what is important is the big picture.

Both precise and imprecise statements made in a precise way lend themselves to formalisation in Lean. Statements made in an imprecise way do not naturally lead themselves to formalisation. However, not all hope is lost, and there are a number of strategies one may take: Make the necessary assumptions such that the statement becomes precisely made; Make the imprecise statement part of the assumptions of other theorems, proofs, definitions etc, making a comment about the context of the imprecise statement.

• How much work would it be to formalise my paper on X?

This depends. If the broad area of high energy physics your paper lies in has already had its foundations formalised, then probably not so long. However, at this early stage of HepLean this is not true for most areas. In these cases, the underlying foundations of the area would have to first be formalised which make take some time.

• What are the current limitations of this project?

There is a steep learning curve for Lean, this combined with a current lack of broad usage in the high-energy physics community, means it is not so appealing for high energy physicists to learn Lean.

There are certain areas of mathematics heavily used in high energy physics that have yet to be formalised.

• What about path integrals?

It is well-known to the high energy physicists that path integrals are not mathematically well-defined. This seems like an obstacle to formalising high energy physics. However, the physicist knows how to define the data of a (Lagrangian) quantum field theory, through the definition of fields, representations on those fields and a Lagrangian. They also know how to take this data and follow a set of rules to calculate e.g. cross-sections. It is likely that this process can be formalised, even though the path integral cannot.

[This is of course ignoring the possibility that a well-defined notion of the path integral exists, through e.g. the geometric cobordism hypothesis.]