And I have to ask - I'm just asking, we're just having a conversation here, I'm the Good Cop in this scenario you understand - if we, mathematics, the academy, humans, are really gaining anything if we can generate permutations of text that, given an infinite number of monkeys^H^H^H^H^Henough GPUs we can generate proof-shaped things that make a solver program turn the green light on.
In this scenario, Kurt Gödel is the Bad Cop.