Can you say more about how it's equivalent to the halting problem?
>In mathematics, Richardson's theorem establishes the undecidability of the equality of real numbers defined by expressions involving integers, π, ln 2 , {\displaystyle \ln 2,} and exponential and sine functions. It was proved in 1968 by mathematician and computer scientist Daniel Richardson of the University of Bath.
>Then, an SR algorithm would ideally re-discover the well-known expression (or an equivalent formulation thereof) F = G × m1 m2 r2 , with G = 6.6743 × 10−11, by opportunely combining the mathematical operations (here, of multiplication and division) with the variables and constant at play
F in this case is the second derivative of the curve of motion of mass, _either_ mass. Yet given a sampling of data the best you could do would be one equation for the motion of mass one and another for m2. The fact they are equal is not an NP-hard problem but equivalent to the halting problem. Similarly for deciding that the equation is a differential equation.