@futurebird @JorgeStolfi @dymaxion @whknott I think that all the way back to at least Leibniz there was this idea that you might be able to automate the general search for truth by reducing it to turn-the-crank derivations. It's the same impulse that leads people to treat ChatGPT as an oracle.