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 se

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.