Kaomet

On paper, current AI/ML can allready do this with math and proofs. But it's still a grind, and doesn't produce pretty pictures like a GAN.

Actually, I don't see what's preventing Deutsch from formalizing his work in an allready existing proof assistant, like Lean or Coq.

Does it make predictions ? It looks like a logical fundation for physics. In computer science, it's the equivalent of inventing a new programming language instead of solving actual problems.

It looks like a physicist is re-inventing the axiomatic method, with possible/impossible as a dichotomy, instead of true/false.

That's programming language work for physical theory, not physics.